EntanglementStructure

formal source

  23namespace IndisputableMonolith.Physics.EntanglementEntropyFromRS
  24open Cost
  25
  26inductive EntanglementStructure where
  27  | product | separable | entangled | maximallyEntangled | clusterState
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem entanglementStructureCount : Fintype.card EntanglementStructure = 5 := by decide
  31
  32/-- Unentangled state: J = 0. -/
  33theorem unentangled_zero_cost : Jcost 1 = 0 := Jcost_unit0
  34
  35/-- Entangled state: J > 0 (off-equilibrium). -/
  36theorem entangled_positive_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  37    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  38
  39/-- Maximal entanglement: log(2^D) = D × log(2). -/
  40noncomputable def maximalEntanglementLog : ℝ := 3 * Real.log 2
  41
  42theorem maximalEntanglement_pos : 0 < maximalEntanglementLog :=
  43  mul_pos (by norm_num) (Real.log_pos (by norm_num))
  44
  45structure EntanglementEntropyCert where
  46  five_structures : Fintype.card EntanglementStructure = 5
  47  unentangled : Jcost 1 = 0
  48  entangled_cost : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  49  max_entanglement_pos : 0 < maximalEntanglementLog
  50
  51noncomputable def entanglementEntropyCert : EntanglementEntropyCert where
  52  five_structures := entanglementStructureCount
  53  unentangled := unentangled_zero_cost
  54  entangled_cost := entangled_positive_cost
  55  max_entanglement_pos := maximalEntanglement_pos
  56