IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
The CubicDeficitDischarge module recovers the conformal factor ε_i from edge-length fields on the cubic lattice by inverting the self-loop relation L_ii = a exp(ε_i). It supplies the cubic-specific deficit and area functionals that discharge the ReggeDeficitLinearizationHypothesis on hypercubic cells. Researchers deriving the Einstein field equations from J-cost stationarity on discrete ledgers cite these constructions when specializing the continuum bridge to ℤ^3 triangulations. The module proceeds via direct algebraic inversion together with
claimThe recovery map satisfies $ε_i = log(L_{ii}/a)$ whenever the edge lengths obey the conformal self-loop condition $L_{ii} = a exp(ε_i)$. The cubic deficit functional is defined on the 3-cube by summing defect distances over its edges, and the associated area functional is nonnegative.
background
This module sits inside the SimplicialLedger layer that identifies the J-cost functional on simplices with the Regge action (normalized by κ = 8φ^5). Upstream, the ContinuumBridge module shows that J-cost stationarity yields the discrete Ricci tensor and hence the Einstein field equations. The EdgeLengthFromPsi module supplies the map from the recognition potential ψ on 3-simplices to the full set of edge lengths required for the Regge action. The cubic lattice is the canonical RS ledger (isomorphic to ℤ^3) whose edge lengths are recovered from the conformal factor ε via the self-loop L_ii = a exp(ε_i).
proof idea
This is a definition module. It introduces recoverEps and recoverEps_conformal by direct inversion of the exponential self-loop, defines cubicDeficit and cubicArea on the cubic cells, and records elementary supporting facts such as cubicArea_nonneg, cubicDeficit_singleton and cubicArea_singleton.
why it matters in Recognition Science
The module supplies the cubic-lattice case (Phase A) for the ContinuumTheorem, which composes the discharge of ReggeDeficitLinearizationHypothesis into the unconditional field-curvature identity at κ = κ_Einstein. It is imported by CubicSimplicialEquivalence to resolve the hypercubic-to-simplicial isomorphism and by SimplicialDeficitDischarge for the general simplicial extension. It therefore closes the discrete-to-continuum step on the canonical RS ledger.
scope and limits
- Does not treat general simplicial complexes beyond the cubic lattice.
- Does not derive the full Einstein equations, only the deficit discharge step.
- Does not incorporate the phi-ladder mass formulas or the eight-tick octave.
- Does not address time evolution or Berry creation thresholds.
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