consistent_zero
plain-language theorem explainer
Anchors supply a minimal interface of time and length components for band checks. The lemma asserts that vanishing of the time anchor forces the length anchor to vanish under the built-in calibration rule. Researchers simplifying expressions in anchor-based consistency arguments cite the simp-tagged result. The proof is a direct one-line projection onto the consistent field of the structure.
Claim. For any anchor structure $A$ with real components $a_1$ (time) and $a_2$ (length), $a_1 = 0$ implies $a_2 = 0$.
background
The Anchors structure is defined as a pair of real numbers $a_1$ and $a_2$ equipped with a consistency predicate. Its documentation states that the predicate encodes calibration consistency: if the time anchor vanishes, the length anchor must also vanish so that $c * tau0 = ell0$ remains solvable. The module RecogSpec.Anchors supplies this minimal interface for band checks in the Recognition Science setting.
proof idea
The proof is a one-line term wrapper that directly applies the consistent field of the supplied anchor structure A.
why it matters
The lemma supplies a simp rule that closes the minimal anchor interface used by band checks. It directly implements the calibration consistency stated in the Anchors documentation. No downstream theorems are recorded yet, leaving the result available for future simplifications in anchor-dependent arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.