IndisputableMonolith.Verification.UnitsRescaledLawsCert

   1import Mathlib
   2import IndisputableMonolith.Verification.BridgeCore
   3
   4/-!
   5# UnitsRescaled Laws Certificate
   6
   7This audit certificate records basic **closure properties** of the anchor-rescaling
   8relation `Verification.UnitsRescaled`:
   9
  10- reflexivity (every units pack is rescaled to itself),
  11- symmetry (rescalings can be inverted),
  12- transitivity (rescalings compose).
  13
  14Because `UnitsRescaled` is a `Type` (a structure), the certificate records these
  15laws at the `Prop` level via `Nonempty`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Verification
  20namespace UnitsRescaledLaws
  21
  22open IndisputableMonolith.Constants
  23
  24structure UnitsRescaledLawsCert where
  25  deriving Repr
  26
  27@[simp] def UnitsRescaledLawsCert.verified (_c : UnitsRescaledLawsCert) : Prop :=
  28  -- refl
  29  (∀ U : RSUnits, Nonempty (UnitsRescaled U U))
  30  ∧
  31  -- symm
  32  (∀ {U U' : RSUnits}, Nonempty (UnitsRescaled U U') → Nonempty (UnitsRescaled U' U))
  33  ∧
  34  -- trans
  35  (∀ {U U' U'' : RSUnits},
  36      Nonempty (UnitsRescaled U U') →
  37      Nonempty (UnitsRescaled U' U'') →
  38        Nonempty (UnitsRescaled U U''))
  39
  40@[simp] theorem UnitsRescaledLawsCert.verified_any (c : UnitsRescaledLawsCert) :
  41    UnitsRescaledLawsCert.verified c := by
  42  refine And.intro ?refl (And.intro ?symm ?trans)
  43  · intro U
  44    exact ⟨UnitsRescaled.refl U⟩
  45  · intro U U' h
  46    rcases h with ⟨hUU'⟩
  47    exact ⟨UnitsRescaled.symm hUU'⟩
  48  · intro U U' U'' h₁ h₂
  49    rcases h₁ with ⟨hUU'⟩
  50    rcases h₂ with ⟨hU'U''⟩
  51    exact ⟨UnitsRescaled.trans hUU' hU'U''⟩
  52
  53end UnitsRescaledLaws
  54end Verification
  55end IndisputableMonolith
  56
  57