Two-Boundary Observation of a Prime Register
Abstract
Both guard distances, rather than current legality alone, determine the exact finite-horizon state.
The bounded runner records whether the entire requested word was legal. At horizon H, compare all words of total length at most H, including the empty word.
Theorem 1.1 (The exact two-boundary profile).
Proof. Machine-checked in Lean as D5/S3/Factorization/Automata/BoundedPrimeHorizon.finite_horizon_kernel (✓ std3). ∎
Source. Repository-derived.
Commentary.
Two live states have equal responses to every such word exactly when the displayed profiles agree. Necessity uses repeated multiplication and division. Sufficiency is induction over the word: first-step guards agree, and successful successors have equal profiles at H-1. Mixed paths, underflow and overflow are all covered.
Theorem 1.2 (Every profile is realized and counted).
Proof. Machine-checked in Lean as D5/S3/Factorization/Automata/BoundedPrimeHorizon.profile_classification (✓ std3). ∎
Source. Repository-derived.
Commentary.
A concrete code collapses only the central interval. It is surjective onto Fin(min(a,2H)+1), and its kernel is exactly the response kernel. The separate rejection point remains visible on the empty word. This is not a claim that a fixed-H quotient updates autonomously for arbitrarily many later steps.