IndisputableMonolith.Verification.KernelMatchCert

   1import IndisputableMonolith.Measurement.KernelMatch
   2
   3namespace IndisputableMonolith
   4namespace Verification
   5namespace KernelMatch
   6
   7/-- Certificate packaging the pointwise kernel identity `J(r(ϑ)) = 2 cot ϑ` from
   8`Measurement/KernelMatch.lean`. This is a foundational ingredient for the `C = 2A`
   9bridge proof. -/
  10structure KernelMatchCert where
  11  deriving Repr
  12
  13@[simp] def KernelMatchCert.verified (_c : KernelMatchCert) : Prop :=
  14  ∀ ϑ : ℝ,
  15    (0 ≤ ϑ ∧ ϑ ≤ Real.pi / 2) →
  16      IndisputableMonolith.Cost.Jcost (Measurement.recognitionProfile ϑ) = 2 * Real.cot ϑ
  17
  18@[simp] theorem KernelMatchCert.verified_any (c : KernelMatchCert) :
  19    KernelMatchCert.verified c := by
  20  intro ϑ hϑ
  21  exact Measurement.kernel_match_pointwise ϑ hϑ
  22
  23end KernelMatch
  24end Verification
  25end IndisputableMonolith
  26