Marked Suffix Agreement

Abstract

A good terminal marker flag forces higher input and output coefficients to agree.

Theorem 1.1 (Agreement above the selected marker).

$$\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)=1\vee \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)=2\vee \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)=3\vee \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)=4\right)\right)\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(\left(\mathrm{getD}\left(\mathrm{ite}\left(7<List.length\left(s\right),\mathrm{some}\left(GetElem.getElem\left(s,7\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\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(10<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),10\right)\right),\mathrm{none}\left(\right)\right),0\right),p\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{getD}\left(\mathrm{ite}\left(12<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),12\right)\right),\mathrm{none}\left(\right)\right),0\right),p\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(s\right),\mathrm{some}\left(GetElem.getElem\left(s,k\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The starting marker has already selected its lowest positive digit, so its mode is one, two, three or four. If the final bad flag is zero, every later input coefficient equals its output coefficient and the starting bad flag is zero. Slots three through six, which store the marker parity, retention flag and the two tail phases, keep their starting values throughout the path.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedSuffixAgreement.marked_suffix_agreement
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization