unitsFromAnchors
plain-language theorem explainer
Given laboratory anchors (a fundamental tick and a fundamental length), this builds the matching RS units pack: time unit, length unit, speed of light, and the light-cone identity. Calibration and uniqueness lemmas cite it as the canonical units witness from anchors. The body is a structure instance whose only nontrivial field is a short case split on the speed-from-anchors formula.
Claim. For anchors $A=(a_1,a_2)$, the associated RS units pack has $\tau_0=a_1$, $\ell_0=a_2$, and $c$ equal to the speed extracted from $A$, and satisfies the light-cone identity $c\cdot\tau_0=\ell_0$.
background
In Recognition Science, physical units are packaged as an RSUnits record: a tick duration $\tau_0$, a fundamental length $\ell_0$ (voxel scale), a speed $c$, and a proof of the light-cone identity $c\cdot\tau_0=\ell_0$. In RS-native units one often takes $\ell_0=1$ and $\tau_0$ equal to the fundamental tick, so $c=\ell_0/\tau_0$ holds by definition; here the same identity is required for arbitrary laboratory anchors.
Anchors supply two real parameters $a_1$ and $a_2$ interpreted as the chosen tick and length. The sibling map that extracts speed from anchors returns $0$ when the tick vanishes and $a_2/a_1$ otherwise, so the light-cone relation is forced whenever the tick is nonzero. The module sits in the RecogSpec layer that turns abstract ledgers and bridges into concrete, band-checked numerical claims.
proof idea
Structure constructor for RSUnits. Set $\tau_0:=A.a_1$ and $\ell_0:=A.a_2$ by projection. Set $c$ to the speed extracted from the same anchors. The identity $c\cdot\tau_0=\ell_0$ is discharged by unfolding that speed map and splitting on whether the tick is zero: the zero branch is immediate by simplification; the nonzero branch is a one-line field simplification of $a_2/a_1\cdot a_1=a_2$.
why it matters
This is the canonical map from laboratory anchors to an RS units pack. Downstream, the calibration witness unitsFromAnchors_calibrated and the simp lemmas for $\tau_0$, $\ell_0$, and $c$ are immediate unfoldings of it. The uniqueness lemma uniqueCalibration_any uses it as the explicit units pack that matches any ledger/bridge/anchors triple, so absolute-layer calibration is inhabited for every anchor choice.
Verification certificates (UnitsFromAnchorsRescaleCert, AnchorsRescaleEqvCert) rely on the same construction to show that rescaling anchors induces the expected units rescaling and that anchors related by positive scale are equivalent. In the broader framework it is the bridge from the abstract light-cone identity $\ell_0=c\cdot\tau_0$ (Constants layer) to the RecogSpec absolute layer that feeds band checks and two-outcome Born certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.