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

SimplicialLedger

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)

  31structure SimplicialLedger where
  32  simplices : Set Simplex3
  33  /-- The simplices form a non-empty set (non-vacuity). -/
  34  non_empty : simplices.Nonempty
  35  /-- SCAFFOLD: Manifold covering property.
  36    Proof requires simplicial complex axioms and manifold topology.
  37    See: LaTeX Manuscript, Chapter "Gravity as Recognition", Section "Simplicial Ledger". -/
  38  is_covering : Prop
  39
  40/-- **DEFINITION: Simplicial Sheaf**
  41    A sheaf assigning a recognition potential to each simplex in the ledger. -/

used by (29)

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

depends on (8)

Lean names referenced from this declaration's body.