Arithmetic Rigidity of a Marked Prefix

Abstract

The marked prefix survives tight odd palindromic cuts with a corrected charge inequality.

Theorem 1.1 (Retained and removed prefix alternatives).

$$\forall n\in \mathbb{N},\forall j\in \mathbb{N},\forall m\in \mathbb{N},\forall p\in \mathbb{N},\forall T\in \mathbb{Z},\left(\left(\left(\left(\left(\left(0<m\wedge \mathrm{classS}\left(n\right)\right)\wedge \mathrm{markedPrefix}\left(n,m,p,T\right)\right)\wedge j<n\right)\wedge \mathrm{mod}\left(n,2\right)\ne \mathrm{mod}\left(j,2\right)\right)\wedge \mathrm{Palindrome}\left(\mathrm{ofFn}\left(\lambda 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(\left(\exists U\in \mathbb{Z},\mathrm{markedPrefix}\left(j,m,p,U\right)\wedge \mathrm{cast}\left(\mathrm{signedDigitCharge}\left(j\right),\mathbb{Z}\right)-\mathrm{cast}\left(\mathrm{signedDigitCharge}\left(n\right),\mathbb{Z}\right)+(1+2\cdot \mathrm{cast}\left(\mathrm{mod}\left(p,2\right),\mathbb{Z}\right)-1)\cdot (\mathrm{ite}\left(2\cdot U-\mathrm{cast}\left(\mathrm{mod}\left(j,2\right),\mathbb{Z}\right)<0,1,0\right)-\mathrm{ite}\left(2\cdot T-\mathrm{cast}\left(\mathrm{mod}\left(n,2\right),\mathbb{Z}\right)<0,1,0\right))\le 0\right)\vee \left(\left(\left(\mathrm{markedPrefix}\left(j,Nat.sub\left(m,1\right),p+3,\mathrm{neg}\left(T\right)\right)\wedge \mathrm{ite}\left(2\cdot T-\mathrm{cast}\left(\mathrm{mod}\left(n,2\right),\mathbb{Z}\right)<0,1,0\right)=1\right)\wedge \mathrm{ite}\left(2\cdot \mathrm{neg}\left(T\right)-\mathrm{cast}\left(\mathrm{mod}\left(j,2\right),\mathbb{Z}\right)<0,1,0\right)=0\right)\wedge \mathrm{cast}\left(\mathrm{signedDigitCharge}\left(j\right),\mathbb{Z}\right)-\mathrm{cast}\left(\mathrm{signedDigitCharge}\left(n\right),\mathbb{Z}\right)+1+2\cdot \mathrm{cast}\left(\mathrm{mod}\left(p,2\right),\mathbb{Z}\right)+1\le 0\right)\right)$$

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

Source. Repository-derived.

Commentary.

A tight palindromic cut between endpoints of opposite parity preserves every positive digit of a literal marked prefix, or removes precisely its lowest digit. In the retained case, the lower tail may change and the difference of signed-digit charges is bounded after correcting by the difference of lower-tail phases. In the removed case, the new lower tail is the exact negative of the old one, with input phase one and output phase zero. The position weight is 1+2(p mod 2), and the phase is the indicator of 2T minus the endpoint parity being negative. The selected digit position and phase snapshots are reconstructed from the path before the marker; the terminal potential then supplies the charge inequality. div and mod denote natural integer quotient and remainder, and Nat.sub denotes truncated natural subtraction.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixRigidity.marked_prefix_rigidity_and_charge
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseArithmetic
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BasePositionMemory
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/CutRepresentation
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedBaseProjection
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedInputAnnotation
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPathSelection
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixExpansion
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SignedDigitPhase
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/UnmarkedFlipSemantics