91. A smaller repair can be bracketed rather than guessed
On this page · Permalink · Source line 3587
Keep the fitted operators, proposed transform and initial state from Section 88 unchanged. In Lorentz coordinates use the center-reset operator \(N=e_0\lambda\), of constant density one under \(du/2\). Write
Fix a required margin \(0\leq\kappa\leq1\). Feasibility means that every action, observation and normalized input has margin at least \(\kappa\). Integrated mass and initial membership remain separate requirements.
Proposition 80: Convex repair bracketing
The feasible repair weights form a closed interval \([\eta_*,1]\). If a cone-positive functional \(\ell=(1,-v^{\mathsf T})\), with \(\|v\|_2\leq1\), and a normalized input \(z\) give \(c=\ell\widehat F_a(u)z<\kappa\), then every feasible weight satisfies
A complete certificate at a weight \(\eta_U\) gives an upper bound on \(\eta_*\). A negative Bernstein coefficient without a negative evaluated point does not give a lower bound.
Read proof · Recorded Lean scope · Permalink · Source line 3598
Proof
For a fixed input and observation, output mass minus spatial norm is a concave continuous function of the operator, hence of \(\eta\). Its superlevel set is closed and convex. Intersecting these sets preserves those properties. The reset has margin one, so the intersection contains one and is an interval ending there. If \(F_\eta\) has margin at least \(\kappa\), every such functional satisfies \(\ell F_\eta z\geq\kappa\). Since \(\ell Nz=1\), this requires \((1-\eta)c+\eta\geq\kappa\). Here \(1-c>0\), and solving gives the bound. A complete positive witness proves feasibility. A negative coefficient only says that a particular sufficient polynomial bound failed. \(\square\)
91.1 The unchanged predecessor example
On this page · Permalink · Source line 3608
Use the previous transform with center \((1/2,1/2)\) and triangular factor
At the direct action, observation \(u=-1\), normalized input \((1,1,0)\) and functional \(\ell=(1,7/25,-24/25)\), exact evaluation gives
For the required margin \(\kappa=1/64\), this proves
The lower endpoint is approximately \(0.02299\). The upper endpoint is not a sampled estimate. A complete exact Bernstein certificate proves that \(\eta=1/32\) works. The weight \(1/64\) fails the requested \(1/64\) margin at the displayed separating functional. This does not by itself prove that its nominal model is probability-invalid.
The new certificate uses 194 leaves and 3,058 recomputed coefficients. A separate comparison-domain certificate uses 185 leaves and 2,833 coefficients. Both retain the same degree-two coefficient box of radius \(1/4096\) in their respective declared Lorentz coordinates, subject to exact integrated mass. The more general mass and spatial output budgets remain \(1/128\) each. Their sum equals the certified margin, so that larger output-error family has a nonnegative lower margin, not a claimed strictly positive residual margin.
The reset weight has fallen from \(1/8\) to \(1/32\), while the deterministic uncertainty box is unchanged. No global optimization over geometry or repair operators is claimed. The current bracket concerns this fixed geometry, this reset path and this required margin.
The comparison domain is checked again before invoking the law theorem. Keeping the same raw discrepancy budget \(241/40000\) from Section 89 gives
Consequently, under a common policy and identical initial states,
The first integer horizon where this upper bound reaches one is now 30 rather than eight. The bound remains conservative. The repaired uncertainty tube is still not a confidence set for the unmodified generating process. This improvement is deterministic certificate refinement, not a new statistical experiment.