At Most One Tight Even Cut

Abstract

A tight palindrome-cut path has at most one even-length deletion.

Theorem 1.1 (The path obstruction).

$$\forall n\in \mathbb{N},\forall cuts\in \mathrm{List}\left(\mathbb{N}\right),\left(\mathrm{classS}\left(n\right)\wedge \mathrm{IsChain}\left(\mathrm{cons}\left(n,cuts\right),s:\mathbb{N}\mapsto t:\mathbb{N}\mapsto \left(t<s\wedge \mathrm{Palindrome}\left(\mathrm{ofFn}\left(i:\mathrm{Fin}\left(Nat.sub\left(s,t\right)\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(t+\mathrm{val}\left(i\right)\right)\right)\right)\right)\wedge \mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(s+1,2\right),\mathbb{Z}\right)\right)=\mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(t+1,2\right),\mathbb{Z}\right)\right)+1\right)\right)\Rightarrow \mathrm{length}\left(\mathrm{filter}\left(e:\mathbb{N}\times \mathbb{N}\mapsto (\mathrm{mod}\left(\mathrm{fst}\left(e\right),2\right)==\mathrm{mod}\left(\mathrm{snd}\left(e\right),2\right)),\mathrm{zip}\left(\mathrm{cons}\left(n,cuts\right),cuts\right)\right)\right)\le 1$$

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

Source. Repository-derived.

Commentary.

The path is any finite descending list of literal tight palindrome cuts beginning in class S. Its even cuts are exactly the pairs with equal endpoint parity. An even palindrome has length two. Signed-weight arithmetic and the source letters force a tight even cut to start at an odd integer at least five with odd rounded half; its successor has positive dyadic valuation. Class preservation and lowest-position monotonicity keep that valuation positive until zero, excluding any further even cut. Induction counts the exceptional first even cut. The statement does not require the path to end at zero. div denotes natural integer quotient and Nat.sub denotes truncated natural subtraction.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/TightPathEvenCuts.tight_path_at_most_one_even_cut
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/TightCutCharge
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/TightCutLowestPosition