pith. sign in
module module high

IndisputableMonolith.Meta.Homogenization

show as:
view Lean formalization →

This module supplies a local non-sealed metric interface for homogenization scaffolding atop the simplicial ledger. It bridges the coordinate-free sheaf representation of the ledger to the foundation summary certificate. The module consists of sibling definitions for metric tensors, determinants, densities and homogenization limits with no sealed proofs.

claimThe module introduces a metric tensor $g$ on a simplicial 3-complex together with its determinant and a homogenization limit $H$ in the coordinate-free sheaf setting.

background

The upstream SimplicialLedger module formalizes the ledger as a simplicial 3-complex rather than a coordinate-fixed cubic lattice. It supplies a coordinate-free sheaf representation that unifies local and global J-cost variations. The present meta module adds a non-sealed metric interface used by homogenization scaffolding.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the SimplicialFoundationSummary certificate that the ledger structure is moving toward a coordinate-free simplicial sheaf representation. It supplies the metric scaffolding layer required for homogenization steps in the Recognition framework.

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)