Class Preservation and Charge Monotonicity

Abstract

Tight legal palindrome cuts preserve class S and do not increase the literal signed-digit charge.

Theorem 1.1 (The tight-cut transition law).

$$\forall n\in \mathbb{N},\forall j\in \mathbb{N},\left(\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)\wedge \mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right)=\mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(j+1,2\right),\mathbb{Z}\right)\right)+1\right)\Rightarrow \left(\mathrm{classS}\left(j\right)\wedge \mathrm{signedDigitCharge}\left(j\right)\le \mathrm{signedDigitCharge}\left(n\right)\right)$$

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

Source. Repository-derived.

Commentary.

A cut is tight when the minimum signed weight of the rounded half drops by exactly one. Complete path realization gives an accepting base path. The class-escape potential bound zero excludes the invalid-output mode, since its f charge is one. In the valid-output mode the q+3f bound with terminal phase gives Q(j)≤Q(n). The path’s output signed expansion has the literal rounded-half value and class spacing; equal-length zero padding and nonadjacent uniqueness identify it with the triple-binary expansion defining class S. div denotes natural integer quotient, and Nat.sub denotes truncated natural subtraction.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/TightCutCharge.tight_cut_class_and_Q
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseArithmetic
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseClassStreams
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/CutRepresentation