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

SimplicialDensity

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)

  27noncomputable def SimplicialDensity (L : SimplicialLedger) (x : Fin 3 → ℝ) : ℝ :=

proof body

Definition body.

  28  let containing := { s ∈ L.simplices | ∃ y : Fin 3 → ℝ, s.vertices 0 = y } -- Simplified membership
  29  (containing.toFinset.card : ℝ) / (L.simplices.toFinset.sum (fun s => s.volume) / L.simplices.toFinset.card)
  30
  31/-- **HYPOTHESIS**: The simplicial recognition density converges to the
  32    macroscopic volume form.
  33    STATUS: EMPIRICAL_HYPO
  34    TEST_PROTOCOL: Mathematical verification of the continuum limit using DEC
  35    on simplicial complexes.
  36    FALSIFIER: Discovery of a simplicial ledger covering that does not satisfy
  37    the homogenization limit. -/

used by (2)

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

depends on (11)

Lean names referenced from this declaration's body.