Marker Reconstruction Certificate

Abstract

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

Theorem 1.1 (Rows 3584 through 4095).

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

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/PrefixRealizationCertificate7.prefix_realization_rows_7 (✓ 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/PrefixRealizationCertificate7.prefix_realization_rows_7
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates