unitsFromAnchors_tau0
plain-language theorem explainer
The fundamental tick duration extracted from measurement anchors equals the first anchor value a1 by definition. Anyone simplifying calibrated RS units or band checks cites this. The proof is pure reflexivity: unitsFromAnchors stores a1 as tau0.
Claim. For any measurement anchors $A=(a_1,a_2)$ (with the consistency side-condition that $a_1=0$ forces $a_2=0$), the fundamental tick duration of the units built from $A$ equals $a_1$: $\tau_0(U(A))=a_1$.
background
RecogSpec packages the minimal measurement interface used by band checks. Anchors is a two-real structure $(a_1,a_2)$ together with the solvability constraint that a vanishing time anchor forces a vanishing length anchor, so $c,\tau_0=\ell_0$ remains well-posed.
In RS-native units the fundamental tick duration $\tau_0$ is the duration of one recognition tick (also written as the constant tick in the Constants layer). The map that builds a units record from anchors is definitional: it installs $a_1$ as $\tau_0$ and derives the remaining display quantities (length unit, speed) from the pair $(a_1,a_2)$.
Sibling projections record the same pattern for $\ell_0$ and $c$. The present lemma is the $\tau_0$ component of that interface.
proof idea
One-line reflexivity. The constructor unitsFromAnchors sets the tau0 field of the resulting units record equal to A.a1 by definition, so the equality holds by rfl. The @[simp] attribute makes the reduction fire automatically in later goals.
why it matters
Calibration of RS display units begins by reading the time anchor into $\tau_0$. Without this simp fact, every band check and uniqueness argument that mentions calibrated units would have to unfold the constructor by hand.
In the broader framework $\tau_0$ is the temporal yardstick tied to the eight-tick octave (T7) and to the RS-native constants ($c=1$, $\hbar=\varphi^{-5}$). Anchoring it to a measured $a_1$ is the first step that lets abstract phi-ladder predictions meet laboratory bands.
No downstream theorems currently list this lemma as a direct dependency in the graph, but the sibling suite (unitsFromAnchors_ell0, unitsFromAnchors_c, unitsFromAnchors_calibrated, UniqueCalibration) forms the local calibration API that MeetsBands and AnchorsEqv rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.