IndisputableMonolith.Constants.GapWeightNumericsScaffold

   1import Mathlib
   2import IndisputableMonolith.Constants.GapWeight
   3import IndisputableMonolith.Numerics.Interval.W8Bounds
   4
   5namespace IndisputableMonolith
   6namespace Constants
   7
   8/-! ## Gap Weight Numeric Match Certificate -/
   9
  10/-- The gap weight derived from DFT-8 matches the expected value within tolerance. -/
  11theorem w8_matches_certified :
  12    (2.490564399 : ℝ) < w8_from_eight_tick ∧ w8_from_eight_tick < (2.490572090 : ℝ) := by
  13  constructor
  14  · exact Numerics.W8Bounds.w8_computed_gt
  15  · exact Numerics.W8Bounds.w8_computed_lt
  16
  17/-- Compatibility alias for legacy code (with approximate equality). -/
  18theorem w8_value : abs (w8_from_eight_tick - 2.490569275454) < 5e-6 := by
  19  -- Follows from the verified interval bounds
  20  have h := w8_matches_certified
  21  rw [abs_lt]
  22  constructor <;> linarith
  23
  24end Constants
  25end IndisputableMonolith
  26