Arithmetic Meaning of the Base Transducer

Abstract

The f charges on accepted paths equal the signed-weight difference of the encoded rounded halves.

Theorem 1.1 (Path charge is the exact signed-weight difference).

$$\forall charge\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),\left(s\in \mathrm{start}\left(\mathrm{baseAutomaton}\left(charge\right)\right)\wedge t\in \mathrm{accept}\left(\mathrm{baseAutomaton}\left(charge\right)\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(charge\right),s,t,xs\right),\mathrm{pathCharge}\left(\lambda [\mathrm{Fin}\left(1492\right)]a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}[\mathrm{Fin}\left(1492\right)]\mapsto \mathrm{fst}\left(a\right),p\right)=\mathrm{cast}\left(\mathrm{signedWeight}\left(\mathrm{foldr}\left(a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto x:\mathbb{Z}\mapsto \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)+2\cdot x,0,xs\right)+\mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right),2\right)\right),\mathrm{none}\left(\right)\right),0\right)\right),\mathbb{Z}\right)-\mathrm{cast}\left(\mathrm{signedWeight}\left(\mathrm{foldr}\left(a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto x:\mathbb{Z}\mapsto \mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)+2\cdot x,0,xs\right)+\mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right),3\right)\right),\mathrm{none}\left(\right)\right),0\right)\right),\mathbb{Z}\right)\right)$$

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

Source. Repository-derived.

Commentary.

The third and fourth edge coordinates encode successive binary digits, least significant first, above the endpoint’s bit zero. Folding a + 2 x reconstructs the shifted integer. Source components 2 and 3 supply the fixed bit-zero parities, so adding them reconstructs the two rounded halves. The carry identities and the forced even remainder after a nonzero signed digit give the signed-weight change at each edge; path induction telescopes it. cast denotes the natural-to-integer embedding. This theorem identifies f weights and does not assert that all legal palindrome cuts have already been represented by accepted paths.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseArithmetic.base_path_signed_weight_difference
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseCertificates
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SignedWeight