IndisputableMonolith.Quantum.CommutationStructure

   1import Mathlib
   2import IndisputableMonolith.Quantum.Observables
   3
   4namespace IndisputableMonolith
   5namespace Quantum
   6namespace CommutationStructure
   7
   8/-- Structural commutation content: projector algebra is idempotent. -/
   9def commutation_from_ledger : Prop :=
  10  ∀ (H : Type*) [RSHilbertSpace H], ∀ P : Projector H, P.op.comp P.op = P.op
  11
  12theorem commutation_structure : commutation_from_ledger := by
  13  intro H hH P
  14  exact P.idempotent
  15
  16/-- Universe-stable extractor for commutation structure. -/
  17theorem commutation_implies_projector_idempotent.{u}
  18    (h : @commutation_from_ledger.{u}) : @commutation_from_ledger.{u} :=
  19  h
  20
  21end CommutationStructure
  22end Quantum
  23end IndisputableMonolith
  24