pith. sign in
module module high

IndisputableMonolith.Meta.Homogenization

show as:
view Lean formalization →

The module supplies a local non-sealed metric interface for homogenization scaffolding above the simplicial ledger. Researchers extending coordinate-free sheaf models of the ledger cite it when preparing homogenization limits. The module contains only interface definitions and metric objects with no sealed theorems or proofs.

claimA local metric interface $M$ on the simplicial 3-complex, non-sealed, supporting homogenization limits that unify local and global $J$-cost variations.

background

The module operates in the meta layer over the simplicial ledger. Upstream, that ledger formalizes the structure as a simplicial 3-complex rather than a coordinate-fixed cubic lattice and supplies a coordinate-free sheaf representation that unifies local and global J-cost variations.

The supplied doc-comment states the module purpose directly: Local non-sealed metric interface used by homogenization scaffolding. Sibling objects include MetricTensor, metric_det, SimplicialDensity, H_HomogenizationLimit and homogenization_limit.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the metric interface required by the downstream SimplicialFoundationSummary. That summary certifies that the ledger structure is moving toward a coordinate-free simplicial sheaf representation. It therefore fills the metric slot in the progression from simplicial ledger to homogenized foundation.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)