Anchors
plain-language theorem explainer
The Anchors structure defines a minimal pair of real numbers a1 and a2 equipped with the implication that a1 = 0 forces a2 = 0. Researchers performing band checks in the Recognition Spec module cite this definition to keep length and time anchors compatible with the relation c * tau0 = ell0. The declaration is a direct structure definition whose content consists solely of the two fields and the consistency predicate.
Claim. A pair of real numbers $a_1, a_2$ such that $a_1 = 0$ implies $a_2 = 0$, serving as the minimal interface for length and time measurement anchors.
background
In the RecogSpec.Anchors module the structure supplies the minimal interface for band checks. Fields a1 and a2 record the length anchor ell0 and time anchor tau0 drawn from Constants and Constants.Derivation. Upstream, tau0 is the fundamental tick duration defined as sqrt(hbar G / (pi c^3)) / c while ell0 equals c * tau0; the consistent field enforces that the product remains solvable when either anchor vanishes.
proof idea
The declaration is a structure definition that directly introduces the two real fields together with the implication as a structure field. No lemmas or tactics are applied.
why it matters
Anchors supplies the interface projected by the downstream lemma consistent_zero in the same module. It maintains calibration consistency between ell0 and tau0, supporting the forcing chain steps that fix D = 3 and the eight-tick octave while preserving the relation among fundamental constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.