homogenization_limit
plain-language theorem explainer
homogenization_limit states that simplicial recognition density converges to the square root of the absolute metric determinant as maximum simplex volume tends to zero. Researchers deriving continuum limits in discrete gravity or emergent spacetime models would cite it to justify replacing ledger counts with volume forms. The proof is a direct one-line wrapper applying the input hypothesis without further reduction.
Claim. Let $L$ be a simplicial ledger and $g$ a metric tensor. If the homogenization hypothesis holds, then for every $ε > 0$ there exists $ℓ_{0,max} > 0$ such that whenever every simplex has volume less than $ℓ_{0,max}$, for all points $x$ the absolute difference between the recognition density at $x$ and the square root of the absolute value of the metric determinant (with the first coordinate set to zero) is less than $ε$.
background
The module proves the continuum limit for simplicial ledger transitions. A simplicial ledger is a nonempty collection of 3-simplices forming a manifold covering. Simplicial density counts simplices containing a point divided by their average volume. The metric tensor supplies a determinant function at each point. The hypothesis H_HomogenizationLimit encodes the convergence claim as an empirical proposition whose test protocol is mathematical verification via discrete exterior calculus on simplicial complexes.
proof idea
The declaration is a term-mode proof. It consists of a single direct application of the supplied hypothesis h, equating the quantified limit statement to the definition of H_HomogenizationLimit without invoking additional lemmas or tactics.
why it matters
This result formalizes the homogenization step that recovers the macroscopic metric from underlying simplicial density in the zero-scale limit. It fills the continuum-limit objective stated in the module documentation. With zero downstream dependencies recorded, the declaration functions as a foundational interface for later derivations of effective geometry from recognition events. It connects to the framework goal of obtaining the metric as the unique effective description once the simplicial scale vanishes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.