Complete Representation of Marker Paths

Abstract

Literal marker transitions are represented completely by the finite product graph.

Definition 1.1 (The marker transition graph before indexing).

$$prefixRawAutomaton=NFA.mk\left(s:\mathrm{List}\left(\mathbb{Z}\right)\mapsto a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \{t:\mathrm{List}\left(\mathbb{Z}\right)\mid (t,a)\in \mathrm{successors}\left(s\right)\},\mathrm{univ}\left(\mathrm{List}\left(\mathbb{Z}\right)\right),\mathrm{univ}\left(\mathrm{List}\left(\mathbb{Z}\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization.prefixRawAutomaton (✓ std3).

Source. Repository-derived.

Commentary.

States are lists of integer components and each step is one of the literal marker successors. This transition graph places no conditions on its endpoints: its start and accept sets are universal. A separate condition picks the source and final flags when a cut is realized. The four alphabet coordinates are the signed-weight charge, signed-digit charge and the two shifted input bits.

Theorem 1.2 (Every marker path stays in the finite graph).

$$\forall charge\in \mathrm{Bool},\forall s\in \mathrm{List}\left(\mathbb{Z}\right),\forall t\in \mathrm{List}\left(\mathbb{Z}\right),\forall xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\mathrm{Nonempty}\left(\mathrm{Path}\left(prefixRawAutomaton,s,t,xs\right)\right)\Rightarrow \left(\forall u\in \mathrm{Fin}\left(4262\right),\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(u\right)\right)\right)=s\Rightarrow \left(\exists v\in \mathrm{Fin}\left(4262\right),\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(v\right)\right)\right)=t\wedge \mathrm{Nonempty}\left(\mathrm{Path}\left(\mathrm{prefixAutomaton}\left(charge\right),u,v,xs\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Starting at any represented state, every symbolic marker path lifts to an indexed path with identical edge labels and identical final components. Complete successor reconstruction is checked at all 4262 product rows. Induction on the arbitrary finite path constructs each indexed successor. This proves completeness of the finite carrier; recognizing the literal marked prefix and its tail phases remains a separate arithmetic step.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization.prefixRawAutomaton
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization.prefix_path_realization
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate0
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate1
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate2
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate3
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate4
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate5
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate6
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate7
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate8