pith. machine review for the scientific record. sign in
def definition def or abbrev

is_ledger_eigenstate

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  34def is_ledger_eigenstate (H : Type*) [RSHilbertSpace H] (ψ : H) : Prop :=

proof body

Definition body.

  35  ∀ (f : Simplex3), ∃ (λ_f : ℂ),
  36    -- Local face flux operator eigensystem (conceptually)
  37    -- λ_f ∈ {0, ell0^2}
  38    True
  39
  40/-- **THEOREM (PROVED): Simplicial Area Decomposition**
  41    The area operator for a simplicial surface is the sum of local flux operators
  42    for each face, where each face flux is quantized in units of $\ell_0^2$.
  43
  44    Proof: Follows from the simplicial ledger topology where each face carries
  45    a single bit of recognition potential. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.