unitsFromAnchors_c
plain-language theorem explainer
The speed-of-light field of the units pack built from anchor data equals the speed computed directly from those anchors. Anyone simplifying calibrated RS units or rewriting display constants will cite this. The proof is pure reflexivity: the field is defined to be that speed.
Claim. For any anchor data $A$, if $U$ is the units pack constructed from $A$, then the speed-of-light component of $U$ equals the speed derived from $A$: $U.c = c(A)$.
background
RecogSpec packages the Recognition Science display layer: anchors fix reference scales, and a units pack carries the derived constants (tick $\tau_0$, length $\ell_0$, speed $c$, and related factors) used when comparing RS-native predictions to SI-facing bands.
speedFromAnchors extracts the speed scale implied by the anchors; unitsFromAnchors assembles the full units record from the same data. In RS-native units one often sets $c=1$, but here $c$ is the concrete ratio of the length and time anchors, so the pack must expose that ratio as its .c field.
Sibling projections (unitsFromAnchors_tau0, unitsFromAnchors_ell0) play the same role for the other base scales. Downstream calibration predicates (exact match to anchors, band membership) rely on these field equalities being definitional.
proof idea
One-line term proof by rfl. Unfolding unitsFromAnchors shows that its .c component is definitionally speedFromAnchors A, so the equality holds by construction. Marked @[simp] so rewrites and simp close goals that mention (unitsFromAnchors A).c without manual unfolding.
why it matters
Small but load-bearing glue in the RecogSpec calibration stack. Without a simp-normal form for the speed field, later lemmas about calibrated packs, unique calibration, and band membership would repeatedly unfold the units constructor.
It sits beside the $\tau_0$ and $\ell_0$ projections and supports the witness that a units pack exactly matches its anchors (including the ratio constraint). In the broader RS picture this is the display-side counterpart of fixing $c$ once length and time anchors are chosen; it does not itself force $c=1$ in native units, but it keeps the SI-facing speed consistent with the anchor ratio used throughout the verification bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.