Arithmetic Meaning of the Signed-Digit Charge

Abstract

The q weights count position charges and successive nonzero-sign changes exactly.

Definition 1.1 (Signed-stream charge with incoming memory).

$$(\forall par\in \mathbb{Z},\forall previous\in \mathbb{Z},\mathrm{digitStreamCharge}\left(par,previous,[]\right)=0)\wedge (\forall par\in \mathbb{Z},\forall previous\in \mathbb{Z},\forall d\in \mathbb{Z},\forall ds\in \mathrm{List}\left(\mathbb{Z}\right),\mathrm{digitStreamCharge}\left(par,previous,\mathrm{cons}\left(d,ds\right)\right)=\mathrm{ite}\left(d=0,0,1+2\cdot par+\mathrm{cast}\left(\mathrm{toNat}\left(Bool.and\left((previous!=0),(previous!=d)\right)\right),\mathbb{Z}\right)\right)+\mathrm{digitStreamCharge}\left(1-par,\mathrm{ite}\left(d=0,previous,d\right),ds\right))$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic.digitStreamCharge (✓ std3).

Source. Repository-derived.

Commentary.

A zero digit contributes nothing and preserves the previous nonzero sign. A nonzero digit contributes 1 + 2 par and an extra unit when its sign differs from a nonzero incoming sign. The parity switches after every digit. This is the position-weight and sign-change part of Q, without its terminal endpoint-parity correction. The Boolean indicators are converted to natural numbers and then embedded in the integers.

Definition 1.2 (Literal last-sign and charge updates).

$$\forall i\in \mathbb{N},\mathrm{chargeRowCheck}\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(1<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),1\right)\right),\mathrm{none}\left(\right)\right),0\right)=1-\mathrm{getD}\left(\mathrm{ite}\left(1<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),1\right)\right),\mathrm{none}\left(\right)\right),0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(16<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),16\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{ite}\left(\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)=0,\mathrm{getD}\left(\mathrm{ite}\left(16<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),16\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(\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)\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(17<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),17\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{ite}\left(\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)=0,\mathrm{getD}\left(\mathrm{ite}\left(17<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),17\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(\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)\right)\right)\wedge \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(e\right)\right)\right)=\mathrm{ite}\left(\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)=0,0,1+2\cdot \mathrm{getD}\left(\mathrm{ite}\left(1<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),1\right)\right),\mathrm{none}\left(\right)\right),0\right)+\mathrm{cast}\left(\mathrm{toNat}\left(Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(17<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),17\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0),(\mathrm{getD}\left(\mathrm{ite}\left(17<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),17\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(\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))\right)\right),\mathbb{Z}\right)\right)-\mathrm{ite}\left(\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)=0,0,1+2\cdot \mathrm{getD}\left(\mathrm{ite}\left(1<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),1\right)\right),\mathrm{none}\left(\right)\right),0\right)+\mathrm{cast}\left(\mathrm{toNat}\left(Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(16<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),16\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0),(\mathrm{getD}\left(\mathrm{ite}\left(16<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),16\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(\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))\right)\right),\mathbb{Z}\right)\right)\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{baseTable}\left(i\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic.chargeRowCheck (✓ std3).

Source. Repository-derived.

Commentary.

Each base edge flips the position parity, updates each most recent nonzero sign exactly when a nonzero digit is emitted, and gives q the difference of the two literal position-and-sign-change contributions.

Theorem 1.3 (The literal position and sign-change sum).

$$\forall ds\in \mathrm{List}\left(\mathbb{Z}\right),\forall p\in \mathbb{N},\forall previous\in \mathbb{Z},\mathrm{digitStreamCharge}\left(\mathrm{cast}\left(\mathrm{mod}\left(p,2\right),\mathbb{Z}\right),previous,ds\right)=\mathrm{cast}\left(\mathrm{sum}\left(\mathrm{map}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto 1+2\cdot \mathrm{mod}\left(\mathrm{snd}\left(z\right),2\right),\mathrm{filter}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto (\mathrm{fst}\left(z\right)!=0),\mathrm{zipIdx}\left(ds,p\right)\right)\right)\right),\mathbb{Z}\right)+\mathrm{cast}\left(\mathrm{length}\left(\mathrm{filter}\left(z:(\mathbb{Z}\times \mathbb{N})\times (\mathbb{Z}\times \mathbb{N})\mapsto (\mathrm{fst}\left(\mathrm{fst}\left(z\right)\right)!=\mathrm{fst}\left(\mathrm{snd}\left(z\right)\right)),\mathrm{zip}\left(\mathrm{filter}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto (\mathrm{fst}\left(z\right)!=0),\mathrm{zipIdx}\left(ds,p\right)\right),\mathrm{tail}\left(\mathrm{filter}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto (\mathrm{fst}\left(z\right)!=0),\mathrm{zipIdx}\left(ds,p\right)\right)\right)\right)\right)\right),\mathbb{Z}\right)+Option.elim\left(\mathrm{ite}\left(\mathrm{filter}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto (\mathrm{fst}\left(z\right)!=0),\mathrm{zipIdx}\left(ds,p\right)\right)=[],\mathrm{none}\left(\right),\mathrm{some}\left(List.head\left(\mathrm{filter}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto (\mathrm{fst}\left(z\right)!=0),\mathrm{zipIdx}\left(ds,p\right)\right)\right)\right)\right),0,z:\mathbb{Z}\times \mathbb{N}\mapsto \mathrm{cast}\left(\mathrm{toNat}\left(Bool.and\left((previous!=0),(previous!=\mathrm{fst}\left(z\right))\right)\right),\mathbb{Z}\right)\right)$$

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

Source. Repository-derived.

Commentary.

Enumerate the digits from natural position p and discard the zeros. The charge is the sum of 1 + 2(i mod 2) over the surviving positions, plus the number of changes between successive surviving signs, plus the change from a nonzero incoming sign to the first surviving sign. An empty nonzero list has zero incoming correction. mod is natural remainder; Option.elim is zero for none and applies the displayed function for some.

Theorem 1.4 (q is the difference of the two stream charges).

$$\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),\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(\mathrm{snd}\left(a\right)\right),p\right)=\mathrm{digitStreamCharge}\left(\mathrm{getD}\left(\mathrm{ite}\left(1<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),1\right)\right),\mathrm{none}\left(\right)\right),0\right),\mathrm{getD}\left(\mathrm{ite}\left(17<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),17\right)\right),\mathrm{none}\left(\right)\right),0\right),\mathrm{pathOutputs}\left(\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(12<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),12\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right)-\mathrm{digitStreamCharge}\left(\mathrm{getD}\left(\mathrm{ite}\left(1<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),1\right)\right),\mathrm{none}\left(\right)\right),0\right),\mathrm{getD}\left(\mathrm{ite}\left(16<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),16\right)\right),\mathrm{none}\left(\right)\right),0\right),\mathrm{pathOutputs}\left(\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(10<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),10\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right)$$

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

Source. Repository-derived.

Commentary.

This equality holds for every finite path and either acceptance mode, without requiring its endpoints to be sources or goals. State component 1 is the current position parity; components 16 and 17 are the latest nonzero signs of the two streams. Every table edge updates these memories and carries the difference of the contributions. Path induction then reconstructs the entire charge. Components 10 and 12 of the successor state are the emitted input and output signed digits.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic.base_path_charge_reconstruction
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic.chargeRowCheck
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic.digitStreamCharge
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic.digit_stream_charge_formula
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams