Sparse Block Upper Constructions

Abstract

Uniform four-cut and two-cut constructions for the sparse binary family.

Theorem 1.1 (The two reductions and both endpoint bits).

$$\forall p\in \mathbb{N},\forall z\in \mathbb{N},\forall c\in \mathbb{N},\forall eps\in \mathbb{N},\left(0<p\wedge eps\le 1\right)\Rightarrow \left(\left(\left(\mathrm{mod}\left(z,2\right)=0\wedge 3\le c\right)\Rightarrow \mathrm{PL}\left(\mathrm{ofFn}\left(\lambda i:\mathrm{Fin}\left(\mathrm{sum}\left(\mathrm{range}\left(p\right),\lambda s:\mathbb{N}\mapsto 2^{2\cdot c+z+2+3\cdot s}\right)+\mathrm{sum}\left(\mathrm{range}\left(c\right),\lambda j:\mathbb{N}\mapsto 2^{2\cdot j+1}\right)+eps\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(i\right)\right)\right)\right)\le \mathrm{PL}\left(\mathrm{ofFn}\left(\lambda i:\mathrm{Fin}\left(\mathrm{sum}\left(\mathrm{range}\left(Nat.sub\left(p,1\right)\right),\lambda s:\mathbb{N}\mapsto 2^{2\cdot Nat.sub\left(c,3\right)+z+9+2+3\cdot s}\right)+\mathrm{sum}\left(\mathrm{range}\left(Nat.sub\left(c,3\right)\right),\lambda j:\mathbb{N}\mapsto 2^{2\cdot j+1}\right)+eps\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(i\right)\right)\right)\right)+4\right)\wedge \left(\left(\mathrm{mod}\left(z,2\right)=1\wedge 1\le c\right)\Rightarrow \mathrm{PL}\left(\mathrm{ofFn}\left(\lambda i:\mathrm{Fin}\left(\mathrm{sum}\left(\mathrm{range}\left(p\right),\lambda s:\mathbb{N}\mapsto 2^{2\cdot c+z+2+3\cdot s}\right)+\mathrm{sum}\left(\mathrm{range}\left(c\right),\lambda j:\mathbb{N}\mapsto 2^{2\cdot j+1}\right)+eps\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(i\right)\right)\right)\right)\le \mathrm{PL}\left(\mathrm{ofFn}\left(\lambda i:\mathrm{Fin}\left(\mathrm{sum}\left(\mathrm{range}\left(Nat.sub\left(p,1\right)\right),\lambda s:\mathbb{N}\mapsto 2^{2\cdot Nat.sub\left(c,1\right)+z+5+2+3\cdot s}\right)+\mathrm{sum}\left(\mathrm{range}\left(Nat.sub\left(c,1\right)\right),\lambda j:\mathbb{N}\mapsto 2^{2\cdot j+1}\right)+eps\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(i\right)\right)\right)\right)+2\right)\right)$$

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

Source. Repository-derived.

Commentary.

The displayed sums are the literal integers with binary blocks (100) repeated p times, a gap of z zeros and (10) repeated c times. For epsilon zero or one, an even gap and at least three tail blocks permit four cuts; an odd gap and at least one tail block permit two cuts. The construction uses the exact long and short odd-palindrome radii and preserves the higher prefix. Nat.sub is truncated natural subtraction; mod is natural remainder; val is the natural value of a finite index.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/SparseBlockUpperSteps.sparse_block_upper_steps
• Dependency: D5/S1/Words/Palindromes/FridPrefix/PalindromicLength
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/OddPalindromeRadius