Exact Sparse Off-Diagonal

Abstract

Exact Sparse Off-Diagonal

Theorem 1.1 (Exact Sparse Off-Diagonal).

$$\forall a\in \mathbb{N},\forall b\in \mathbb{N},\left(\left(\left(0<a\wedge \mathrm{mod}\left(a,2\right)=1\right)\wedge \mathrm{mod}\left(b,2\right)=1\right)\wedge 2\cdot a+1\le b\right)\Rightarrow \mathrm{PL}\left(\mathrm{ofFn}\left(\lambda k:\mathrm{Fin}\left(\mathrm{sum}\left(\mathrm{range}\left(a\right),i:\mathbb{N}\mapsto 2^{2\cdot b+2+3\cdot i}\right)+\mathrm{sum}\left(\mathrm{range}\left(b\right),j:\mathbb{N}\mapsto 2^{2\cdot j+1}\right)\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(k\right)\right)\right)\right)=a+b$$

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

Source. Repository-derived.

Commentary.

For positive odd a and odd b at least 2a+1, the prefix palindromic length of the sparse integer with binary expansion (100)^a(10)^b equals a+b. The constructed cut path attains the signed-weight lower bound.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/SparseExactOffDiagonal.offdiagonal_exact_family
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SignedCutLowerBound
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SparseFamilyUpper
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SparseInitialArithmetic