SIAnchor
plain-language theorem explainer
An SI anchor packages one external laboratory constant (name, real value, provenance, unit string) used to fix absolute scale. Calibration and claim-language code cite it when moving from pure φ-ratios to SI numerics. It is a plain record type with no proof obligations.
Claim. An SI anchor is a 4-tuple $(n, v, s, u)$ with name $n$ a string, SI numerical value $v \in \mathbb{R}$, source string $s$ (e.g. CODATA 2022), and unit string $u$ (e.g. J·s). It records one externally supplied constant that sets absolute scale for SI-anchored predictions.
background
The CalibrationPolicy module separates two classes of RS output. Dimensionless predictions (ratios, exponents, φ-ladder relations) need no external input. SI-anchored predictions need at least one laboratory number to fix absolute scale; without it the codebase stays in placeholder units ($c=1$, $\hbar=1$, $G=1$).
An SI anchor is that external number, stored with provenance. The module doc states the policy fork: dimensionless-only mode treats all SI constants as inputs; single-anchor mode fixes exactly one (typically CODATA $\hbar$) and derives the rest via φ-based relations. Absolute scale is not yet forced internally from the Recognition Composition Law or the T0–T8 chain; the anchor is the honest external seam.
Related upstream “canonical” and “value” constructions elsewhere in the monolith supply forced measures or evaluated expressions; they do not replace this calibration record. The anchor is bookkeeping for verification claims, not a derived constant.
proof idea
No proof. The declaration is a structure (record type) with four fields: name, value, source, and unit. Field doc-comments fix the intended meaning; there are no constructors beyond the implicit structure constructor and no lemmas in the body.
why it matters
This type is the payload of single-anchor calibration. CalibrationMode’s SingleAnchor constructor carries an SIAnchor; hbar_anchor is the canonical instance (CODATA 2022 $\hbar = 1.054571817\times 10^{-34}$ J·s, exact under SI 2019). SIAnchoredPrediction stores the anchor used for each SI numeric claim, and singleAnchorClaim builds the honest English claim that RS derives other SI values from φ plus that one external constant.
In framework terms it marks the boundary between zero-parameter φ content (T5 J-uniqueness, T6 φ fixed point, mass ladder, α band) and dimensionful SI output. RS-native units set $\hbar = \varphi^{-5}$ and $G = \varphi^5/\pi$ with $c=1$; converting those to joule-seconds still needs one external scale. The structure makes that dependency explicit so verification does not overclaim “no external input” for SI numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.