IndisputableMonolith.RecogSpec.Bands

   1import Mathlib
   2import IndisputableMonolith.Verification.BridgeCore
   3
   4namespace IndisputableMonolith
   5namespace RecogSpec
   6
   7structure Band where
   8  lo : ℝ
   9  hi : ℝ
  10
  11def Band.width (b : Band) : ℝ := b.hi - b.lo
  12
  13abbrev Bands := List Band
  14
  15def Band.contains (b : Band) (x : ℝ) : Prop := b.lo ≤ x ∧ x ≤ b.hi
  16
  17def Band.Valid (b : Band) : Prop := b.lo ≤ b.hi
  18
  19lemma Band.contains_lo_of_valid (b : Band) (hb : Band.Valid b) :
  20  Band.contains b b.lo := by
  21  dsimp [Band.contains, Band.Valid] at *
  22  exact And.intro le_rfl hb
  23
  24lemma Band.contains_hi_of_valid (b : Band) (hb : Band.Valid b) :
  25  Band.contains b b.hi := by
  26  dsimp [Band.contains, Band.Valid] at *
  27  exact And.intro hb le_rfl
  28
  29lemma Band.width_nonneg (b : Band) (hb : Band.Valid b) : 0 ≤ b.width := by
  30  dsimp [Band.width, Band.Valid] at *
  31  exact sub_nonneg.mpr hb
  32
  33def wideBand (x : ℝ) (ε : ℝ) : Band := { lo := x - ε, hi := x + ε }
  34
  35lemma wideBand_width {x ε : ℝ} (hε : 0 ≤ ε) : (wideBand x ε).width = 2 * ε := by
  36  dsimp [Band.width, wideBand]
  37  ring
  38
  39lemma wideBand_width_nonneg {x ε : ℝ} (hε : 0 ≤ ε) : 0 ≤ (wideBand x ε).width := by
  40  have hw : (wideBand x ε).width = 2 * ε := wideBand_width (x:=x) (ε:=ε) hε
  41  have h2 : 0 ≤ (2 : ℝ) := by norm_num
  42  have hnonneg : 0 ≤ 2 * ε := mul_nonneg h2 hε
  43  simpa [hw] using hnonneg
  44
  45lemma wideBand_contains_center {x ε : ℝ} (hε : 0 ≤ ε) :
  46  Band.contains (wideBand x ε) x := by
  47  dsimp [Band.contains, wideBand]
  48  constructor
  49  · have : x - ε ≤ x := by simpa using sub_le_self x hε
  50    simpa using this
  51  ·
  52    have hx : x ≤ x + ε := by
  53      simpa using (le_add_of_nonneg_right hε : x ≤ x + ε)
  54    simpa using hx
  55
  56lemma wideBand_valid {x ε : ℝ} (hε : 0 ≤ ε) : (wideBand x ε).Valid := by
  57  dsimp [Band.Valid, wideBand]
  58  linarith
  59
  60lemma wideBand_contains_lo {x ε : ℝ} (hε : 0 ≤ ε) :
  61  Band.contains (wideBand x ε) (wideBand x ε).lo :=
  62  Band.contains_lo_of_valid _ (wideBand_valid (x:=x) (ε:=ε) hε)
  63
  64lemma wideBand_contains_hi {x ε : ℝ} (hε : 0 ≤ ε) :
  65  Band.contains (wideBand x ε) (wideBand x ε).hi :=
  66  Band.contains_hi_of_valid _ (wideBand_valid (x:=x) (ε:=ε) hε)
  67
  68@[simp] def sampleBandsFor (x : ℝ) : Bands := [wideBand x 1]
  69
  70lemma sampleBandsFor_nonempty (x : ℝ) : (sampleBandsFor x).length = 1 := by
  71  simp [sampleBandsFor]
  72
  73lemma sampleBandsFor_singleton (x : ℝ) : sampleBandsFor x = [wideBand x 1] := by
  74  simp [sampleBandsFor]
  75
  76@[simp] def evalBandsAt (c : ℝ) (x : ℝ) : Bands := sampleBandsFor (c * x)
  77
  78noncomputable def meetsBandsChecker_gen (xs : List ℝ) (bs : Bands) : Bool := by
  79  classical
  80  exact xs.any (fun x => bs.any (fun b => decide (Band.contains b x)))
  81
  82noncomputable def meetsBandsChecker (xs : List ℝ) (c : ℝ) : Bool :=
  83  meetsBandsChecker_gen xs (evalBandsAt c 1)
  84
  85/-- Evaluate whether the anchors `U.c` lie in any of the candidate bands `X`. -/
  86def evalToBands_c (U : IndisputableMonolith.Constants.RSUnits) (X : Bands) : Prop :=
  87  ∃ b ∈ X, Band.contains b U.c
  88
  89/-- Invariance of the c-band check under units rescaling (c fixed by cfix). -/
  90lemma evalToBands_c_invariant {U U' : IndisputableMonolith.Constants.RSUnits}
  91  (h : IndisputableMonolith.Verification.UnitsRescaled U U') (X : Bands) :
  92  evalToBands_c U X ↔ evalToBands_c U' X := by
  93  dsimp [evalToBands_c]
  94  have hc : U'.c = U.c := h.cfix
  95  constructor
  96  · intro hx
  97    rcases hx with ⟨b, hb, hbx⟩
  98    refine ⟨b, hb, ?_⟩
  99    simpa [Band.contains, hc] using hbx
 100  · intro hx
 101    rcases hx with ⟨b, hb, hbx⟩
 102    refine ⟨b, hb, ?_⟩
 103    simpa [Band.contains, hc.symm] using hbx
 104
 105/-- The centered `wideBand` around `U.c` always includes `U.c`. -/
 106lemma evalToBands_c_wideBand_center
 107  (U : IndisputableMonolith.Constants.RSUnits) (tol : ℝ) (htol : 0 ≤ tol) :
 108  evalToBands_c U [wideBand U.c tol] := by
 109  refine ⟨wideBand U.c tol, by simp, ?_⟩
 110  simpa using wideBand_contains_center (x:=U.c) (ε:=tol) htol
 111
 112/-- Convenience: `sampleBandsFor x` contains `x`, hence satisfies `evalToBands_c` with anchors `c=x`. -/
 113lemma evalToBands_c_sampleBandsFor
 114  (x : ℝ) : evalToBands_c { tau0 := 1, ell0 := x, c := x, c_ell0_tau0 := by simp } (sampleBandsFor x) := by
 115  refine ⟨wideBand x 1, ?_, ?_⟩
 116  · simp [sampleBandsFor]
 117  · simpa using wideBand_contains_center (x:=x) (ε:=1) (by norm_num)
 118
 119@[simp] lemma meetsBandsChecker_gen_nil (bs : Bands) :
 120  meetsBandsChecker_gen [] bs = false := by
 121  classical
 122  simp [meetsBandsChecker_gen]
 123
 124@[simp] lemma meetsBandsChecker_nil (c : ℝ) :
 125  meetsBandsChecker [] c = false := by
 126  classical
 127  simp [meetsBandsChecker, meetsBandsChecker_gen]
 128
 129@[simp] lemma meetsBandsChecker_gen_nilBands (xs : List ℝ) :
 130  meetsBandsChecker_gen xs [] = false := by
 131  classical
 132  simp [meetsBandsChecker_gen]
 133
 134lemma center_in_sampleBandsFor (x : ℝ) :
 135  ∃ b ∈ sampleBandsFor x, Band.contains b x := by
 136  refine ⟨wideBand x 1, ?_, ?_⟩
 137  · simp [sampleBandsFor]
 138  · have : Band.contains (wideBand x 1) x := wideBand_contains_center (x:=x) (ε:=1) (by norm_num)
 139    simpa using this
 140
 141lemma center_in_each_sample (x : ℝ) :
 142  ∀ {b}, b ∈ sampleBandsFor x → Band.contains b x := by
 143  intro b hb
 144  have hb' : b = wideBand x 1 := by
 145    simpa [sampleBandsFor] using hb
 146  simpa [hb'] using wideBand_contains_center (x:=x) (ε:=1) (by norm_num)
 147
 148/-! ### Dimension forcing via LCM arithmetic -/
 149
 150/-- The LCM of 2^D and 45 equals 360 if and only if D = 3.
 151    This is the arithmetic kernel of the "8↔45 hinge" dimension forcing argument. -/
 152theorem lcm_pow2_45_eq_iff (D : ℕ) : Nat.lcm (2 ^ D) 45 = 360 ↔ D = 3 := by
 153  constructor
 154  · intro h
 155    -- gcd(2^D, 45) = 1 for all D since 45 = 3² × 5 has no factors of 2
 156    -- Thus lcm(2^D, 45) = 2^D × 45
 157    -- 2^D × 45 = 360 ⟺ 2^D = 8 ⟺ D = 3
 158    have hgcd : Nat.gcd (2 ^ D) 45 = 1 := by
 159      have hcop : Nat.Coprime 2 45 := by native_decide
 160      exact Nat.Coprime.pow_left D hcop
 161    have hlcm : Nat.lcm (2 ^ D) 45 = 2 ^ D * 45 / Nat.gcd (2 ^ D) 45 := Nat.lcm_eq_mul_div (2 ^ D) 45
 162    rw [hgcd, Nat.div_one] at hlcm
 163    rw [hlcm] at h
 164    have h8eq : 2 ^ D = 8 := by omega
 165    have : 2 ^ D = 2 ^ 3 := by simp at h8eq ⊢; exact h8eq
 166    exact Nat.pow_right_injective (by norm_num : 1 < 2) this
 167  · intro hD
 168    subst hD
 169    native_decide
 170
 171end RecogSpec
 172end IndisputableMonolith
 173