Complete Representation of Palindrome Cuts

Abstract

Every actual palindrome cut from class S is represented by the complete finite transducer.

Definition 1.1 (The literal signed-digit class S).

$$\forall n\in \mathbb{N},\mathrm{classS}\left(n\right)\iff \left(\exists h\in \mathbb{N},3\cdot \mathrm{div}\left(n+1,2\right)<2^{h+1}\wedge \left(\forall i\in \mathrm{Fin}\left(h\right),\forall j\in \mathrm{Fin}\left(h\right),\left(\left(\left(\left(\mathrm{val}\left(i\right)<\mathrm{val}\left(j\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{val}\left(i\right)<List.length\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right),\mathrm{val}\left(i\right)\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{val}\left(j\right)<List.length\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right),\mathrm{val}\left(j\right)\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\right)\wedge \left(\forall k\in \mathbb{N},\left(\mathrm{val}\left(i\right)<k\wedge k<\mathrm{val}\left(j\right)\right)\Rightarrow \mathrm{getD}\left(\mathrm{ite}\left(k<List.length\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right),k\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{val}\left(i\right)<List.length\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right),\mathrm{val}\left(i\right)\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{val}\left(j\right)<List.length\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{tripleSignedDigits}\left(\mathrm{div}\left(n+1,2\right),h\right),\mathrm{val}\left(j\right)\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\Rightarrow 3\le Nat.sub\left(\mathrm{val}\left(j\right),\mathrm{val}\left(i\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/CutRepresentation.classS (✓ std3).

Source. Repository-derived.

Commentary.

Class S consists of endpoints whose rounded-half nonadjacent expansion has a gap of at least three between consecutive nonzero digits of different signs. The existential length has an explicit bound making the triple-binary expansion complete. Indices i and j range over Fin h; intermediate indices k range over the naturals. Entry means option lookup with default zero, div and mod mean natural integer quotient and remainder, and Nat.sub is truncated natural subtraction.

Theorem 1.2 (Literal legal cuts give accepting paths).

$$\forall n\in \mathbb{N},\forall j\in \mathbb{N},\forall minimumLength\in \mathbb{N},\left(\left(\mathrm{classS}\left(n\right)\wedge j<n\right)\wedge \mathrm{Palindrome}\left(\mathrm{ofFn}\left(i:\mathrm{Fin}\left(Nat.sub\left(n,j\right)\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(j+\mathrm{val}\left(i\right)\right)\right)\right)\right)\Rightarrow \left(\exists charge\in \mathrm{Bool},\exists s\in \mathrm{Fin}\left(1492\right),\exists t\in \mathrm{Fin}\left(1492\right),\exists xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\left(\left(\left(\left(\left(\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)\wedge \mathrm{Nonempty}\left(\mathrm{Path}\left(\mathrm{baseAutomaton}\left(charge\right),s,t,xs\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)\wedge minimumLength\le \mathrm{length}\left(xs\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every nonempty palindromic suffix from j to n with n in class S, an accepting path records both endpoint parities and both shifted endpoint values. Either acceptance mode may occur: true has a valid output class, and false records an output class violation. The proof builds the bit-relation path from the actual dyadic palindrome radius, pads it by zero bits, supplies complete nonadjacent signed expansions, derives distance-two input spacing from the consecutive-sign condition, and performs the carry realization. The accepting path has at least the requested minimum length. This theorem supplies complete legal-cut representation; tightness is used separately to exclude the class-violation mode.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/CutRepresentation.classS
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/CutRepresentation.cut_representation_completeness
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseDigitRealization
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic