IndisputableMonolith.Quantum.BornRuleStructure

   1import Mathlib
   2import IndisputableMonolith.Quantum.BornRule
   3
   4namespace IndisputableMonolith
   5namespace Quantum
   6namespace BornRuleStructure
   7
   8open BornRule
   9
  10/-- Structural Born-rule content: probability weights are nonnegative. -/
  11def born_rule_from_ledger : Prop := ∀ ψ : ℂ, 0 ≤ Complex.normSq ψ
  12
  13theorem born_rule_structure : born_rule_from_ledger := by
  14  intro ψ
  15  exact born_rule_consistent ψ
  16
  17/-- Phase cancellation in probabilities: global phase does not alter `|ψ|²`. -/
  18theorem born_rule_phase_cancels (r θ : ℝ) :
  19    Complex.normSq ((r : ℂ) * Complex.exp (θ * Complex.I)) = r ^ 2 :=
  20  born_rule_phase_independent r θ
  21
  22/-- Born-rule structure gives nonnegativity at any specific amplitude. -/
  23theorem born_rule_nonnegative_at (h : born_rule_from_ledger) (ψ : ℂ) :
  24    0 ≤ Complex.normSq ψ :=
  25  h ψ
  26
  27/-- Born-rule structure implies nonnegative probability weight at each amplitude. -/
  28theorem born_rule_implies_nonnegative (h : born_rule_from_ledger) (ψ : ℂ) :
  29    0 ≤ Complex.normSq ψ :=
  30  born_rule_nonnegative_at h ψ
  31
  32end BornRuleStructure
  33end Quantum
  34end IndisputableMonolith
  35