pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge

show as:
view Lean formalization →

The SimplicialDeficitDischarge module constructs an explicit calibration of deficit functionals against ledger graphs for general simplicial complexes. It extends the unconditional cubic-lattice discharge already obtained in CubicDeficitDischarge and invokes the linear_regge_vanishes result from Phase C4 to equate the Regge sum with κ times the Laplacian action on the conformal ε-field. Researchers deriving discrete Regge equations from J-cost stationarity cite it when moving from lattices to arbitrary triangulations. The module achieves its目的,

claimA deficit functional $D$ is calibrated against a ledger graph if its Regge sum equals $κ · Δε$ on the conformal ε-field. For the cubic lattice the equality holds by direct construction; for a general simplicial complex it follows from the vanishing of the linearized Regge deficit supplied by the Piran-Williams linearization.

background

The module belongs to the SimplicialLedger hierarchy whose goal is to identify the J-cost functional on a discrete recognition ledger with the Regge action. Upstream, ContinuumBridge proves that J-cost stationarity reproduces the Regge equations (up to the normalization κ = 8φ⁵). EdgeLengthFromPsi supplies the map from the recognition potential ψ on 3-simplices to the ten edge lengths of each 4-simplex. CubicDeficitDischarge discharges the ReggeDeficitLinearizationHypothesis unconditionally on the RS-canonical cubic lattice (Phase A).

proof idea

The module is an assembly point rather than a single theorem. It imports the cubic calibration, the Cayley-Menger volume formula, the Schläfli and dihedral-angle identities, and the Piran-Williams linearization from DeficitLinearization. These are combined to produce the simplicial_linearization_discharge statement that extends the cubic result to arbitrary complexes via the linear_regge_vanishes lemma.

why it matters in Recognition Science

It supplies the missing general-simplicial calibration required by the four-phase program that promotes the draft paper's Theorem 5.1 (field-curvature identity) to a Lean theorem. The result feeds the sibling declarations field_curvature_identity_simplicial and SimplicialFieldCurvatureCert, thereby closing the discrete-to-continuum bridge asserted in ContinuumBridge. It touches the remaining open step of lifting the calibration from static to dynamical complexes.

scope and limits

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (8)