quarkMassCompliance
plain-language theorem explainer
Registers the quark-masses physics module as calibration-compliant for verification audits: it has a seam note and lists only MeV among SI units. Auditors of the Recognition Science calibration policy cite this entry when checking which modules stay inside the dimensionless-vs-SI boundary. The body is a three-field structure literal, not a derived theorem.
Claim. The quark-masses module is recorded as calibration-compliant: a seam note is present, and the only SI unit used is $\mathrm{MeV}$.
background
The Calibration Policy module separates two classes of RS claims. Dimensionless predictions (ratios, exponents, ladder relations) follow from $\varphi=(1+\sqrt{5})/2$ alone and need no external scale. SI-anchored predictions need at least one external anchor (for example CODATA $\hbar$) before absolute numerics are meaningful.
Current Constants placeholders ($\hbar=1$, $G=1$, $c=1$) put the codebase in dimensionless-only mode: ratios are fair game; SI numerics are not claimed as zero-parameter outputs. Compliance records exist so audits can see, module by module, whether a seam note documents the boundary and which SI unit strings appear.
CalibrationCompliance is the audit record type: a module path string, a boolean for the seam note, and the list of SI unit labels used.
proof idea
Pure definition: a structure literal of type CalibrationCompliance with three fixed fields (module path Physics/QuarkMasses.lean, hasSeamNote := true, siUnitsUsed := ["MeV"]). No lemmas, tactics, or computation.
why it matters
Keeps the quark-mass ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) inside the verification story without overclaiming SI absolute scale. MeV values are flagged as unit-bearing, so they sit on the SI-anchored side of the policy unless an explicit single-anchor mode is adopted. No downstream theorems currently depend on this entry; it is an audit marker for the verification domain, not a step in the T0–T8 forcing chain. It documents that quark-mass work acknowledges the seam between $\varphi$-native ratios and laboratory energy units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.