78. An integrated theory of construction and correction
On this page · Permalink · Source line 3170
Proposition 70: Separate structural acceptance, approximation control and sequential rejection
Consider a fitted polynomial model in a declared predictive coordinate system, and prospectively registered observation tests with total budget \(\delta\).
A successfully replayed quadratic certificate from Proposition 62 establishes internal all-horizon validity. A successful operator-only proposal from Proposition 63 is one way to obtain it, not an assumption that all valid models have such a proposal.
For any generating density on a common probability cone with a justified Lipschitz constant, a positive degree-\(n\) approximation and certified coefficient budgets satisfy Propositions 64–65, hence a fixed-horizon upper law bound. If a generating process lies outside that representation, a separately justified bound on its conditional kernels instead invokes Proposition 69.
For predictable tests on actual dependent observations, Propositions 66 and 68 give simultaneous lower discrepancy certificates, including at data-selected stopping times. Covered randomized actions admit the contextual evidence of Proposition 67. These conclusions coexist without implying that structural acceptance or statistical nonrejection proves the generating process belongs to the model class.
Read proof · Recorded Lean scope · Permalink · Source line 3172
Proof
Each structural statement is a deterministic consequence of its replayed equalities and inequalities. The approximation statements require their declared common-domain, regularity and coefficient conditions, or alternatively the conditional-kernel discrepancy assumptions. The statistical conclusions hold on the simultaneous probability event of Proposition 66. None of these implications uses nonrejection as an upper bound or infers coverage from a finite determinant. Their conjunction therefore retains the separate hypotheses and conclusions exactly as stated. \(\square\)
The central object is now more than a fitted operator. It includes an admissible domain with a replayable witness, an explicit approximation class, and an evidence rule specifying which observations could contradict its predictions. Geometry discovery proposes a representation. Verification checks its algebra. Approximation theory accounts for information lost by a chosen finite description. Sequential tests expose conditional discrepancies in observed signals.
Those roles are related but not interchangeable. A failed search means that this construction did not provide a witness. A failed witness means its submitted identities or signs do not establish the claimed validity. A detected residual means a registered predictive condition is inconsistent with the observations at the stated error budget. These three outcomes should be reported differently.