IndisputableMonolith.Verification.BandsInvariantCert

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Bands
   3
   4/-!
   5# Bands-Invariance Certificate (c-band checker is dimensionless)
   6
   7This audit certificate packages the fact that the absolute-layer band check
   8
   9`evalToBands_c U X : Prop := ∃ b ∈ X, Band.contains b U.c`
  10
  11is invariant under anchor rescalings (`Verification.UnitsRescaled`), because such
  12rescalings keep the speed parameter `c` fixed (`cfix`).
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Verification
  17namespace BandsInvariant
  18
  19open IndisputableMonolith.RecogSpec
  20
  21structure BandsInvariantCert where
  22  deriving Repr
  23
  24@[simp] def BandsInvariantCert.verified (_c : BandsInvariantCert) : Prop :=
  25  ∀ {U U' : IndisputableMonolith.Constants.RSUnits}
  26    (_h : Verification.UnitsRescaled U U') (X : RecogSpec.Bands),
  27      RecogSpec.evalToBands_c U X ↔ RecogSpec.evalToBands_c U' X
  28
  29@[simp] theorem BandsInvariantCert.verified_any (c : BandsInvariantCert) :
  30    BandsInvariantCert.verified c := by
  31  intro U U' h X
  32  exact RecogSpec.evalToBands_c_invariant (U := U) (U' := U') h X
  33
  34end BandsInvariant
  35end Verification
  36end IndisputableMonolith
  37