SimplicialDensity
plain-language theorem explainer
SimplicialDensity defines the local count of recognition events per unit volume for simplicial ledger L at point x in R^3. Researchers establishing continuum limits from discrete coverings cite this when linking microscopic simplices to macroscopic geometry. The definition counts containing simplices via membership and normalizes by the mean volume from summation and cardinality over the ledger set.
Claim. For simplicial ledger $L$ and point $x : Fin 3 → ℝ$, the recognition density is the cardinality of simplices containing $x$ divided by the average volume of all simplices in $L$.
background
The module proves existence of the continuum limit for simplicial ledger transitions, with the objective that the macroscopic metric $g_{μν}$ is the unique effective description of the underlying simplicial recognition density. SimplicialLedger is a collection of 3-simplices forming a manifold covering, with the non-emptiness property required. Upstream structures supply nuclear densities in φ-tiers, J-cost convexity from ledger factorization, and spectral emergence of gauge content and generations.
proof idea
Direct definition that builds the containing set by vertex membership test at x, then computes the ratio of its cardinality to the mean volume obtained by summing volumes and dividing by total cardinality.
why it matters
This supplies the local density function used by H_HomogenizationLimit and the homogenization_limit theorem in the same module. Those establish convergence of the density to the square root of the metric determinant as scale ℓ0 approaches zero. It fills the step in the Homogenization Theorem toward the unique macroscopic metric from the simplicial covering, anchoring D=3 emergence in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.