pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger

show as:
view Lean formalization →

SimplicialLedger supplies the 3-simplex voxel as the discrete atom of volume in the Recognition ledger. It is imported by modules that force D=3, construct the continuum bridge to Regge calculus, and prove homogenization. The module consists of type and function definitions that downstream arguments treat as the geometric substrate.

claimA 3-simplex (tetrahedron) $V$ is the atom of volume in the ledger; the simplicial ledger is the structure whose cells are such voxels equipped with J-cost and recognition patterns.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants, the J-cost functional from Cost, and pattern definitions from Patterns. It introduces Simplex3 as the basic 3-dimensional simplex and SimplicialLedger as the collection of such simplices carrying local and global J-costs. The setting is the discrete foundation layer that precedes dimension forcing and the passage to a continuum metric.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the geometric primitives required by DimensionForcing (D = 3), SimplicialFoundationSummary (certificate of simplicial structure), ContinuumBridge (J-cost stationarity equals Regge equations), EdgeLengthFromPsi, InteriorFlat, and Homogenization (continuum limit of the ledger). It occupies the position of the voxel definition in the T8 forcing chain and the discrete-to-continuum transition.

scope and limits

used by (7)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)