calibratedModules
plain-language theorem explainer
Static registry of Lean modules that emit SI-unit numerics and are expected to carry explicit calibration documentation. Auditors of the dimensionless-vs-SI policy cite it when checking which physics files may claim absolute scales. The body is a three-entry string list, not a proved claim.
Claim. The modules treated as SI-calibrated (and therefore required to document their external anchor) are the electron-mass definitions, the quark-mass sector, and the neutrino sector.
background
The CalibrationPolicy module separates two kinds of RS output. Dimensionless predictions are ratios and exponents fixed by $\varphi=(1+\sqrt{5})/2$ alone. SI-anchored predictions need at least one external scale (for example a CODATA $\hbar$) before they become numbers in SI units.
Policy modes are dimensionless-only (current Constants placeholders $c=\hbar=G=1$) versus single-anchor (fix one SI constant, derive the rest via $\varphi$-relations). Modules that still print SI numerics must be listed and audited so claims do not silently mix the two modes.
Upstream "Calibration" notions in CostAxioms and CostFromDistinction normalize cost curvature or pin a distinguished inconsistent configuration; they are the mathematical sense of fixing a scale, not this registry itself.
proof idea
Definitional constant: a List String literal with three module paths. No tactics, no lemmas, no computation. Downstream compliance checks are expected to read this list rather than hard-code paths.
why it matters
Keeps the verification layer honest about which physics files may claim SI values. The module doc states that true SI predictions either accept an external anchor (breaking zero external input) or need an internal absolute-scale mechanism not yet formalized. This list is the audit hook for that boundary: electron mass, quarks, and neutrinos are the sectors currently flagged as SI-facing.
No downstream theorems yet depend on it (used_by empty). It supports the sibling compliance surface (CalibrationCompliance and the dimensionless-only / single-anchor claims) rather than a forcing-chain step (T0–T8). Landmark contact is policy hygiene around $\varphi$-native constants versus SI anchors, not a new physical derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.