`LedgerState`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.GaugeInvariance
domain: QFT
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.GaugeInvariance on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  35/-! ## The Ledger and Redundancy -/
  36
  37/-- A ledger state encodes physical reality. -/
  38structure LedgerState where
  39  entries : List ℂ
  40  phase : ℝ  -- Global phase
  41
  42/-- Two ledger states are physically equivalent if they differ only by a global phase.
  43
  44    This is the origin of U(1) gauge symmetry! -/
  45def physicallyEquivalent (s1 s2 : LedgerState) : Prop :=
  46  ∃ θ : ℝ, s2.entries = s1.entries.map (fun z => z * exp (I * θ))
  47
  48/-- **THEOREM**: Physical equivalence is an equivalence relation. -/
  49theorem physical_equiv_refl (s : LedgerState) : physicallyEquivalent s s := by
  50  use 0
  51  simp [Complex.exp_zero]
  52
  53/-- Phase inversion gives symmetry: if s2 = s1 rotated by θ, then s1 = s2 rotated by -θ.
  54    Proof: exp(iθ) * exp(-iθ) = 1, so z * exp(iθ) * exp(-iθ) = z for all z.
  55    The composed List.map is the identity.
  56    PROOF STATUS: Core exponential identity proven; List.map composition tedious. -/
  57theorem physical_equiv_symm {s1 s2 : LedgerState}
  58    (h : physicallyEquivalent s1 s2) : physicallyEquivalent s2 s1 := by
  59  obtain ⟨θ, hθ⟩ := h
  60  use -θ
  61  -- Key mathematical fact: exp(iθ) * exp(i(-θ)) = 1
  62  have hexp : exp (I * θ) * exp (I * ↑(-θ)) = 1 := by
  63    rw [← Complex.exp_add]
  64    simp only [ofReal_neg, mul_neg, add_neg_cancel, Complex.exp_zero]
  65  -- Therefore z * exp(iθ) * exp(i(-θ)) = z for all z
  66  have hcancel : ∀ z : ℂ, z * exp (I * θ) * exp (I * ↑(-θ)) = z := fun z => by
  67    calc z * exp (I * θ) * exp (I * ↑(-θ))
  68        = z * (exp (I * θ) * exp (I * ↑(-θ))) := by ring

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.