First Nonzero Digit Order

Abstract

A tight accepted base path has no earlier nonzero output coefficient.

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

$$\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(\mathrm{true}\right)\right)\wedge t\in \mathrm{accept}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right)\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(\mathrm{true}\right),s,t,xs\right),\mathrm{pathCharge}\left(\lambda [\mathrm{Fin}\left(1492\right)]a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}[\mathrm{Fin}\left(1492\right)]\mapsto \mathrm{fst}\left(a\right),p\right)=1\Rightarrow \left(\forall i\in \mathbb{N},\mathrm{getD}\left(\mathrm{ite}\left(i<List.length\left(\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(12<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),12\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right),\mathrm{some}\left(GetElem.getElem\left(\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(12<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),12\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right),i\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\Rightarrow \left(\exists k\in \mathbb{N},k\le i\wedge \mathrm{getD}\left(\mathrm{ite}\left(k<List.length\left(\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(10<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),10\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)\right),\mathrm{some}\left(GetElem.getElem\left(\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(10<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),10\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right),k\right)\right),\mathrm{none}\left(\right)\right),0\right)\ne 0\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The lowest-position product records an output nonzero coefficient before the first input nonzero coefficient. Lifting the base path preserves every label, so a true terminal flag would contradict its bound zero on a path with f charge one. The persistent flag is therefore false. Induction along the base path, using the literal first-sign memory checker, supplies a nonzero input coefficient no later than any nonzero output coefficient. Optional list entries use default zero. The coefficients include the dummy leading zero, so both streams use the same indexing.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/BaseLowestPosition.base_path_lowest_order
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseQArithmetic
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPathRealization