Lowest Signed-Digit Position Certificate

Abstract

No accepted escape path in the complete lifted graph has positive f weight.

Definition 1.1 (The complete lifted lowest-position graph).

$$\forall i\in \mathbb{N},\mathrm{minimumTable}\left(i\right):\mathbb{N}\times \mathrm{Bool}\times \mathrm{List}\left(\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right)\times \mathrm{Option}\left(\mathbb{Z}\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.minimumTable (✓ std3).

Source. Repository-derived.

Commentary.

For indices zero through 1709, minimumTable selects one of 1710 literal rows through a balanced tree of index comparisons and 64 private minimumTableChunk functions taking the original natural index. Each row lists the base-state index, the persistent lowest-position escape flag, every lifted edge, and the optional integer potential. Base states are the 1492 states of baseTable. Outside this range lookup returns the final row; all runs use Fin 1710.

Definition 1.2 (The literal lowest-position flag update).

$$\forall i\in \mathbb{N},\mathrm{successors}\left(i\right)=\mathrm{map}\left(\lambda e:\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto (\mathrm{fst}\left(e\right),Bool.or\left(\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{minimumTable}\left(i\right)\right)\right),Bool.and\left(Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(14<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(\mathrm{minimumTable}\left(i\right)\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(\mathrm{minimumTable}\left(i\right)\right)\right)\right),14\right)\right),\mathrm{none}\left(\right)\right),0\right)==0),(\mathrm{getD}\left(\mathrm{ite}\left(10<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),10\right)\right),\mathrm{none}\left(\right)\right),0\right)==0)\right),(\mathrm{getD}\left(\mathrm{ite}\left(12<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right),12\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0)\right)\right),\mathrm{snd}\left(e\right)),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(\mathrm{minimumTable}\left(i\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.successors (✓ std3).

Source. Repository-derived.

Commentary.

For every outgoing base edge, preserve its four labels and attach the persistent flag. The flag is set when the first-input-sign memory is still zero, the newly emitted input digit is zero, and the newly emitted output digit is nonzero. This is the arithmetic update used both by the potential checker and by complete path realization.

Definition 1.3 (The lowest-position escape automaton).

$$\mathrm{minimumAutomaton}\left(\right)=NFA.mk\left(i:\mathrm{Fin}\left(1710\right)\mapsto a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \{j:\mathrm{Fin}\left(1710\right)\mid (\mathrm{val}\left(j\right),a)\in \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(i\right)\right)\right)\right)\right)\},\{i:\mathrm{Fin}\left(1710\right)\mid \mathrm{val}\left(i\right)<7\},\{i:\mathrm{Fin}\left(1710\right)\mid Bool.and\left(Bool.and\left(\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(i\right)\right)\right)\right),\mathrm{baseTerminal}\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(i\right)\right)\right)\right)\right)\right)\right),(\mathrm{getD}\left(\mathrm{ite}\left(18<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(i\right)\right)\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(i\right)\right)\right)\right)\right),18\right)\right),\mathrm{none}\left(\right)\right),0\right)==0)\right)\}\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.minimumAutomaton (✓ std3).

Source. Repository-derived.

Commentary.

Its seven source indices are zero through six. Edges are literal table entries. A terminal state has the escape flag true and its base state is accepted in the valid-output mode of baseAutomaton. The flag becomes true when an output nonzero digit appears before the first input nonzero digit.

Theorem 1.4 (The lowest-position escape bound).

$$\forall s\in \mathrm{Fin}\left(1710\right),\forall t\in \mathrm{Fin}\left(1710\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{minimumAutomaton}\left(\right)\right)\wedge t\in \mathrm{accept}\left(\mathrm{minimumAutomaton}\left(\right)\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{minimumAutomaton}\left(\right),s,t,xs\right),\mathrm{pathCharge}\left(\lambda [\mathrm{Fin}\left(1710\right)]a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}[\mathrm{Fin}\left(1710\right)]\mapsto \mathrm{fst}\left(a\right),p\right)\le 0\right)$$

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

Source. Repository-derived.

Commentary.

Kernel reduction checks all 1710 rows, verifies complete lifting of the base graph, and proves the source, goal and reverse-closed potential inequalities. Every accepting run has total f charge at most zero. This graph statement requires an arithmetic identification of f with the signed-weight difference before it can imply a statement about actual cuts.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.minimumAutomaton
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.minimumTable
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.minimum_accepted_bound
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate.successors
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseCertificates