IndisputableMonolith.Verification.UnitsFromAnchorsRescaleCert

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Spec
   3
   4/-!
   5# Units-from-Anchors Rescaling Certificate
   6
   7This audit certificate records that rescaling anchors by a positive factor `s`
   8corresponds to a `Verification.UnitsRescaled` relation between the resulting
   9`RSUnits` packs (with `c` fixed).
  10
  11This makes the “units are only defined up to scale” invariance explicit in the
  12certified surface.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Verification
  17namespace UnitsFromAnchorsRescale
  18
  19open IndisputableMonolith.RecogSpec
  20
  21/-- Rescale anchors by a factor `s` (scaling both a1 and a2).
  22
  23The consistency field is preserved because `a1 = 0 → a2 = 0` implies
  24`s*a1 = 0 → s*a2 = 0`. -/
  25def rescaleAnchors (s : ℝ) (A : RecogSpec.Anchors) : RecogSpec.Anchors :=
  26{ a1 := s * A.a1
  27  a2 := s * A.a2
  28  consistent := by
  29    intro h
  30    by_cases hs : s = 0
  31    · simp [hs]
  32    · have ha1 : A.a1 = 0 := by
  33        -- from s*a1=0 and s≠0
  34        have : s = 0 ∨ A.a1 = 0 := mul_eq_zero.mp h
  35        cases this with
  36        | inl hs0 => exact (hs hs0).elim
  37        | inr ha1 => exact ha1
  38      have ha2 : A.a2 = 0 := A.consistent ha1
  39      simp [ha2] }
  40
  41private lemma speedFromAnchors_rescale (A : RecogSpec.Anchors) (s : ℝ) (hs : 0 < s) :
  42    RecogSpec.speedFromAnchors (rescaleAnchors s A) = RecogSpec.speedFromAnchors A := by
  43  have hs0 : s ≠ 0 := ne_of_gt hs
  44  by_cases hA : A.a1 = 0
  45  · -- degenerate anchors: both speeds are 0
  46    have hA' : (rescaleAnchors s A).a1 = 0 := by simp [rescaleAnchors, hA]
  47    simp [RecogSpec.speedFromAnchors, hA, hA', rescaleAnchors]
  48  · have hA' : (rescaleAnchors s A).a1 ≠ 0 := by
  49      -- s*a1 ≠ 0
  50      simp [rescaleAnchors, hs0, hA]
  51    -- compute both speeds on the nondegenerate branch and cancel `s`
  52    have hsA : RecogSpec.speedFromAnchors (rescaleAnchors s A) =
  53        (rescaleAnchors s A).a2 / (rescaleAnchors s A).a1 :=
  54      RecogSpec.speedFromAnchors_of_ne_zero (A := rescaleAnchors s A) hA'
  55    have hA0 : RecogSpec.speedFromAnchors A = A.a2 / A.a1 :=
  56      RecogSpec.speedFromAnchors_of_ne_zero (A := A) hA
  57    -- simplify the ratio
  58    have hcancel : (s * A.a2) / (s * A.a1) = A.a2 / A.a1 := by
  59      field_simp [hs0, hA]
  60    -- finish
  61    calc
  62      RecogSpec.speedFromAnchors (rescaleAnchors s A)
  63          = (rescaleAnchors s A).a2 / (rescaleAnchors s A).a1 := hsA
  64      _ = (s * A.a2) / (s * A.a1) := by simp [rescaleAnchors]
  65      _ = A.a2 / A.a1 := hcancel
  66      _ = RecogSpec.speedFromAnchors A := hA0.symm
  67
  68private def unitsFromAnchors_unitsRescaled (A : RecogSpec.Anchors) (s : ℝ) (hs : 0 < s) :
  69    Verification.UnitsRescaled (RecogSpec.unitsFromAnchors A) (RecogSpec.unitsFromAnchors (rescaleAnchors s A)) := by
  70  refine
  71    { s := s
  72      hs := hs
  73      tau0 := by simp [RecogSpec.unitsFromAnchors, rescaleAnchors]
  74      ell0 := by simp [RecogSpec.unitsFromAnchors, rescaleAnchors]
  75      cfix := by
  76        -- c = speedFromAnchors is invariant under rescaling
  77        simp [RecogSpec.unitsFromAnchors, speedFromAnchors_rescale (A := A) (s := s) hs] }
  78
  79structure UnitsFromAnchorsRescaleCert where
  80  deriving Repr
  81
  82@[simp] def UnitsFromAnchorsRescaleCert.verified (_c : UnitsFromAnchorsRescaleCert) : Prop :=
  83  ∀ (A : RecogSpec.Anchors) (s : ℝ), 0 < s →
  84    Nonempty
  85      (Verification.UnitsRescaled
  86        (RecogSpec.unitsFromAnchors A)
  87        (RecogSpec.unitsFromAnchors (rescaleAnchors s A)))
  88
  89@[simp] theorem UnitsFromAnchorsRescaleCert.verified_any (c : UnitsFromAnchorsRescaleCert) :
  90    UnitsFromAnchorsRescaleCert.verified c := by
  91  intro A s hs
  92  exact ⟨unitsFromAnchors_unitsRescaled (A := A) (s := s) hs⟩
  93
  94end UnitsFromAnchorsRescale
  95end Verification
  96end IndisputableMonolith
  97