98. A conditional data-to-domain theorem
On this page · Permalink · Source line 3977
Proposition 87: Observable structured learning with a covered domain
Suppose the scalar process obeys the conditional law of Proposition 83 with the declared reference measure and fixed parameters satisfying \(|a|,|b|\leq1\). Use the predictable regressions, fixed dictionary and confidence protocol of Proposition 84. At a data-selected finite time, form the full outward-rounded rectangle. If its density floor \(\rho\) is nonnegative, that rectangle has an exact all-horizon probability certificate on \(C\). If \(\rho>0\), every chosen center inside it has the marginal and record bounds of Propositions 85–86 relative to every member.
With probability at least \(19/20\) over the specified stochastic observation process, these implications cover its true parameter at every checked time, including a stopping time. Internal validity of a verified rectangle is deterministic. Statistical coverage remains conditional on the declared process, moment, parameter and observation assumptions.
Read proof · Recorded Lean scope · Visual guide: A confidence set can meet an exact certificate · Visual guide: Choose the future quantity before its bound · Permalink · Source line 3979
Proof
Proposition 84 provides one simultaneous event on which both true parameters belong to all returned intervals. Proposition 83 supplies the domain certificate for the entire rectangle whenever its sufficient density floor is nonnegative. The selected center is one of its members, and the maximum distances to the endpoints bound each parameter difference. Proposition 85 gives conditional and record error. If the floor is positive, all true conditional rows have the same lower reference component, so Proposition 86 applies to the scalar Markov process. Selection of the stopping time does not alter the already simultaneous event. None of these implications verifies the assumptions from a single sample path. \(\square\)
No claim of empirical coverage follows from the saved run. It is one seeded finite realization of the exactly declared discrete analogue. The general confidence result is a theorem, with assumptions recorded in the certificate. Its independent checker rederives the sufficient statistics, rational radii, outer endpoints, density floor and error budgets from the saved path. It rejects a changed reference measure, a narrower claimed interval, an altered path checksum or an unsupported claim that the assumptions were independently verified.
This is the point where probability-domain certification and data uncertainty become connected in an executed dependent-signal example. The family is more restrictive than an arbitrary learned operator. That restriction is visible and does useful work: it preserves the nonlinear posterior curve while uncertainty changes its likelihoods.