Class Spacing of Transducer Outputs

Abstract

Both signed streams of any path ending at a valid charge-mode goal forbid opposite digits at distance two.

Definition 1.1 (Digit memories and persistent class flag).

$$\forall i\in \mathbb{N},\mathrm{classRowCheck}\left(i\right)=\mathrm{all}\left(e:\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{decide}\left(\left(\left(\mathrm{getD}\left(\mathrm{ite}\left(11<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),11\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{getD}\left(\mathrm{ite}\left(10<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right),10\right)\right),\mathrm{none}\left(\right)\right),0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(13<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),13\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{getD}\left(\mathrm{ite}\left(12<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right),12\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(10<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),10\right)\right),\mathrm{none}\left(\right)\right),0\right)\cdot \mathrm{getD}\left(\mathrm{ite}\left(11<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right),11\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne \mathrm{neg}\left(1\right)\right)\wedge \left(\mathrm{getD}\left(\mathrm{ite}\left(18<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),18\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\Rightarrow \left(\mathrm{getD}\left(\mathrm{ite}\left(18<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right),18\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\wedge \mathrm{getD}\left(\mathrm{ite}\left(12<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),12\right)\right),\mathrm{none}\left(\right)\right),0\right)\cdot \mathrm{getD}\left(\mathrm{ite}\left(13<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(i\right)\right),13\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne \mathrm{neg}\left(1\right)\right)\right)\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{baseTable}\left(i\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseClassStreams.classRowCheck (✓ std3).

Source. Repository-derived.

Commentary.

The checker tests both shifted digit memories, immediate rejection of an input violation, and backward propagation of the output violation flag on every base edge.

Theorem 1.2 (No opposite signs two digit positions apart).

$$\forall output\in \mathrm{Bool},\forall s\in \mathrm{Fin}\left(1492\right),\forall t\in \mathrm{Fin}\left(1492\right),\forall xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),t\in \mathrm{accept}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right),s,t,xs\right),\mathrm{IsChain}\left(\mathrm{zip}\left(\mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\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(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right),\mathrm{tail}\left(\mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\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(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right)\right),a:\mathbb{Z}\times \mathbb{Z}\mapsto b:\mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{fst}\left(a\right)\cdot \mathrm{snd}\left(b\right)\ne \mathrm{neg}\left(1\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

output selects target component 12 when true and component 10 when false. Zip the digit stream with its tail. Consecutive pairs (a,b) and (b,c) satisfy a times c unequal to minus one. Together with the sparse signed-digit property, this is the class S condition that consecutive nonzero digits of opposite signs have gap at least three. The input transducer rejects violations immediately. The output stores a persistent violation flag, which is zero at every charge-mode accepting goal. Induction propagates that flag backwards and reconstructs each triple from the two digit memories. This result does not assert completeness for actual palindrome cuts.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseClassStreams.base_path_class_spacing
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseClassStreams.classRowCheck
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams