Pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge

show as:
view Lean formalization →

The SimplicialDeficitDischarge module defines calibration of a deficit functional against a ledger graph as equality between its Regge sum and κ times the Laplacian action on the conformal ε-field. Researchers closing the discrete-to-continuum gap in Recognition Science cite it when extending cubic-lattice results to general simplicial complexes. The module assembles imports from the cubic discharge, continuum bridge, and geometry libraries to prepare the calibration without supplying new theorems.

claimA deficit functional $F$ is calibrated against ledger graph $G$ when its Regge sum satisfies $\sum \delta_i = \kappa \cdot \Delta_\epsilon$, where $\delta_i$ are the Regge deficits, $\kappa=8\phi^5$, and $\Delta_\epsilon$ is the Laplacian action on the conformal $\epsilon$-field.

background

Recognition Science identifies the J-cost functional on the simplicial ledger with the Regge action (normalized by $\kappa=8\phi^5$), so that J-cost stationarity yields the Regge equations; this identification is supplied by the ContinuumBridge module. The present module belongs to the four-phase program that discharges the ReggeDeficitLinearizationHypothesis: Phase A is handled unconditionally for the cubic lattice by CubicDeficitDischarge, while the general simplicial case is prepared by geometry modules (CayleyMenger for simplex volumes, DeficitLinearization for the Piran-Williams linearization, and Schlaefli/DihedralAngle for angle data). EdgeLengthFromPsi supplies the prior identification of the recognition potential $\psi$ on 3-simplices with the ten edge lengths per 4-simplex needed to define the Regge action.

proof idea

This is a definition module, no proofs. It imports the cubic lattice discharge, the continuum bridge, and the geometry primitives (CayleyMenger, DeficitLinearization, etc.) and records the calibration definition together with the reference to Phase C4's linear_regge_vanishes for the general case.

why it matters in Recognition Science

The module supplies the calibration notion required by the parent field-curvature identity (draft paper Theorem 5.1) that equates J-cost stationarity on the ledger with the Einstein field equations. It is the organizing file for the simplicial half of the four-phase program described in CubicDeficitDischarge and EdgeLengthFromPsi; downstream siblings such as field_curvature_identity_simplicial and simplicial_linearization_discharge will invoke the calibration once linear_regge_vanishes is available.

scope and limits

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (8)