Tight Palindromic Factorizations

Abstract

The signed-weight lower bound is attained precisely when the prefix can be reduced to zero through tight palindrome cuts.

Theorem 1.1 (Equality is equivalent to a tight cut path).

$$\forall n\in \mathbb{N},\mathrm{PL}\left(\mathrm{ofFn}\left(i:\mathrm{Fin}\left(n\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(i\right)\right)\right)\right)=\mathrm{signedWeight}\left(\mathrm{cast}\left(Nat.div\left(n+1,2\right),\mathbb{Z}\right)\right)\iff \left(\exists cuts\in \mathrm{List}\left(\mathbb{N}\right),\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)\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(Nat.div\left(s+1,2\right),\mathbb{Z}\right)\right)=\mathrm{signedWeight}\left(\mathrm{cast}\left(Nat.div\left(t+1,2\right),\mathbb{Z}\right)\right)+1\right)\right)$$

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

Source. Repository-derived.

Commentary.

The list starts at the prefix endpoint n and ends at zero. Each successive pair decreases the endpoint, removes a nonempty palindromic suffix, and lowers the signed weight of the rounded half by exactly one. An optimal factorization supplies such a path when equality holds; conversely, a tight path constructs a factorization meeting the lower bound. Nat.sub denotes truncated natural subtraction and Nat.div denotes natural integer division. 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/TightFactorization.tight_factorization_iff
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SignedCutLowerBound