C_proj_raw
plain-language theorem explainer
Records the CPM projection constant as the real value 2.0, with no uncertainty and manual provenance citing a rank-one Hermitian bound (dated 2026-01-06). Anyone assembling the quarantined calibration table cites this entry. The body is a structure literal: value, optional error, and a DataProvenance.manual tag.
Claim. The CPM projection constant is the measurement result with value $2.0$, empty uncertainty, and manual provenance labeled "Rank-one Hermitian bound" on $2026$-$01$-$06$.
background
The module is the quarantine layer for empirical and calibration numbers. Certified theorem surfaces must not import raw measurements; every such number is wrapped so source, date, and optional error stay attached and auditable.
MeasurementResult packages three fields: the measured value (here a real), an optional uncertainty, and a DataProvenance record. Manual provenance is the explicit non-mined path: a human-supplied citation string and date rather than a generator hash.
Sibling raw constants in the same file (C_net, stability and classify thresholds, energy control) follow the same pattern. The numeric $2.0$ is the conventional rank-one Hermitian projection bound used as a CPM control constant, not a derived RS ladder quantity.
proof idea
Definition only: a structure literal for MeasurementResult ℝ. Sets value to $2.0$, uncertainty to none, and provenance to DataProvenance.manual with the citation string and date. No lemmas, tactics, or computation.
why it matters
Keeps the CPM projection scale inside the measurement quarantine so the certified surface never hard-codes a bare float. Downstream, calibrationSummary lists it as the C_proj row (value $2.0$ plus provenance source string) alongside net, energy, and threshold constants. That summary is the audit table for preregistered tests that may import quarantined modules while theorem-level claims may not. It does not itself sit on the T0–T8 forcing chain; it is bookkeeping for control constants used when checking projection bounds in the measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.