IndisputableMonolith.RecogSpec.Anchors

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace RecogSpec
   5
   6/-- Measurement anchors (minimal interface used by band checks). -/
   7structure Anchors where
   8  a1 : ℝ
   9  a2 : ℝ
  10  /-- Calibration consistency: if the time anchor vanishes, the length anchor must
  11      also vanish so that `c * tau0 = ell0` remains solvable. -/
  12  consistent : a1 = 0 → a2 = 0
  13
  14namespace Anchors
  15
  16@[simp] lemma consistent_zero (A : Anchors) : A.a1 = 0 → A.a2 = 0 :=
  17  A.consistent
  18
  19end Anchors
  20
  21end RecogSpec
  22end IndisputableMonolith
  23