pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge

show as:
view Lean formalization →

This module defines calibration of a deficit functional against a ledger graph, requiring the Regge sum to equal κ times the Laplacian action on the conformal ε-field. It supplies the explicit cubic-lattice construction as Phase A of the four-phase program. Researchers deriving discrete Regge equations from J-cost stationarity cite it to bridge the simplicial ledger to the Einstein field equations. The module assembles the argument via imports of the continuum bridge, cubic discharge, and geometry linearization results.

claimA deficit functional $D$ is calibrated against ledger graph $G$ when its Regge sum equals $8φ^5$ times the Laplacian action of the conformal ε-field on $G$. Phase A realizes this equality explicitly on the RS-canonical cubic lattice; the general simplicial case follows from linear_regge_vanishes in Phase C4.

background

The module sits inside the Foundation.SimplicialLedger hierarchy that discharges the ReggeDeficitLinearizationHypothesis stated in EdgeLengthFromPsi. Upstream, ContinuumBridge identifies the J-cost functional on the simplicial ledger with the Regge action (normalized by κ = 8φ⁵) and shows that J-cost stationarity yields the Regge equations. CubicDeficitDischarge supplies the unconditional cubic-lattice case of that identification, while DeficitLinearization packages the Piran-Williams linearization of the Regge deficit angle around a flat complex. CayleyMenger and Schlaefli supply the volume and angle formulas needed to express the deficit in terms of edge lengths derived from the recognition potential ψ.

proof idea

This is a definition module, no proofs. It imports the cubic calibration, the continuum-bridge identification of J-cost with the Regge action, and the geometry modules for Cayley-Menger volumes and deficit linearization, then declares the calibrated predicate together with the simplicial linearization discharge statement.

why it matters in Recognition Science

The module supplies the simplicial calibration predicate required by field_curvature_identity_simplicial and SimplicialFieldCurvatureCert (siblings). It advances Phase A of the program that turns the draft paper's Theorem 5.1 (field-curvature identity) into a Lean theorem by discharging ReggeDeficitLinearizationHypothesis for the cubic lattice; the general case is deferred to Phase C4's linear_regge_vanishes. It therefore closes one concrete link between the discrete RS ledger and the Einstein field equations.

scope and limits

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (8)