89. The prediction cost needs a common comparison domain
On this page · Permalink · Source line 3534
A successful discovered domain does not imply that the known reference model has that same domain. To invoke a common-cone law bound, the example separately checks the corrected family on the predecessor's exact ellipse. This is a second certificate used only for comparison. It is not supplied to geometry discovery.
In that comparison domain, the coefficient-wise upper bounds on the raw fitting discrepancy are
Using \(\int_{-1}^1|u|^kdu/2=1/(k+1)\) gives the integrated upper budget \(241/40000\). The same center-reset reference is valid there. Both models have the same initial state.
Proposition 79: Certified repair with a retained comparison budget
For the exact construction of Section 88, independent replay establishes internal validity of the repaired model and its declared coefficient uncertainty family. Independent comparison-domain replay and the coefficient bounds above give
Consequently, for any common policy and any finite horizon \(T\),
This compares the unmodified reference process and the nominal repaired process. It is not a guarantee that the raw noisy model was valid or that the repaired uncertainty family contains the original reference.
Read proof · Recorded Lean scope · Permalink · Source line 3546
Proof
The polynomial witnesses and exact mass identities imply the nominal and robust validity statements by Propositions 71, 75 and 76. The separate comparison witness establishes the required common domain for the nominal repaired and reference operators. The absolute coefficient bounds dominate the integrated raw error by the triangle inequality. Proposition 73 then gives the displayed repair budget and law bound. All hypotheses are either exact identities in the supplied witnesses or direct norm bounds from the declared rational coefficients. \(\square\)
The bound is conservative. It becomes one at horizon eight, so it makes no nontrivial long-horizon accuracy claim. The example's point is the separation of a verified all-horizon probability model from a finite-horizon approximation guarantee. A probability-valid model is not necessarily a close model.
The noisy proposal, the failed raw fit, the repair and the comparison bound all appear in the release records. None is replaced by a more favorable trajectory score. The coefficient box is around the repaired family in the specified coordinates, not an inferred distribution of sensor noise.