Pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger

show as:
view Lean formalization →

SimplicialLedger defines the 3-simplex as the fundamental volume element of the recognition ledger. Modules on dimension forcing and the discrete-to-continuum bridge cite it when they require a coordinate-free geometric substrate. The module supplies the voxel definition together with ledger operations and supporting lemmas but contains no major theorem proofs.

claimThe simplicial voxel is the 3-simplex $\Delta^3$ that serves as the atom of volume in the ledger.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from Constants, the J-cost functional from Cost, and pattern structures from Patterns. It introduces the simplicial voxel as the elementary 3-dimensional cell together with associated ledger operations on 3-simplices. The local setting is the foundation layer that supplies discrete geometry for subsequent recognition-cost arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the simplicial primitives required by DimensionForcing to establish D = 3 and by ContinuumBridge to identify the J-cost functional with the Regge action (up to normalization by $\kappa = 8\phi^5$). It also supports the simplicial foundation certificate and the homogenization theorem that extracts the macroscopic metric from the ledger.

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)