CalibrationCompliance
plain-language theorem explainer
Audit record for whether a physics module obeys the calibration policy: which file it is, whether it documents the SI seam, and which SI units it touches. Mass-sector compliance entries (quarks, neutrinos, electron) instantiate it. Pure data structure; no proof.
Claim. A calibration-compliance record is a triple $(M, s, U)$ where $M$ is a module path string, $s$ is a boolean flag that the module carries an explicit SI-seam note, and $U$ is the list of SI unit labels (e.g.\ MeV, eV) appearing in that module's predictions.
background
The Calibration Policy module separates two kinds of RS claims. Dimensionless predictions are ratios, exponents, and $\varphi$-ladder relations fixed by $\varphi=(1+\sqrt{5})/2$ alone (zero external parameters). SI-anchored predictions need at least one external scale (e.g.\ 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). Absolute internal scale-fixing is not yet formalized.
This structure is the audit row used to check that mass modules declare their SI seam and list the units they emit, rather than silently mixing dimensionless RS output with SI numerics.
proof idea
No proof: the declaration is a structure (record type) with three fields. Downstream values are literal constructors filling module, hasSeamNote, and siUnitsUsed.
why it matters
Gives a uniform audit type for the verification layer so mass modules can be checked against the dimensionless-vs-SI policy. Instantiated by quarkMassCompliance, neutrinoCompliance, and electronMassCompliance, each tagging a Physics module path, affirming a seam note, and listing MeV or eV.
In the broader RS picture this guards the boundary between $\varphi$-ladder mass formulas (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and SI reporting. Without such records, SI units could be claimed under dimensionless-only mode, which the module doc explicitly forbids until an anchor or internal scale mechanism exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.