IndisputableMonolith.Verification.MetricFromUnitsCert

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.RecogSpec.Spec
   4
   5/-!
   6# Metric-from-Units Certificate (Minkowski / light-cone)
   7
   8This module provides a **non-scaffold** first milestone for the “Ledger ⇒ Metric”
   9bridge checklist:
  10
  11- define a minimal 4D “metric” interface (symmetric bilinear evaluation),
  12- instantiate it with the Minkowski metric determined by a speed parameter `c`,
  13- and prove the **light-cone/null** condition for the anchor vector `(τ₀, ℓ₀, 0, 0)`
  14  using the RS cone-bound identity `c · τ₀ = ℓ₀`.
  15
  16No imports from `Relativity/Geometry/*` are used.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Verification
  21namespace MetricFromUnits
  22
  23open IndisputableMonolith.Constants
  24
  25/-! ### Minimal 4-vector and metric interface -/
  26
  27structure Vec4 where
  28  t : ℝ
  29  x : ℝ
  30  y : ℝ
  31  z : ℝ
  32
  33/-- Minimal symmetric “metric” interface: an evaluation pairing plus symmetry. -/
  34structure Metric4 where
  35  eval : Vec4 → Vec4 → ℝ
  36  symm : ∀ v w : Vec4, eval v w = eval w v
  37
  38/-! ### Minkowski metric determined by speed `c` -/
  39
  40/-- Minkowski bilinear evaluation with signature `(-c^2, +1, +1, +1)` in coordinates
  41`(t, x, y, z)`. -/
  42def minkowskiEval (c : ℝ) (v w : Vec4) : ℝ :=
  43  -(c ^ 2) * v.t * w.t + v.x * w.x + v.y * w.y + v.z * w.z
  44
  45lemma minkowskiEval_symm (c : ℝ) (v w : Vec4) : minkowskiEval c v w = minkowskiEval c w v := by
  46  unfold minkowskiEval
  47  ring
  48
  49/-- The Minkowski `Metric4` instance at speed `c`. -/
  50def minkowskiMetric (c : ℝ) : Metric4 :=
  51  { eval := minkowskiEval c, symm := minkowskiEval_symm c }
  52
  53/-- Quadratic form induced by a metric. -/
  54def normSq (g : Metric4) (v : Vec4) : ℝ :=
  55  g.eval v v
  56
  57/-! ### Light-cone/null anchor vector -/
  58
  59/-- Anchor vector `(τ, ℓ, 0, 0)` extracted from RS units. -/
  60def anchorsVec (U : RSUnits) : Vec4 :=
  61  { t := U.tau0, x := U.ell0, y := 0, z := 0 }
  62
  63lemma anchorsVec_null_of_cone (c τ ℓ : ℝ) (h : c * τ = ℓ) :
  64    normSq (minkowskiMetric c) { t := τ, x := ℓ, y := 0, z := 0 } = 0 := by
  65  unfold normSq minkowskiMetric minkowskiEval
  66  -- reduce to `-(c^2)*τ^2 + ℓ^2 = 0` and rewrite `ℓ = c*τ`
  67  simp [pow_two, h.symm]
  68  ring
  69
  70/-- The anchor vector is null for every RSUnits pack (by the built-in cone bound). -/
  71lemma anchorsVec_null (U : RSUnits) :
  72    normSq (minkowskiMetric U.c) (anchorsVec U) = 0 := by
  73  -- RSUnits contains the cone bound `c * τ0 = ℓ0` as a field.
  74  simpa [anchorsVec] using anchorsVec_null_of_cone U.c U.tau0 U.ell0 U.c_ell0_tau0
  75
  76/-! ### Certificate -/
  77
  78structure MetricFromUnitsCert where
  79  deriving Repr
  80
  81/-- Verification predicate: Minkowski metric built from RS units has a null anchor vector. -/
  82@[simp] def MetricFromUnitsCert.verified (_c : MetricFromUnitsCert) : Prop :=
  83  ∀ U : RSUnits, normSq (minkowskiMetric U.c) (anchorsVec U) = 0
  84
  85@[simp] theorem MetricFromUnitsCert.verified_any (c : MetricFromUnitsCert) :
  86    MetricFromUnitsCert.verified c := by
  87  intro U
  88  exact anchorsVec_null U
  89
  90end MetricFromUnits
  91end Verification
  92end IndisputableMonolith
  93