Literal Most Recent Sign Memory

Abstract

The most recent sign memory equals the last nonzero emitted coefficient.

Theorem 1.1 (The literal minimum-position transition law).

$$\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),s\in \mathrm{start}\left(\mathrm{baseAutomaton}\left(charge\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(charge\right),s,t,xs\right),\mathrm{getD}\left(\mathrm{ite}\left(\mathrm{ite}\left(output,17,16\right)<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(t\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(t\right)\right)\right),\mathrm{ite}\left(output,17,16\right)\right)\right),\mathrm{none}\left(\right)\right),0\right)=\mathrm{getD}\left(\mathrm{ite}\left(\mathrm{filter}\left(z:\mathbb{Z}\mapsto (z!=0),\mathrm{pathOutputs}\left(\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)=[],\mathrm{none},\mathrm{some}\left(List.getLast\left(\mathrm{filter}\left(z:\mathbb{Z}\mapsto (z!=0),\mathrm{pathOutputs}\left(\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)\right),0\right)\right)$$

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

Source. Repository-derived.

Commentary.

For either emitted stream, each literal base edge updates the most recent sign when its new coefficient is nonzero. Induction along an arbitrary source path identifies the terminal memory with the last nonzero coefficient of the emitted stream. All source memories start at zero, and absent last entries use default zero. Acceptance and tightness are unnecessary; this statement also applies to the partial path before a marker is selected. The last-option expression is none for an empty list and some(List.getLast(…)) otherwise; the nonempty proof argument is implicit.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseLastSignMemory.base_path_last_sign
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseChargeArithmetic