Signed Digit Streams of the Base Transducer

Abstract

Every accepted base-transducer path emits nonadjacent signed digits with an exact radix-two value.

Definition 1.1 (Ordered transition observations).

$$\left(\forall alpha\in \mathrm{Type},\forall sigma\in \mathrm{Type},\forall beta\in \mathrm{Type},\forall M\in \mathrm{NFA}\left(alpha,sigma\right),\forall emit\in sigma\to alpha\to sigma\to beta,\forall s\in sigma,\mathrm{pathOutputs}\left(M,emit,NFA.Path.nil\left(s\right)\right)=[]\right)\wedge \left(\forall alpha\in \mathrm{Type},\forall sigma\in \mathrm{Type},\forall beta\in \mathrm{Type},\forall M\in \mathrm{NFA}\left(alpha,sigma\right),\forall emit\in sigma\to alpha\to sigma\to beta,\forall s\in sigma,\forall q\in sigma,\forall t\in sigma,\forall a\in alpha,\forall xs\in \mathrm{List}\left(alpha\right),\forall hstep\in q\in \mathrm{step}\left(M,s,a\right),\forall p\in \mathrm{Path}\left(M,q,t,xs\right),\mathrm{pathOutputs}\left(M,emit,NFA.Path.cons\left(q,s,t,a,xs,hstep,p\right)\right)=\mathrm{cons}\left(\mathrm{emit}\left(s,a,q\right),\mathrm{pathOutputs}\left(M,emit,p\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams.pathOutputs (✓ std3).

Source. Repository-derived.

Commentary.

pathOutputs reads one transition observation per edge in path order. The nil constructor emits the empty list; cons prepends emit s a q to the observations of the remaining path. Its automaton, alphabet, state and output types are arbitrary.

Theorem 1.2 (Exact sparse signed-digit reconstruction).

$$\forall charge\in \mathrm{Bool},\forall output\in \mathrm{Bool},\forall s\in \mathrm{Fin}\left(1492\right),\forall t\in \mathrm{Fin}\left(1492\right),\forall xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\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)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(charge\right),s,t,xs\right),\left(\left(\left(\forall z\in \mathbb{Z},z\in \mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(charge\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{Fin}\left(1492\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\Rightarrow \left(z=\mathrm{neg}\left(1\right)\vee \left(z=0\vee z=1\right)\right)\right)\wedge \mathrm{IsChain}\left(\mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(charge\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{Fin}\left(1492\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right),a:\mathbb{Z}\mapsto b:\mathbb{Z}\mapsto a=0\vee b=0\right)\right)\wedge \mathrm{foldr}\left(z:\mathbb{Z}\mapsto acc:\mathbb{Z}\mapsto z+2\cdot acc,0,\mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(charge\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{Fin}\left(1492\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right)=2\cdot (\mathrm{foldr}\left(a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto acc:\mathbb{Z}\mapsto \mathrm{ite}\left(output,\mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(a\right)\right)\right)\right)+2\cdot acc,0,xs\right)+\mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,3,2\right)<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),\mathrm{ite}\left(output,3,2\right)\right)\right),\mathrm{none}\left(\right)\right),0\right))\right)\wedge \mathrm{ite}\left(\mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(charge\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{Fin}\left(1492\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)=[],\mathrm{none}\left(\right),\mathrm{some}\left(List.head\left(\mathrm{pathOutputs}\left(\mathrm{baseAutomaton}\left(charge\right),\lambda [\mathrm{Fin}\left(1492\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{Fin}\left(1492\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,12,10\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(q\right)\right)\right),\mathrm{ite}\left(output,12,10\right)\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right)\right)\right)=\mathrm{some}\left(0\right)\right)$$

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

Source. Repository-derived.

Commentary.

output selects the fourth edge coordinate and target-state component 12 when true, or the third edge coordinate and component 10 when false. Every emitted digit is minus one, zero, or one; consecutive digits cannot both be nonzero. Folding z + 2 x gives twice the encoded rounded half. The first emitted digit is the dummy zero at position minus one. All path lengths are allowed. This is a statement about accepted graph paths; completeness for actual palindrome cuts and the Q interpretation remain separate obligations.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams.base_path_sparse_signed_digits
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams.pathOutputs
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseCertificates