Exact Stream of a Marked Prefix

Abstract

Literal marked prefixes determine the ordered signed stream.

Theorem 1.1 (Padded stream and exact lower tail).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall p\in \mathbb{N},\forall T\in \mathbb{Z},\forall ds\in \mathrm{List}\left(\mathbb{Z}\right),\left(\left(\left(\left(\mathrm{markedPrefix}\left(n,m,p,T\right)\wedge \left(\forall z\in \mathbb{Z},z\in ds\Rightarrow \left(z=\mathrm{neg}\left(1\right)\vee \left(z=0\vee z=1\right)\right)\right)\right)\wedge \mathrm{IsChain}\left(ds,\lambda a:\mathbb{Z}b:\mathbb{Z}\mapsto a=0\vee b=0\right)\right)\wedge \mathrm{foldr}\left(\lambda z:\mathbb{Z}x:\mathbb{Z}\mapsto z+2\cdot x,0,ds\right)=2\cdot \mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right)\wedge p+3\cdot m+2\le \mathrm{length}\left(ds\right)\right)\Rightarrow \left(\exists lower\in \mathrm{List}\left(\mathbb{Z}\right),\exists k\in \mathbb{N},\left(\left(\left(\left(\mathrm{length}\left(lower\right)=p+1\wedge \mathrm{foldr}\left(\lambda z:\mathbb{Z}x:\mathbb{Z}\mapsto z+2\cdot x,0,lower\right)=2\cdot T\right)\wedge \left(\forall i\in \mathbb{N},\mathrm{getD}\left(\mathrm{ite}\left(i<List.length\left(lower\right),\mathrm{some}\left(GetElem.getElem\left(lower,i\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\Rightarrow i+2\le p\right)\right)\wedge ds=\mathrm{append}\left(\mathrm{append}\left(lower,\mathrm{flatten}\left(\mathrm{replicate}\left(m,[1,0,0]\right)\right)\right),\mathrm{replicate}\left(k+1,0\right)\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(\mathrm{reverse}\left(\mathrm{append}\left([0,0],lower\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{reverse}\left(\mathrm{append}\left([0,0],lower\right)\right),0\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(\mathrm{reverse}\left(\mathrm{append}\left([0,0],lower\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{reverse}\left(\mathrm{append}\left([0,0],lower\right)\right),1\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)$$

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

Source. Repository-derived.

Commentary.

Any nonadjacent signed expansion of twice the rounded half-endpoint, of length at least p+3m+2, consists of a lower tail of length p+1, then m blocks [1,0,0], then at least one leading zero. The lower tail evaluates to twice T and its nonzero positions i satisfy i+2 at most p. Adding the two initial zero memories gives two zero digits immediately before the selected marker, including p=0. The proof constructs the literal expansion, evaluates the geometric block, and applies nonadjacent digit uniqueness. div is natural integer quotient; option lookups have default zero.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixExpansion.marked_prefix_expansion
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/CanonicalSignedDigits
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixArithmetic