Calibrated
plain-language theorem explainer
A units pack is calibrated to a pair of anchors when its tick, length, and speed equal the anchor values and the speed forced by those anchors. Spec and uniqueness arguments cite this as the exact-match predicate between laboratory anchors and an RSUnits triple. The body is a three-conjunct propositional definition, not a proved theorem.
Claim. A units pack $U=(\tau_0,\ell_0,c)$ is calibrated to anchors $A=(a_1,a_2)$ when $\tau_0=a_1$, $\ell_0=a_2$, and $c$ equals the speed extracted from $A$ (the ratio constraint implied by the anchors).
background
RecogSpec packages the bridge from external measurement anchors into RS-native units. An Anchors value supplies two positive reals $(a_1,a_2)$ standing for a chosen tick duration and length scale. The structure RSUnits is the minimal pack $(\tau_0,\ell_0,c)$ with the structural law $c\cdot\tau_0=\ell_0$.
In RS-native conventions the fundamental length is the voxel scale $\ell_0$ and the fundamental time is one tick $\tau_0$; the speed $c$ is then fixed by the product law. Sibling helpers speedFromAnchors and unitsFromAnchors build the unique pack (when defined) whose tick and length match the anchors and whose $c$ is the induced ratio.
Upstream constants modules supply the default RS values of $\tau_0$ and $\ell_0$ and the CODATA-linked derivations used when anchors are taken from SI data. Calibration is the exact equality witness that a candidate pack sits on those anchors, including the ratio constraint.
proof idea
Definitional, not a proof. The predicate is the conjunction of three equalities: the pack's tick equals the first anchor, its length equals the second anchor, and its speed equals speedFromAnchors applied to the same anchors. No lemmas are invoked; the body is pure propositional packaging of that match.
why it matters
Calibration is the gate between laboratory anchors and every uniqueness or rigidity argument that needs a fixed units pack. Downstream, character-rigidity and cost-uniqueness developments (doubled-trace rigidity, generated $J$-cost formula, prime-calibrated mixed-pair and composite-defect characters) quantify over or assume calibrated ratio characters and packs; the d'Alembert/RCL uniqueness thread likewise needs a fixed bilinear display once units are pinned.
In the Recognition chain this sits under the constants and bridge layer that feeds T5 $J$-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$: without an exact anchor match, native displays of $c$, $\hbar$, and $G$ cannot be compared to SI bands. Sibling UniqueCalibration and unitsFromAnchors_calibrated close the existence/uniqueness side of the same interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.