Signed-Digit Realization of Cut Bit Paths

Abstract

Sparse expansions turn every accepting cut-bit path into an accepting finite arithmetic path.

Theorem 1.1 (Digit rigidity and carry realization).

$$\forall n\in \mathbb{N},\forall j\in \mathbb{N},\forall r\in \mathbb{Z},\forall bits\in \mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right),\forall dns\in \mathrm{List}\left(\mathbb{Z}\right),\forall djs\in \mathrm{List}\left(\mathbb{Z}\right),\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(r\in \mathrm{ite}\left(\mathrm{mod}\left(n,2\right)=\mathrm{mod}\left(j,2\right),[6],\mathrm{ite}\left(\mathrm{mod}\left(j,2\right)<\mathrm{mod}\left(n,2\right),[1,2,0],[1,2]\right)\right)\wedge \mathrm{Nonempty}\left(\mathrm{Path}\left(cutBitAutomaton,r,0,bits\right)\right)\right)\wedge \left(\forall a\in \mathbb{N}\times \mathbb{N},a\in bits\Rightarrow \left(\mathrm{fst}\left(a\right)\le 1\wedge \mathrm{snd}\left(a\right)\le 1\right)\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{N}\times \mathbb{N}x:\mathbb{N}\mapsto \mathrm{fst}\left(a\right)+2\cdot x,0,bits\right)=\mathrm{div}\left(n,2\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{N}\times \mathbb{N}x:\mathbb{N}\mapsto \mathrm{snd}\left(a\right)+2\cdot x,0,bits\right)=\mathrm{div}\left(j,2\right)\right)\wedge \mathrm{length}\left(dns\right)=\mathrm{length}\left(bits\right)\right)\wedge \mathrm{length}\left(djs\right)=\mathrm{length}\left(bits\right)\right)\wedge \left(\forall z\in \mathbb{Z},z\in dns\Rightarrow \left(z=\mathrm{neg}\left(1\right)\vee \left(z=0\vee z=1\right)\right)\right)\right)\wedge \left(\forall z\in \mathbb{Z},z\in djs\Rightarrow \left(z=\mathrm{neg}\left(1\right)\vee \left(z=0\vee z=1\right)\right)\right)\right)\wedge \mathrm{IsChain}\left(dns,\lambda a:\mathbb{Z}b:\mathbb{Z}\mapsto a=0\vee b=0\right)\right)\wedge \mathrm{IsChain}\left(djs,\lambda a:\mathbb{Z}b:\mathbb{Z}\mapsto a=0\vee b=0\right)\right)\wedge \mathrm{IsChain}\left(\mathrm{zip}\left(\mathrm{cons}\left(0,\mathrm{cons}\left(0,dns\right)\right),\mathrm{tail}\left(\mathrm{cons}\left(0,\mathrm{cons}\left(0,dns\right)\right)\right)\right),\lambda a:\mathbb{Z}\times \mathbb{Z}b:\mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{fst}\left(a\right)\cdot \mathrm{snd}\left(b\right)\ne \mathrm{neg}\left(1\right)\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{Z}x:\mathbb{Z}\mapsto a+2\cdot x,0,dns\right)=2\cdot \mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{Z}x:\mathbb{Z}\mapsto a+2\cdot x,0,djs\right)=2\cdot \mathrm{cast}\left(\mathrm{div}\left(j+1,2\right),\mathbb{Z}\right)\right)\Rightarrow \left(\exists charge\in \mathrm{Bool},\exists s\in \mathrm{Fin}\left(1492\right),\exists t\in \mathrm{Fin}\left(1492\right),\exists xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\left(\left(\left(\left(\left(\left(s\in \mathrm{start}\left(\mathrm{baseAutomaton}\left(charge\right)\right)\wedge t\in \mathrm{accept}\left(\mathrm{baseAutomaton}\left(charge\right)\right)\right)\wedge \mathrm{Nonempty}\left(\mathrm{Path}\left(\mathrm{baseAutomaton}\left(charge\right),s,t,xs\right)\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right),2\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{mod}\left(n,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s\right)\right)\right),3\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{cast}\left(\mathrm{mod}\left(j,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}x:\mathbb{Z}\mapsto \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)+2\cdot x,0,xs\right)=\mathrm{cast}\left(\mathrm{div}\left(n,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{foldr}\left(\lambda a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}x:\mathbb{Z}\mapsto \mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)+2\cdot x,0,xs\right)=\mathrm{cast}\left(\mathrm{div}\left(j,2\right),\mathbb{Z}\right)\right)\wedge \mathrm{length}\left(xs\right)=\mathrm{length}\left(bits\right)\right)$$

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

Source. Repository-derived.

Commentary.

Both supplied signed expansions have the length of the bit input and evaluate to twice the respective ceiling half-endpoint. Their coefficients are minus one, zero or one, and adjacent digits cannot both be nonzero. The input additionally forbids opposite signs at distance two, including the two initial zero memories. Modulo-four rigidity identifies the emitted digits at each step; bounded converter carries preserve the residual value and the input spacing prevents rejection. The terminal bit state and zero residual force all converter carries to flush. The finite graph then realizes this arithmetic run with exactly one transition per supplied bit. The charge-mode Boolean selects one of the two graph acceptance sets. div and mod are natural integer quotient and remainder.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseDigitRealization.base_bit_path_realization
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BasePathRealization
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/CutBitRelation