IndisputableMonolith.Verification.AnchorsRescaleEqvCert

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Spec
   3import IndisputableMonolith.Verification.UnitsFromAnchorsRescaleCert
   4
   5/-!
   6# Anchors-Rescaling Equivalence Certificate
   7
   8This audit certificate records that rescaling anchors by a positive factor `s`
   9does not change their **units-equivalence class** (the quotient by the speed
  10equivalence `AnchorsEqv`).
  11
  12Rather than reproving the ratio algebra directly, we derive the speed invariance
  13from the already-certified `UnitsFromAnchorsRescaleCert`: since `UnitsRescaled`
  14fixes `c`, and `unitsFromAnchors` sets `c := speedFromAnchors`, the induced speeds
  15must be equal.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Verification
  20namespace AnchorsRescaleEqv
  21
  22open IndisputableMonolith.RecogSpec
  23open IndisputableMonolith.Verification.UnitsFromAnchorsRescale
  24
  25structure AnchorsRescaleEqvCert where
  26  deriving Repr
  27
  28@[simp] def AnchorsRescaleEqvCert.verified (_c : AnchorsRescaleEqvCert) : Prop :=
  29  ∀ (A : RecogSpec.Anchors) (s : ℝ), 0 < s →
  30    Quot.mk RecogSpec.anchorsSetoid A = Quot.mk RecogSpec.anchorsSetoid (rescaleAnchors s A)
  31
  32@[simp] theorem AnchorsRescaleEqvCert.verified_any (c : AnchorsRescaleEqvCert) :
  33    AnchorsRescaleEqvCert.verified c := by
  34  intro A s hs
  35  have hNonempty :=
  36    IndisputableMonolith.Verification.UnitsFromAnchorsRescale.UnitsFromAnchorsRescaleCert.verified_any {} A s hs
  37  rcases hNonempty with ⟨hUU'⟩
  38  have hC :
  39      (RecogSpec.unitsFromAnchors (rescaleAnchors s A)).c = (RecogSpec.unitsFromAnchors A).c :=
  40    hUU'.cfix
  41  have hspeed : RecogSpec.speedFromAnchors A = RecogSpec.speedFromAnchors (rescaleAnchors s A) := by
  42    have : RecogSpec.speedFromAnchors (rescaleAnchors s A) = RecogSpec.speedFromAnchors A := by
  43      simpa [RecogSpec.unitsFromAnchors] using hC
  44    exact this.symm
  45  apply Quot.sound
  46  simpa [RecogSpec.AnchorsEqv] using hspeed
  47
  48end AnchorsRescaleEqv
  49end Verification
  50end IndisputableMonolith
  51