54. Integrated certificate-carrying realization
On this page · Permalink · Source line 2140
Proposition 49: Conditional learning with an all-horizon probability certificate
Suppose the observable identification assumptions of Proposition 37 hold for a declared finite-rank controlled process. Suppose a justified confidence procedure produces an operator and initial-state set containing the true realization on an event of probability at least \(1-\delta\). Assume the per-action mass constraints are exact.
If a fitted realization admits a checked finite witness of Proposition 39, it is an internally valid stochastic model at every horizon. If the witness is robust over the whole confidence set and covers its initial states, then on the coverage event the same probability domain is valid for both the fitted and true models. When their summed base-norm instrument discrepancies are at most \(\epsilon_t\) and their initial discrepancy is at most \(e_0\), every common policy has the bound
Conditioning on a positive-probability event then obeys Proposition 44. Exact coordinate transport preserves the certificate. A signed packet decomposition preserves it after complete synthesis but does not turn individual packets into probability states without Proposition 30's extra positivity requirement.
Read proof · Recorded Lean scope · Permalink · Source line 2142
Proof
Observable identification supplies the specified realization and the confidence procedure supplies the stated event, not an inferred event of its own. Proposition 39 supplies internal validity for the fitted model. Proposition 40 extends the same domain to every member of the uncertainty set, hence to its true member on that event. Propositions 42 and 43 give the total-variation bound, and Proposition 44 gives the conditional bound. For a coordinate change \(T\), use \(V'=TV\), \(B_s'=TB_sT^{-1}\) and \(\lambda'=\lambda T^{-1}\). Then \(B_s'V'=V'A_s\) and \(\lambda'V'=\mathbf1^\top\) with the unchanged nonnegative witnesses. Full packet synthesis is the identity. \(\square\)
This closes a concrete foundational gap. A learner can now return not just a matrix family but a verifiable domain in which that family has probability meaning. It can attach a robust uncertainty statement when one is justified, or return an internally valid approximation with its correction budget explicitly recorded.
It does not turn a successful fit into unrestricted knowledge of the world. The model class, observation protocol, rank coverage, exact mass law, domain witness and approximation budget remain visible parts of the result. Failure of a finite search is a withheld certificate, not a proof of invalidity. The nonpolyhedral example explains why this distinction is necessary even for very small exact models.