IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
This module supplies the cubic-lattice discharge of the Regge deficit linearization hypothesis together with the recoverEps map that extracts the conformal factor from self-loop edge lengths. Workers on the discrete-to-continuum bridge in Recognition Science cite it when assembling the cubic phase of the field-curvature identity. The module consists of targeted definitions and short lemmas that compose directly into the cubic case of the larger discharge argument.
claimGiven a conformal edge-length field with self-loops $L_{ii}=a·e^{ε_i}$, recover $ε_i=log(L_{ii}/a)$. Define the cubic deficit and area functionals on the lattice; prove non-negativity of the area and the singleton-hinge identities that discharge the linearization hypothesis on the cubic lattice.
background
The module operates inside the SimplicialLedger layer that bridges the discrete RS ledger to the continuum. It imports Constants (τ₀=1 tick), ContinuumBridge (J-cost functional equals the Regge action up to normalization κ=8φ⁵; stationarity δJ=0 yields the Regge equations), and EdgeLengthFromPsi (scalar recognition potential ψ on 3-simplices determines the ten edge lengths per 4-simplex needed for the Regge action, closing the identification asserted in paper Theorem 5.1).
proof idea
This is a definition module whose lemmas are one-line wrappers or direct algebraic reductions. recoverEps and recoverEps_conformal invert the exponential self-loop relation. cubicDeficit and cubicArea are defined on the cubic lattice; cubicDeficit_singleton and cubicArea_singleton reduce to the hinge case; cubicArea_nonneg follows from the exponential form; singletonHinge_product closes the product identity required for the linearization discharge.
why it matters in Recognition Science
The module supplies the cubic_linearization_discharge step that Phase D of ContinuumTheorem composes into the unconditional field-curvature identity. It also supplies the cubic side of the equivalence treated in CubicSimplicialEquivalence (addressing Beltracchi §5) and feeds the general simplicial discharge assembled in SimplicialDeficitDischarge. The work therefore fills the cubic lattice case of the paper's Theorem 5.1.
scope and limits
- Does not prove the full simplicial discharge of the linearization hypothesis.
- Does not derive the Einstein field equations from J-cost stationarity.
- Does not address non-cubic lattices or higher-dimensional simplices.
- Does not compute numerical values of φ or α inside the module.
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