Unmarked Flip Semantics

Abstract

The unmarked flip flag records pointwise negation of the lower signed streams.

Theorem 1.1 (Exact meaning of the persistent flip flag).

$$\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),\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)=0\Rightarrow \left(\mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(t\right),\mathrm{some}\left(GetElem.getElem\left(t,2\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\iff \left(\mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(s\right),\mathrm{some}\left(GetElem.getElem\left(s,2\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\wedge \left(\forall z\in \mathbb{Z}\times \mathbb{Z},z\in \mathrm{zip}\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{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)\Rightarrow \mathrm{fst}\left(z\right)+\mathrm{snd}\left(z\right)=0\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

A path ending in marker mode zero has remained unmarked throughout. Its final flip flag is nonzero exactly when the starting flag is nonzero and every emitted input/output coefficient pair sums to zero. The two streams have the same length because each transition emits one coefficient on each side. Starting with flip flag one therefore records exact negation of the whole lower signed tail.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/UnmarkedFlipSemantics.unmarked_path_flip_semantics
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization