Base Projection of Marked Paths

Abstract

Base Projection of Marked Paths.

Theorem 1.1 (Path projection and digit equality).

$$\forall charge\in \mathrm{Bool},\forall s\in \mathrm{List}\left(\mathbb{Z}\right),\forall t\in \mathrm{List}\left(\mathbb{Z}\right),\forall xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\forall p\in \mathrm{Path}\left(prefixRawAutomaton,s,t,xs\right),\forall u\in \mathrm{Fin}\left(1492\right),\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(s\right),\mathrm{some}\left(GetElem.getElem\left(s,0\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{val}\left(u\right),\mathbb{Z}\right)\Rightarrow \left(\exists v\in \mathrm{Fin}\left(1492\right),\exists q\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(charge\right),u,v,xs\right),\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(t\right),\mathrm{some}\left(GetElem.getElem\left(t,0\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{val}\left(v\right),\mathbb{Z}\right)\wedge \left(\forall output\in \mathrm{Bool},\mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]r:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(r\right),\mathrm{some}\left(GetElem.getElem\left(r,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(r\right),\mathrm{some}\left(GetElem.getElem\left(r,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)=\mathrm{pathOutputs}\left(\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]r:\mathrm{Fin}\left(1492\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(r\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(r\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),q\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/MarkedBaseProjection.marker_base_projection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The underlying base index follows every raw marker transition. Starting from any valid base index, path induction constructs an indexed base path with the same labels. Its terminal index is exact, and its input and output signed-digit streams equal those observed through the raw marker states. toNat denotes integer conversion to a natural number, and getD uses zero for absent entries.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedBaseProjection.marker_base_projection
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization