C_eng_raw
plain-language theorem explainer
Packages the CPM energy control constant as an empirical measurement: value 2.5 with uncertainty 0.2 and calibrated provenance from energy diagnostic runs (2026-01-06). Citation target for anyone auditing quarantine of CPM calibration numbers. Construction is a plain MeasurementResult record literal; no proof content.
Claim. The energy control constant for CPM is the measurement result with value $2.5$, optional uncertainty $0.2$, and calibrated data provenance sourced from empirical diagnostic runs (dated 2026-01-06, labeled energy diagnostic analysis).
background
The module is quarantine infrastructure for empirical inputs. Certified theorem-level claims must not import raw measurements; every constant, threshold, or mined datum is wrapped so provenance (source, date, method) travels with the number. Modules under Verification/Measurement/* are quarantined; only preregistered test suites may mix them with the certified surface.
MeasurementResult α is the wrapper: a value of type α, an optional real uncertainty, and a DataProvenance record. Sibling raw constants in the same file (C_net_raw, C_proj_raw, classify/stability thresholds) follow the same pattern. The type of the value here is real energy in the RS-native sense (Energy := ℝ).
Upstream calibration language in the foundation (second-derivative normalization of the cost at the log-origin, or distinguished inconsistent configurations with fixed positive cost) is not invoked by this definition; the name "energy control constant" is an empirical CPM dial, not a derivation from the J-cost axioms.
proof idea
Definition only: a structure literal for MeasurementResult ℝ. Fields are set to value 2.5, uncertainty some 0.2, and provenance built by the calibrated constructor with three string arguments (source blurb, date, method label). No tactics, no lemmas, no computation.
why it matters
Feeds the in-module calibrationSummary, which lists all CPM calibration constants with provenance strings; the summary entry for energy is ("C_eng", "2.5", ...) drawn from this record. Keeps the energy dial outside the certified surface so theorem claims cannot silently depend on a floating empirical number.
It does not sit on the T0–T8 forcing chain, the Recognition Composition Law, or the phi-ladder mass formula. Its role is audit hygiene: every empirical CPM constant is named, dated, and tagged before any hypothesis bridge (HypothesisFromData) can promote it toward a conditional claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.