physicallyEquivalent

formal source

  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
  69      _ = z * 1 := by rw [hexp]
  70      _ = z := by ring
  71  -- The composed map is the identity, so s2.map(·*exp(-iθ)) = s1.map(id) = s1
  72  rw [hθ, List.map_map]
  73  -- List extensionality: show each element is unchanged
  74  apply List.ext_getElem
  75  · simp only [List.length_map]