IndisputableMonolith.Verification.UniqueCalibrationCert

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Spec
   3
   4/-!
   5# UniqueCalibration Certificate (absolute-layer calibration is explicit)
   6
   7This certificate packages the lemma `IndisputableMonolith.RecogSpec.uniqueCalibration_any`:
   8for every ledger/bridge and every anchor pair, there is a *unique* RS-units pack
   9calibrated to those anchors (with the speed determined by `speedFromAnchors`).
  10
  11This is an **audit** certificate: it makes the “absolute-layer calibration witness”
  12explicit and machine-checked, rather than relying on implicit choice.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Verification
  17namespace UniqueCalibration
  18
  19open IndisputableMonolith.RecogSpec
  20
  21structure UniqueCalibrationCert where
  22  deriving Repr
  23
  24@[simp] def UniqueCalibrationCert.verified (_c : UniqueCalibrationCert) : Prop :=
  25  ∀ (L : RecogSpec.Ledger) (B : RecogSpec.Bridge L) (A : RecogSpec.Anchors),
  26    RecogSpec.UniqueCalibration L B A
  27
  28@[simp] theorem UniqueCalibrationCert.verified_any (c : UniqueCalibrationCert) :
  29    UniqueCalibrationCert.verified c := by
  30  intro L B A
  31  exact RecogSpec.uniqueCalibration_any L B A
  32
  33end UniqueCalibration
  34end Verification
  35end IndisputableMonolith
  36