Marked Path Selection

Abstract

A good completed marker path separates into its lower tail, selected digit and higher suffix.

Theorem 1.1 (Selected transition and phase snapshots).

$$(\lambda digit:\mathrm{List}\left(\mathbb{Z}\right)\to \left(\mathbb{N}\to \mathbb{Z}\right)\mapsto \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(\mathrm{prefixRawAutomaton},s,t,xs\right),\left(\left(\mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(s\right),\mathrm{some}\left(GetElem.getElem\left(s,1\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\wedge \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(t\right),\mathrm{some}\left(GetElem.getElem\left(t,1\right)\right),\mathrm{none}\left(\right)\right),0\right)=4\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(7<List.length\left(t\right),\mathrm{some}\left(GetElem.getElem\left(t,7\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\Rightarrow \left(\exists u\in \mathrm{List}\left(\mathbb{Z}\right),\exists v\in \mathrm{List}\left(\mathbb{Z}\right),\exists as\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\exists bs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\exists a\in \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z},\exists before\in \mathrm{Path}\left(\mathrm{prefixRawAutomaton},s,u,as\right),\exists after\in \mathrm{Path}\left(\mathrm{prefixRawAutomaton},v,t,bs\right),\left(\left(\left(\left(\left(\left(\left(\left(xs=\mathrm{append}\left(as,\mathrm{cons}\left(a,bs\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(u\right),\mathrm{some}\left(GetElem.getElem\left(u,1\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,1\right)\right),\mathrm{none}\left(\right)\right),0\right)=1\right)\wedge (v,a)\in \mathrm{successors}\left(u\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(7<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,7\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\wedge \mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{digit}\left(q,10\right),p\right)=\mathrm{append}\left(\mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{digit}\left(q,10\right),before\right),\mathrm{cons}\left(\mathrm{digit}\left(v,10\right),\mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{digit}\left(q,10\right),after\right)\right)\right)\right)\wedge \mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{digit}\left(q,12\right),p\right)=\mathrm{append}\left(\mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{digit}\left(q,12\right),before\right),\mathrm{cons}\left(\mathrm{digit}\left(v,12\right),\mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{digit}\left(q,10\right),after\right)\right)\right)\right)\wedge \mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(q\right),\mathrm{some}\left(GetElem.getElem\left(q,1\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)=\mathrm{append}\left(\mathrm{replicate}\left(\mathrm{length}\left(as\right),0\right),\mathrm{cons}\left(1,\mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(q\right),\mathrm{some}\left(GetElem.getElem\left(q,1\right)\right),\mathrm{none}\left(\right)\right),0\right),after\right)\right)\right)\right)\wedge \left(\forall k\in \mathbb{N},\left(3\le k\wedge k\le 6\right)\Rightarrow \mathrm{getD}\left(\mathrm{ite}\left(k<List.length\left(t\right),\mathrm{some}\left(GetElem.getElem\left(t,k\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{getD}\left(\mathrm{ite}\left(k<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,k\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\wedge \left(\left(\left(\left(\left(\left(\left(\left(\left(\mathrm{digit}\left(v,10\right)=1\wedge \mathrm{digit}\left(u,10\right)=0\right)\wedge \mathrm{digit}\left(u,11\right)=0\right)\wedge \mathrm{digit}\left(u,12\right)=0\right)\wedge \mathrm{digit}\left(u,13\right)=0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,3\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{digit}\left(u,1\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(4<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,4\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{toNat}\left((\mathrm{digit}\left(v,12\right)==1)\right),\mathbb{Z}\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(5<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,5\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{toNat}\left(Bool.or\left(\mathrm{decide}\left(\mathrm{digit}\left(u,16\right)<0\right),Bool.and\left((\mathrm{digit}\left(u,16\right)==0),(\mathrm{digit}\left(u,2\right)==1)\right)\right)\right),\mathbb{Z}\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(6<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,6\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{toNat}\left(Bool.or\left(\mathrm{decide}\left(\mathrm{digit}\left(u,17\right)<0\right),Bool.and\left((\mathrm{digit}\left(u,17\right)==0),(\mathrm{digit}\left(u,3\right)==1)\right)\right)\right),\mathbb{Z}\right)\right)\wedge \left(\mathrm{digit}\left(v,12\right)=1\vee \left(\left(\left(\mathrm{digit}\left(v,12\right)=0\wedge \mathrm{getD}\left(\mathrm{ite}\left(5<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,5\right)\right),\mathrm{none}\left(\right)\right),0\right)=1\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(6<List.length\left(v\right),\mathrm{some}\left(GetElem.getElem\left(v,6\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(u\right),\mathrm{some}\left(GetElem.getElem\left(u,2\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\right)\right)\right)\right))\left(\lambda q:\mathrm{List}\left(\mathbb{Z}\right)k:\mathbb{N}\mapsto \mathrm{getD}\left(\mathrm{ite}\left(k<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(q\right),\mathrm{some}\left(GetElem.getElem\left(q,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(q\right),\mathrm{some}\left(GetElem.getElem\left(q,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right),k\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every path from mode zero to mode four whose final bad flag is zero has a selected transition from mode zero to mode one. Its preceding path is the unmarked lower tail. Input and output streams agree after the selected transition. The two preceding signed digits vanish in both streams. The selected input digit is one. Its output is either one, or zero with input negative phase one, output negative phase zero and an unbroken lower negation flag. Marker parity, retention and both phases at the terminal state are exactly the snapshots saved on the selected transition.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPathSelection.marked_path_selection
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedSuffixAgreement