53. Repeated proposal and verification with a confidence budget
On this page · Permalink · Source line 2120
Model development may choose another core, propose another domain or collect another independent batch after an earlier certificate is withheld. Statistical coverage must survive that selection process.
Proposition 48: Sequential confidence accounting for certified proposals
At stage \(n\), let the proposal be measurable from previous data, and let a verification procedure return a set \(\mathcal U_n\) for the true model in the declared identifiable coordinate system. Assume conditional coverage
Then with probability at least \(1-\delta\), every returned uncertainty set covers its true model. On this event, any data-selected domain with an exactly verified robust certificate for all members of its corresponding \(\mathcal U_n\) is also valid for the true model, provided the true initial state is covered by the certified base. The conclusion remains valid at any stopping time chosen from the recorded results.
Read proof · Recorded Lean scope · Permalink · Source line 2124
Proof
Take expectations of the conditional failure bounds, then apply the countable union bound. Off the union of failure events, all coverages hold simultaneously. Robust invariance over an entire set then applies to its true member by deterministic implication, independently of how its domain was chosen. A stopped stage is one of the already covered stages. \(\square\)
For example, \(\delta_n=\delta 2^{-n}\) spends a finite total confidence budget. Fresh reset trials for a proposal fixed by past data can use Proposition 35 conditionally, with this stage budget. An exact witness needs no statistical correction for how many candidate cones were tried. The coverage statement does need correction for repeatedly constructing confidence sets or inspecting post-selected data.
The proposition does not infer a global rank bound, validate an unknown reset operation, or transform dependent observations into independent trials. Those are assumptions of the coverage procedure. A known coordinate transformation can transport a confidence set exactly. An estimated transformation requires the subspace and conditioning controls already separated in Part III.