stabilityThreshold_hypothesis
plain-language theorem explainer
Packages the empirical stability threshold 0.01 as a quarantined data hypothesis over the reals. Measurement and verification authors cite it when bridging calibration numbers into preregistered claims without polluting the certified surface. Construction is a one-line factory call that attaches provenance, a falsifier string, and a removal plan pointing at a future overlap-perturbation bound.
Claim. The real number $0.01$ is recorded as an empirical data hypothesis named stability threshold: the claim that this threshold is large enough that classification is stable under perturbation, together with provenance of the underlying measurement, a falsifier (perturbation changes classification within the threshold), and a removal plan (replace by a tight bound from an overlap-perturbation estimate).
background
The ambient module is the quarantine layer for empirical inputs. Certified theorem-level claims must not import raw measurements; instead every calibration constant, mined dataset, or measured real is wrapped in provenance (source, hash, generator, timestamp, version) and, when it is meant to become a claim, lifted to a data hypothesis.
A data hypothesis is the bridge type: name, claimed value in some type $\alpha$, the underlying measurement result with provenance, status, a human-readable falsifier, and a removal plan that says how the number should eventually be discharged by a proof. Sibling raw values such as the stability threshold measurement supply the numeric claim; this declaration only reifies that measurement as a hypothesis record.
Local convention: modules under Verification/Measurement stay quarantined. Test and preregistration suites may import them; the certified surface may not.
proof idea
Not a proof. The definition is a single application of the measurement-to-hypothesis factory: it fixes the name string, plugs in the raw stability-threshold measurement as the claim, and attaches two fixed strings as falsifier and removal plan (perturbation changes classification within threshold; prove a tight bound from the overlap-perturbation estimate). No tactics, no lemmas beyond that constructor.
why it matters
Keeps the stability threshold $0.01$ on the correct side of the quarantine wall so classification-stability talk can be preregistered without smuggling unproven numerics into the certified surface. The removal plan explicitly points at replacing the constant by a proved tight bound from an overlap-perturbation estimate, which is the intended path from data hypothesis to theorem. No downstream certified parents yet (unused); its role is infrastructural bookkeeping inside the measurement/verification layer rather than a step of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.