Signed-Weight Lower Bound for Period Doubling

Abstract

Every actual period-doubling prefix requires at least the signed weight of its rounded half.

Theorem 1.1 (A lower bound for the true prefix palindromic length).

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

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

Source. Repository-derived.

Commentary.

For an actual palindrome suffix from cut j to endpoint n, the signed binary weight of the rounded half of n is at most one more than the weight at j. The short-radius and long-radius cases use different dyadic estimates, and the even-palindrome case has length two. Strong induction along optimal suffix cuts gives the second clause for every prefix. Nat.sub is truncated natural subtraction, Nat.div is natural integer division, and cast denotes the natural-to-integer embedding.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/SignedCutLowerBound.palindromic_suffix_signed_bound
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/DyadicSignedWeight
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/EvenPalindrome
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/OddPalindromeRadius
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PalindromicLength