IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
The CubicDeficitDischarge module recovers the conformal parameter ε_i from self-loop edge lengths via L_ii = a exp(ε_i) and defines the cubic deficit and area functionals on the lattice. Researchers proving the discrete-to-continuum bridge in Recognition Science cite it for the cubic specialization of Regge deficit linearization. The module consists of targeted definitions and nonnegativity lemmas that discharge the linearization hypothesis on ℤ^3.
claimThe recovery map is given by $\varepsilon_i = \log(L_{ii}/a)$ for a conformal edge-length field on the cubic lattice; the associated cubic deficit functional is defined so that its stationarity reproduces the linearized Regge equations under the J-cost.
background
The module sits inside the simplicial ledger construction that identifies the J-cost functional with the Regge action (up to normalization by κ = 8φ^5) as stated in the ContinuumBridge module. Edge lengths are obtained from the recognition potential ψ on 3-simplices via the EdgeLengthFromPsi module, which supplies the ten edge lengths per 4-simplex needed for the Regge action. Constants supplies the RS time quantum τ₀ = 1 tick that normalizes all lengths.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
It supplies Phase A (cubic_linearization_discharge) for the ContinuumTheorem that establishes the field-curvature identity at κ = κ_Einstein. The module is imported by CubicSimplicialEquivalence to resolve the hypercubic-to-simplicial equivalence and by SimplicialDeficitDischarge to build the general simplicial case.
scope and limits
- Does not treat non-cubic lattices or irregular triangulations.
- Does not establish the full continuum limit or Einstein equations.
- Does not compute numerical values for constants such as α or G.
- Does not discharge the linearization hypothesis outside the cubic case.
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