electronMassCompliance
plain-language theorem explainer
Audit record stating that the electron-mass module is calibration-compliant: it carries an explicit seam note and reports MeV as its only SI unit. Verification and release reviewers cite it when checking that mass numerics are flagged as SI-anchored rather than pure φ predictions. The body is a literal structure value, not a proof.
Claim. The electron-mass physics module is recorded as calibration-compliant: path $\texttt{Physics/ElectronMass/Defs.lean}$, seam note present, and SI units used equal to $\{\mathrm{MeV}\}$.
background
The Calibration Policy module separates two classes of RS claims. 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 laboratory units.
CalibrationCompliance is a small audit structure: which module path is checked, whether a seam note documents the dimensionless/SI boundary, and which SI unit strings appear. Electron mass sits on the $\varphi$-ladder mass formula (yardstick times $\varphi$ to a rung offset), so any MeV figure is SI-facing and must be marked as such.
Current Constants placeholders ($\hbar=1$, $G=1$, $c=1$) keep the stack in dimensionless-only mode until an anchor policy is chosen.
proof idea
Not a proof. The definition is a one-shot structure literal of type CalibrationCompliance: module path string, hasSeamNote := true, and siUnitsUsed := ["MeV"]. No lemmas or tactics.
why it matters
Electron mass is a flagship RS mass-ladder output; MeV values are the usual experimental contact point. This compliance entry forces that contact to stay inside the calibration policy: seam-documented and unit-tagged, not silently treated as a zero-parameter $\varphi$-only claim.
It supports the module's dimensionless-only versus single-anchor distinction and the audit list of calibrated modules. No downstream theorems currently depend on it; it is infrastructure for verification reviews rather than a step in the T0–T8 forcing chain. It does not fix the absolute scale or choose the anchor; it only records how the electron-mass file presents its SI face.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.