pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge

show as:
view Lean formalization →

The module defines calibration of a deficit functional against a ledger graph, requiring its Regge sum to match κ times the Laplacian action on the conformal ε-field. It supplies the explicit cubic-lattice construction as Phase A. General simplicial complexes use the linear_regge_vanishes result from Phase C4. Researchers deriving the Einstein equations from J-cost stationarity cite it to link discrete RS ledgers to continuum gravity. The module assembles geometry and ledger imports without independent proofs.

claimA deficit functional $F$ is calibrated against a ledger graph when its Regge sum satisfies $\sum \mathrm{Regge}(\sigma) = \kappa \cdot \Delta(\varepsilon)$ on the conformal field $\varepsilon$, where $\kappa=8\phi^5$.

background

This module belongs to the Foundation.SimplicialLedger hierarchy. It imports ContinuumBridge, whose doc states that the J-cost functional on the simplicial ledger is the Regge action (normalized by $\kappa=8\phi^5$) and that J-cost stationarity yields the Regge equations. It further imports CubicDeficitDischarge, which discharges ReggeDeficitLinearizationHypothesis unconditionally for the RS-canonical cubic lattice as Phase A of the four-phase program. EdgeLengthFromPsi supplies the identification of the recognition potential $\psi$ with the ten edge lengths per 4-simplex. Geometry modules provide Cayley-Menger determinants, Piran-Williams linearization, dihedral angles, and Schläfli relations.

The local theoretical setting is the program to promote the draft paper's Theorem 5.1 (field-curvature identity) from pattern-matching to a Lean theorem, with Phase A handling the cubic case and Phase C4 supplying the general simplicial calibration via linear_regge_vanishes.

proof idea

This is a definition module, no proofs. It declares the calibration predicate and related simplicial objects by importing and organizing results from the cubic lattice case (CubicDeficitDischarge), the continuum bridge, and the geometry primitives (Cayley-Menger, DeficitLinearization, DihedralAngle, Schlaefli).

why it matters in Recognition Science

This module supplies the simplicial calibration required for the field-curvature identity. It feeds the ContinuumBridge result that J-cost stationarity implies the Einstein field equations. The parent program is the discharge of ReggeDeficitLinearizationHypothesis across Phase A (cubic) and Phase C4 (general simplicial via linear_regge_vanishes). It touches the open question of extending the cubic calibration to arbitrary complexes while preserving the match to $\kappa \cdot$ laplacian_action.

scope and limits

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (8)