`homogenization_limit`

proved

show as: view math explainer →

module: IndisputableMonolith.Meta.Homogenization
domain: Meta
line: 46 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Meta.Homogenization on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  43/-- **THEOREM: Metric from Density (Homogenization)**
  44    As the simplicial scale $\ell_0 \to 0$, the simplicial recognition density
  45    converges to the volume form of the macroscopic metric $g_{\mu\nu}$. -/
  46theorem homogenization_limit (h : H_HomogenizationLimit L g) (L : SimplicialLedger) (g : MetricTensor) :
  47    ∀ ε > 0, ∃ ell0_max > 0,
  48      (∀ simplex ∈ L.simplices, simplex.volume < ell0_max) →
  49      ∀ x, abs (SimplicialDensity L x - Real.sqrt (abs (metric_det g (fun i => if i.val = 0 then 0 else x i)))) < ε := h
  50
  51end Meta
  52end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.