Complete Lowest-Position Product Realization

Abstract

Every base path lifts to the complete product graph and records exactly its lowest-position escape events.

Theorem 1.1 (The product flag is the event disjunction).

$$\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(true\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{baseAutomaton}\left(true\right),s,t,xs\right),\exists u\in \mathrm{Fin}\left(1710\right),\exists v\in \mathrm{Fin}\left(1710\right),\left(\left(\left(u\in \mathrm{start}\left(minimumAutomaton\right)\wedge \mathrm{fst}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(u\right)\right)\right)=\mathrm{val}\left(s\right)\right)\wedge \mathrm{fst}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(v\right)\right)\right)=\mathrm{val}\left(t\right)\right)\wedge \mathrm{Nonempty}\left(\mathrm{Path}\left(minimumAutomaton,u,v,xs\right)\right)\right)\wedge \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{minimumTable}\left(\mathrm{val}\left(v\right)\right)\right)\right)=\mathrm{any}\left(id,\mathrm{pathOutputs}\left(\lambda s0:\mathrm{Fin}\left(1492\right)[\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{Fin}\left(1492\right)\mapsto Bool.and\left(Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(14<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s0\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{val}\left(s0\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{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)==0)\right),(\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)!=0)\right),p\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The lift preserves each of the four labels and the initial and final base-state indices. It starts with a false flag. Its final flag equals the Boolean disjunction of the path events: no input nonzero has yet been recorded, the current input digit is zero, and the current output digit is nonzero. No accepting-endpoint premise is needed for path construction; if the flag is true and the base endpoint accepts, the lifted path accepts in minimumAutomaton. any is Boolean list disjunction, id is the Boolean identity, and the anonymous bracket in the event lambda represents the unused edge-label argument.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPathRealization.minimum_path_realization
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MinimumPositionCertificate