Likely and Allowed: The Joint State of Prediction and Admissibility

Give a forecaster the exact probability law of a process, then ask what happens next given that the future must obey a declared rule. If it ignores which futures the rule still allows, it can be forced to be wrong by nearly as much as any forecaster can be: error approaching 1-1/d on a d-symbol alphabet. A model can predict the next word perfectly and still write code that will not compile. Knowing what is likely is not knowing what is allowed, and I make that distinction exact. A history carries two states: its predictive state \varepsilon, which fixes its future law, and its residual state \kappa, which fixes which continuations a separately declared rule still admits. Each is classical on its own. I prove that the pair J=(\varepsilon,\kappa) is exactly the state of survival-aware prediction. Every survival probability and every survival-conditioned forecast depends only on J. Conversely, under full support those forecasts recover J after the finite horizon \max(k-2,\,m-1), and no shorter horizon works in general. The converse survives noise. Forecasts that agree within an explicit margin pin down the residual state exactly and the predictive state to within a bound set by an observability constant, and I give counterexamples showing that neither constant can be dropped. The same state gives value bounds for planning, tight bounds on certificate bases for search by elimination, and a sharp map of when the canonical machine is canonical. The core theorems are machine-checked in Lean 4 (159 theorems, standard axioms only), and every finite claim is reproduced in exact arithmetic. The archive contains the paper (PDF and Markdown), the Lean 4 formalization, and exact-arithmetic reproduction scripts.