theorem
proved
tactic proof
pauli_exclusion
show as:
view Lean formalization →
formal statement (Lean)
215theorem pauli_exclusion :
216 ∀ (state : Type*) (ψ : state → state → ℂ),
217 (∀ a b, ψ a b = -(ψ b a)) → (∀ a, ψ a a = 0) := by
proof body
Tactic-mode proof.
218 intro state ψ antisym a
219 have heq : ψ a a = -(ψ a a) := antisym a a
220 -- x = -x in ℂ implies x = 0 (since char ℂ = 0)
221 -- Algebraic proof: x = -x → x - x = -x - x → 0 = -2x → x = 0
222 have h2 : (2 : ℂ) ≠ 0 := two_ne_zero
223 -- ψ + ψ = ψ + (-ψ) = 0
224 have hsum : ψ a a + ψ a a = 0 := by
225 nth_rewrite 2 [heq]
226 exact add_neg_cancel (ψ a a)
227 have h2x : (2 : ℂ) * ψ a a = 0 := by rw [two_mul]; exact hsum
228 exact (mul_eq_zero.mp h2x).resolve_left h2
229
230/-! ## Connection to 8-Tick Ledger -/
231
232/-- A ledger entry type for tracking phase. -/