IndisputableMonolith.Verification.BornRuleDerivationCert

   1import Mathlib
   2import IndisputableMonolith.Measurement.BornRule
   3
   4/-!
   5# Born Rule Derivation Certificate (two-outcome, axiom-free)
   6
   7This certificate packages the derived two-outcome Born rule statement from
   8`IndisputableMonolith/Measurement/BornRule.lean` **without** any hidden typeclass axioms.
   9
  10It states: given a two-branch rotation and amplitudes whose squared norms match the
  11geometric `cos²/sin²` amplitudes, the normalized recognition-cost probabilities match
  12those squared norms.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Verification
  17namespace BornRuleDerivation
  18
  19open IndisputableMonolith.Measurement
  20
  21structure BornRuleDerivationCert where
  22  deriving Repr
  23
  24@[simp] def BornRuleDerivationCert.verified (_c : BornRuleDerivationCert) : Prop :=
  25  ∀ (α₁ α₂ : ℂ) (rot : TwoBranchRotation),
  26    (‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 = 1) →
  27    (‖α₁‖ ^ 2 = complementAmplitudeSquared rot) →
  28    (‖α₂‖ ^ 2 = initialAmplitudeSquared rot) →
  29      ∃ m : TwoOutcomeMeasurement,
  30        prob₁ m = ‖α₁‖ ^ 2 ∧
  31        prob₂ m = ‖α₂‖ ^ 2
  32
  33@[simp] theorem BornRuleDerivationCert.verified_any (c : BornRuleDerivationCert) :
  34    BornRuleDerivationCert.verified c := by
  35  intro α₁ α₂ rot hα hrot₁ hrot₂
  36  exact born_rule_from_C (α₁:=α₁) (α₂:=α₂) hα rot hrot₁ hrot₂
  37
  38end BornRuleDerivation
  39end Verification
  40end IndisputableMonolith
  41