pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Meta.Homogenization

show as:
view Lean formalization →

The Meta.Homogenization module supplies a local non-sealed metric interface for homogenization scaffolding on the simplicial ledger. Researchers extending coordinate-free sheaf models of the ledger topology would cite it when adding metric limits to J-cost unification. The module contains only definitions for tensors, densities, and limit objects with no theorems or proofs.

claimThe module defines the metric tensor $g$ on the simplicial 3-complex together with its determinant, the simplicial density function, and the homogenization limit operator $H$ used for local metric scaffolding.

background

The module sits inside the Recognition Science meta layer and imports the simplicial ledger topology. That upstream module formalizes the ledger 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.

proof idea

This is a definition module, no proofs. It declares the metric interface objects (MetricTensor, metric_det, SimplicialDensity, H_HomogenizationLimit, homogenization_limit) that downstream modules apply directly.

why it matters in Recognition Science

The module feeds the SimplicialFoundationSummary certificate, which records progress toward a coordinate-free simplicial sheaf representation of the ledger. It supplies the local metric scaffolding required for homogenization steps in the meta layer while remaining unsealed.

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)