IndisputableMonolith.Quantum.EntanglementOntologyStructure

   1import Mathlib
   2import IndisputableMonolith.Quantum.BornRule
   3
   4namespace IndisputableMonolith
   5namespace Quantum
   6namespace EntanglementOntologyStructure
   7
   8open BornRule
   9
  10/-- Structural entanglement content represented by interference cross terms. -/
  11def entanglement_ontology_from_ledger : Prop :=
  12  ∀ ψ₁ ψ₂ : ℂ,
  13    Complex.normSq (ψ₁ + ψ₂) = Complex.normSq ψ₁ + Complex.normSq ψ₂ +
  14      2 * (ψ₁ * (starRingEnd ℂ) ψ₂).re
  15
  16theorem entanglement_ontology_structure : entanglement_ontology_from_ledger := by
  17  intro ψ₁ ψ₂
  18  exact interference_from_phase ψ₁ ψ₂
  19
  20/-- Entanglement-ontology structure implies the interference cross-term identity. -/
  21theorem entanglement_implies_interference (h : entanglement_ontology_from_ledger)
  22    (ψ₁ ψ₂ : ℂ) :
  23    Complex.normSq (ψ₁ + ψ₂) = Complex.normSq ψ₁ + Complex.normSq ψ₂ +
  24      2 * (ψ₁ * (starRingEnd ℂ) ψ₂).re :=
  25  h ψ₁ ψ₂
  26
  27end EntanglementOntologyStructure
  28end Quantum
  29end IndisputableMonolith
  30