87. Selection from data does not remove the uncertainty quantifier
On this page · Permalink · Source line 3463
A domain can be selected after examining fitted operators without a separate statistical penalty for each geometry tried. That statement holds only when the final verification ranges over an already justified confidence set.
Proposition 78: Data-selected geometry with honest coverage
Suppose a random set \(\mathcal U\) of operators and initial states, in a declared fixed predictive coordinate system, contains the true model with probability at least \(1-\delta\). A data-dependent procedure may propose any transform \(T\) and any domain. If its exact verifier proves domain membership and invariance for every member of the same set \(\mathcal U\), then on that coverage event the true model has the verified domain. No union bound over geometry proposals is needed for this deterministic implication.
If original-coordinate perturbations satisfy \(\|\Delta\|_2\leq e\), their combined mass and spatial output error after a known transform \(T\) is at most
The corresponding transformed uncertainty budget must be used even when \(T\) was chosen from the data.
Read proof · Recorded Lean scope · Permalink · Source line 3467
Proof
On the coverage event the true model is a member of the set quantified by the verifier. Its domain properties follow by direct inclusion, regardless of how \(T\) was selected. For the error, a normalized Lorentz input has Euclidean norm at most \(\sqrt2\). Thus the Euclidean norm of \(T\Delta T^{-1}z\) is at most \(\sqrt2\|T\|_2\|T^{-1}\|_2e\). The sum of its mass magnitude and spatial norm is at most \(\sqrt2\) times its Euclidean norm. Multiply the two bounds. \(\square\)
The set must not be shrunk around a convenient candidate without preserving coverage. Moving the center by a reset mixture changes the family being certified. A tube around the repaired family need not contain the original true family. Repeatedly estimating new confidence sets still requires the stage accounting of Proposition 48. Statistical rank coverage and observation identifiability remain assumptions of the upstream procedure.
The final reference certificate explicitly says that no statistical coverage is claimed. Its uncertainty box is a deterministic, exactly described set around the repaired operator family. This supports a reproducible robustness statement without pretending that the example has estimated an unknown noise distribution.