IndisputableMonolith.Verification.MeasurementBridgeCert

   1import Mathlib
   2import IndisputableMonolith.Measurement.C2ABridge
   3
   4/-!
   5# Measurement Bridge Certificate (C = 2A and weight bridges)
   6
   7This certificate packages the key **two-branch** measurement bridge theorems proved in
   8`IndisputableMonolith/Measurement/C2ABridge.lean`:
   9
  10- `C = 2A` for the canonical path extracted from a two-branch rotation, and
  11- the corresponding weight identities (pathWeight = exp(-2A), hence Born weight).
  12
  13It intentionally does **not** import any Quantum scaffolds or any “measurement axioms” typeclass.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Verification
  18namespace MeasurementBridge
  19
  20open IndisputableMonolith.Measurement
  21
  22structure MeasurementBridgeCert where
  23  deriving Repr
  24
  25@[simp] def MeasurementBridgeCert.verified (_c : MeasurementBridgeCert) : Prop :=
  26  (∀ rot : TwoBranchRotation,
  27      Measurement.pathAction (Measurement.pathFromRotation rot) = 2 * Measurement.rateAction rot)
  28  ∧
  29  (∀ rot : TwoBranchRotation,
  30      Measurement.pathWeight (Measurement.pathFromRotation rot) = Real.exp (- 2 * Measurement.rateAction rot))
  31
  32@[simp] theorem MeasurementBridgeCert.verified_any (c : MeasurementBridgeCert) :
  33    MeasurementBridgeCert.verified c := by
  34  refine And.intro ?hC ?hW
  35  · intro rot
  36    exact Measurement.measurement_bridge_C_eq_2A rot
  37  · intro rot
  38    exact Measurement.weight_bridge rot
  39
  40end MeasurementBridge
  41end Verification
  42end IndisputableMonolith
  43