Marker Reconstruction Certificate

Abstract

Literal marker successors are completely represented in this finite row interval.

Theorem 1.1 (Rows 2048 through 2559).

$$\forall i\in \mathbb{N},\left(2048\le i\wedge i<2560\right)\Rightarrow \mathrm{prefixRealizationRowCheck}\left(i\right)=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

Kernel reduction checks every literal marker successor against the indexed edge list and every target index against the 4262-state bound. The interval includes its lower endpoint and excludes its upper endpoint.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate4.prefix_realization_rows_4
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates