calibrationSummary
plain-language theorem explainer
Static inventory of five calibration knobs used in the quarantined measurement layer: classify and stability thresholds plus the network, projection, and energy control constants, each paired with its numeric value and provenance source tag. Auditors of the empirical/certified boundary cite it to see which numbers sit outside theorem-level claims. The body is a literal list that reads source strings off the raw MeasurementResult wrappers.
Claim. The calibration summary is the finite list of triples $(\mathrm{name},\,\mathrm{value},\,\mathrm{source})$ for five constants: classify threshold $0.9$, stability threshold $0.01$, network control $C_{\mathrm{net}}=1.0$, projection bound $C_{\mathrm{proj}}=2.0$, and energy control $C_{\mathrm{eng}}=2.5$, each tagged by the provenance source of its raw measurement wrapper.
background
The surrounding module is the quarantine layer for empirical inputs. Certified (theorem-level) claims must not import raw data; every measured number, calibration constant, or mined dataset is wrapped in a provenance record that names source, hash or generator, and date. Measurement results carry a value, optional uncertainty, and that provenance; hypotheses built from data are explicitly marked so they cannot silently enter the certified surface.
The five entries here are the local calibration constants of that layer. The projection bound $C_{\mathrm{proj}}=2$ is the CPM operator-norm bound on the ILG projection kernel. The energy control $C_{\mathrm{eng}}=2.5$ is recorded as an empirical diagnostic value with uncertainty $0.2$. Network control $C_{\mathrm{net}}$, the classify threshold $0.9$, and the stability threshold $0.01$ are the remaining knobs, each stored as a raw measurement result with its own provenance tag.
Upstream gravity analysis modules use a similar provenance string pattern (what is derived in Lean versus what is assumed) so a reader cannot mistake a tag for a theorem. This summary is the measurement-side counterpart: a single table of names, values, and sources.
proof idea
Definition by list literal, not a proof. Each triple hard-codes the constant name and its decimal value string, then pulls the source field from the corresponding raw measurement wrapper (classifyThreshold_raw, stabilityThreshold_raw, C_net_raw, C_proj_raw, C_eng_raw) via the provenance record's source, rendered with toString. No lemmas are applied; the #eval is disabled because real numbers are not computable in this context.
why it matters
Keeps the empirical/certified split auditable. The module doc requires that modules under Verification/Measurement/* stay quarantined and that the certified surface never import them; this summary is the human-readable ledger of which calibration numbers live in that quarantine and where they came from.
It does not feed a parent theorem (no downstream uses yet). Its role is infrastructural: anyone checking coercive-projection or CPM energy-control claims can see at a glance that $C_{\mathrm{proj}}$ and $C_{\mathrm{eng}}$ are tagged as calibrated or paper-derived data rather than Lean-proved constants. That matches the broader Recognition pattern of separating forcing-chain theorems (T0–T8, RCL, $\varphi$-ladder) from measurement scaffolding.
If a later preregistered test or hypothesis bridge needs to cite the full calibration set, this list is the single source of names and provenance strings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.