Literal Endpoint Charge

Abstract

Accepted q paths have the literal arithmetic charge Q(j) - Q(n).

Definition 1.1 (The nonadjacent digit formula).

$$\forall X\in \mathbb{N},\forall h\in \mathbb{N},\mathrm{tripleSignedDigits}\left(X,h\right)=\mathrm{ofFn}\left(i:\mathrm{Fin}\left(h\right)\mapsto \mathrm{cast}\left(\mathrm{mod}\left(\mathrm{div}\left(3\cdot X,2^{\mathrm{val}\left(i\right)+1}\right),2\right),\mathbb{Z}\right)-\mathrm{cast}\left(\mathrm{mod}\left(\mathrm{div}\left(X,2^{\mathrm{val}\left(i\right)+1}\right),2\right),\mathbb{Z}\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.tripleSignedDigits (✓ std3).

Source. Repository-derived.

Commentary.

Digits are in increasing order of position: digit i is bit i+1 of 3X minus bit i+1 of X. div and mod are natural integer quotient and remainder. The chosen length is a separate parameter.

Definition 1.2 (Q from positions, sign changes and endpoint parity).

$$\forall n\in \mathbb{N},\mathrm{signedDigitCharge}\left(n\right)=\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(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),\log \left(2,3\cdot \mathrm{div}\left(n+1,2\right)\right)+1\right),0\right)\right)\right)\right)+\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(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),\log \left(2,3\cdot \mathrm{div}\left(n+1,2\right)\right)+1\right),0\right)\right),\mathrm{tail}\left(\mathrm{filter}\left(z:\mathbb{Z}\times \mathbb{N}\mapsto (\mathrm{fst}\left(z\right)!=0),\mathrm{zipIdx}\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),\log \left(2,3\cdot \mathrm{div}\left(n+1,2\right)\right)+1\right),0\right)\right)\right)\right)\right)\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(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),\log \left(2,3\cdot \mathrm{div}\left(n+1,2\right)\right)+1\right),0\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(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),\log \left(2,3\cdot \mathrm{div}\left(n+1,2\right)\right)+1\right),0\right)\right)\right)\right)\right),0,z:\mathbb{Z}\times \mathbb{N}\mapsto \mathrm{toNat}\left(((\mathrm{mod}\left(n,2\right)==1)!=\mathrm{decide}\left(\mathrm{fst}\left(z\right)<0\right))\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.signedDigitCharge (✓ std3).

Source. Repository-derived.

Commentary.

Take X = div(n+1,2) and h = log(2,3X)+1. Enumerate its nonadjacent digits, discard zeros, and sum the weights 1+2(i mod 2), consecutive sign changes, and endpoint parity XOR the negativity of the first surviving sign. The last indicator is zero when no digit survives. Option.elim returns the displayed default for none and applies its function for some.

Definition 1.3 (Endpoint and first-sign memory checker).

$$\forall i\in \mathbb{N},\mathrm{memoryRowCheck}\left(i\right)=\mathrm{all}\left(\lambda 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(2<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),2\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{getD}\left(\mathrm{ite}\left(2<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),2\right)\right),\mathrm{none}\left(\right)\right),0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(3<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),3\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{getD}\left(\mathrm{ite}\left(3<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),3\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(14<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),14\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{ite}\left(\mathrm{getD}\left(\mathrm{ite}\left(14<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),14\right)\right),\mathrm{none}\left(\right)\right),0\right)=0,\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),\mathrm{getD}\left(\mathrm{ite}\left(14<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),14\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(15<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),15\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{ite}\left(\mathrm{getD}\left(\mathrm{ite}\left(15<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),15\right)\right),\mathrm{none}\left(\right)\right),0\right)=0,\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),\mathrm{getD}\left(\mathrm{ite}\left(15<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),15\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{baseTable}\left(i\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.memoryRowCheck (✓ std3).

Source. Repository-derived.

Commentary.

Every outgoing edge must preserve the two endpoint parities and update both first-nonzero-sign memories only while their incoming memory is zero. This Boolean checker is reused by the charge identification and by the lowest-position arithmetic interpretation.

Theorem 1.4 (Exact charge of every accepting path).

$$\forall n\in \mathbb{N},\forall j\in \mathbb{N},\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(\mathrm{true}\right),s,t,xs\right),\left(\left(\left(\left(\left(s\in \mathrm{start}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right)\right)\wedge t\in \mathrm{accept}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right)\right)\right)\wedge \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)=\mathrm{cast}\left(\mathrm{mod}\left(n,2\right),\mathbb{Z}\right)\right)\wedge \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)=\mathrm{cast}\left(\mathrm{mod}\left(j,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}x:\mathbb{Z}\mapsto \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)+2\cdot x,0,xs\right)=\mathrm{cast}\left(\mathrm{div}\left(n,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}x:\mathbb{Z}\mapsto \mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)+2\cdot x,0,xs\right)=\mathrm{cast}\left(\mathrm{div}\left(j,2\right),\mathbb{Z}\right)\right)\Rightarrow \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{baseOffset}\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(t\right)\right)\right)\right)=\mathrm{cast}\left(\mathrm{signedDigitCharge}\left(j\right),\mathbb{Z}\right)-\mathrm{cast}\left(\mathrm{signedDigitCharge}\left(n\right),\mathbb{Z}\right)$$

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

Source. Repository-derived.

Commentary.

For an accepting charge-mode path whose source parities and binary folds encode n and j, the sum of q edge charges plus the terminal phase correction is Q(j)-Q(n). Component 2 or 3 of the source is the endpoint parity; the last two components of an edge label are bits of the integer quotients div(n,2) and div(j,2). The proof checks all sign-memory transitions and identifies the padded output streams with the unique nonadjacent expansions of the rounded halves. The dummy initial zero contributes no weight.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.base_path_Q_semantics
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.memoryRowCheck
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.signedDigitCharge
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic.tripleSignedDigits
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/CanonicalSignedDigits
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/TripleBinaryDigits