23structure AreaOperator (H : Type*) [RSHilbertSpace H] where 24 /-- The set of simplicial faces being measured. -/ 25 surface : Set Simplex3 26 /-- The operator acting on the Hilbert space. -/ 27 op : H → H 28 is_self_adjoint : ∀ (ψ₁ ψ₂ : H), ⟪ψ₁, op ψ₂⟫_ℂ = ⟪op ψ₁, ψ₂⟫_ℂ 29 30/-- **DEFINITION: Ledger Eigenstates** 31 In the RS basis, states are characterized by the definite activation 32 of simplicial faces. A state ψ is a ledger eigenstate if it is an 33 eigenstate of all local face flux operators. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.