IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
This module supplies the cubic-lattice discharge of the Regge deficit linearization, recovering the conformal factor ε_i from self-loop edge lengths L_ii = a exp(ε_i). It supplies the Phase A step required by the field-curvature identity. Researchers closing the discrete-to-continuum bridge in Recognition Science cite the cubicDeficit and recoverEps constructions. Content consists of direct definitions plus singleton lemmas establishing non-negativity and functional identities.
claimThe module defines recoverEps and cubicDeficit such that $L_{ii}=a\exp(\varepsilon_i)$ recovers the conformal factor on the hypercubic lattice, together with the associated cubicArea and cubicDeficitFunctional.
background
Upstream, Constants fixes the RS time quantum τ₀=1 tick. ContinuumBridge establishes that the J-cost functional on the simplicial ledger equals the Regge action (normalized by κ=8φ⁵) and that stationarity δJ=0 yields the Regge equations. EdgeLengthFromPsi supplies the map from the recognition potential ψ on 3-simplices to the full set of edge lengths needed for the Regge action. The present module specializes these constructions to the cubic (hypercubic) lattice, introducing recoverEps, cubicDeficit, cubicArea and the singletonHinge family.
proof idea
This is a definition module. recoverEps and recoverEps_conformal are direct inverses of the exponential map. cubicDeficit and cubicArea are defined by summation over the six edges of each tetrahedron; singleton lemmas (cubicDeficit_singleton, cubicArea_singleton, cubicArea_nonneg) are one-line wrappers that substitute the singletonHinge definitions and apply non-negativity of the exponential.
why it matters in Recognition Science
The module supplies the cubic_linearization_discharge step required by ContinuumTheorem (Phase D of Theorem 5.1). It is imported by CubicSimplicialEquivalence to address the hypercubic-to-simplicial passage and by SimplicialDeficitDischarge (Phase C5) as the cubic special case. It therefore closes the lattice-specific part of the J-cost = Regge action identification.
scope and limits
- Does not treat general simplicial complexes.
- Does not derive the Einstein field equations.
- Does not address non-conformal edge-length fields.
- Does not discharge the full ReggeDeficitLinearizationHypothesis.
used by (3)
depends on (3)
declarations in this module (19)
-
def
recoverEps -
theorem
recoverEps_conformal -
def
singletonHinge -
theorem
singletonHinge_weight -
theorem
singletonHinge_edges -
def
cubicDeficit -
def
cubicArea -
theorem
cubicDeficit_singleton -
theorem
cubicArea_singleton -
theorem
cubicArea_nonneg -
def
cubicDeficitFunctional -
theorem
singletonHinge_product -
def
cubicHinges -
theorem
regge_sum_cubicHinges -
theorem
laplacian_action_as_prod_sum -
theorem
cubic_linearization_discharge -
theorem
field_curvature_identity_cubic -
structure
CubicFieldCurvatureCert -
theorem
cubicFieldCurvatureCert