Odd Cuts in Even Tight Paths

Abstract

Every cut in an even tight path from an even endpoint to zero has odd length.

Theorem 1.1 (The path obstruction).

$$\forall n\in \mathbb{N},\forall cuts\in \mathrm{List}\left(\mathbb{N}\right),\left(\left(\left(\left(\mathrm{classS}\left(n\right)\wedge \mathrm{mod}\left(n,2\right)=0\right)\wedge \mathrm{mod}\left(\mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right),2\right)=0\right)\wedge \mathrm{ite}\left(\mathrm{cons}\left(n,cuts\right)=[],\mathrm{none},\mathrm{some}\left(List.getLast\left(\mathrm{cons}\left(n,cuts\right)\right)\right)\right)=\mathrm{some}\left(0\right)\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{IsChain}\left(\mathrm{cons}\left(n,cuts\right),s:\mathbb{N}\mapsto t:\mathbb{N}\mapsto \mathrm{mod}\left(s,2\right)\ne \mathrm{mod}\left(t,2\right)\right)$$

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

Source. Repository-derived.

Commentary.

The initial endpoint belongs to class S and is even, and its rounded-half signed weight is even. The descending path ends at zero and every cut is a literal palindrome whose signed weight drops by one. Induction makes the number of cuts equal to the initial signed weight and balances endpoint parity with the count of equal-parity edges. The one-even-cut bound then forces that count to zero, so all endpoint parities differ. div denotes natural integer quotient and Nat.sub denotes truncated natural subtraction. The last-option expression is none for an empty list and some(List.getLast(…)) otherwise; the nonempty proof argument is implicit.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/EvenTightPaths.even_tight_path_has_only_odd_cuts
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/TightPathEvenCuts