IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence
CubicSimplicialEquivalence module shows that a hinge contributes zero to the Regge sum precisely when its associated edge deficit vanishes on the given length field. Discrete gravity modelers cite it to confirm that cubic simplicial refinements preserve the J-cost action without extra terms. The argument assembles imported results on edge lengths from psi, cubic deficit discharge, and the continuum bridge into direct algebraic checks for trivial contributions and refinement invariance.
claimFor an edge-length field $ell$ on a cubic simplicial complex, a hinge $h$ is trivial if the deficit $delta(ell, e)=0$ on its edge $e$, which forces the Regge contribution of $h$ to vanish: $contrib(h, ell)=0$. The module also establishes that appending such trivial hinges leaves the total Regge sum invariant under refinement.
background
The module sits inside the simplicial ledger of Recognition Science, where edge lengths derive from a recognition potential psi and the J-cost functional equals the Regge action up to the factor kappa = 8 phi^5. The imported ContinuumBridge states: 'The J-cost functional on the simplicial ledger IS the Regge action (up to normalization by kappa = 8 phi^5)' and shows that stationarity of J-cost recovers the Regge equations. EdgeLengthFromPsi supplies the map from psi to the six edge lengths per tetrahedron, while CubicDeficitDischarge removes the linearization hypothesis for the RS-canonical cubic lattice, making all subsequent statements unconditional.
proof idea
The module imports Constants, ContinuumBridge, EdgeLengthFromPsi, and CubicDeficitDischarge, then defines the trivial-hinge predicate via vanishing deficit. It proves zero contribution by direct substitution into the Regge sum definition and shows refinement invariance by applying the append-trivial and discharge-inheritance lemmas. The structure consists of a sequence of one-line wrappers around the imported discharge results followed by algebraic identities for the sum over hinges.
why it matters in Recognition Science
The module advances the four-phase program to turn the draft paper's Theorem 5.1 (field-curvature identity) into a Lean theorem by discharging the cubic case of the Regge deficit linearization. It feeds the parent results on J-cost stationarity implying the Einstein equations and supplies the invariance certificates needed for the simplicial-to-continuum bridge. Without this equivalence, the discrete ledger would retain an extra hypothesis when matching the Regge action.
scope and limits
- Does not treat non-cubic lattices or irregular triangulations.
- Does not derive numerical values or bounds on the Regge sum.
- Does not address dynamical evolution of the edge-length field.
- Does not prove convergence of the discrete sum to the continuum Einstein-Hilbert action.
depends on (4)
declarations in this module (11)
-
def
HingeTrivial -
theorem
trivial_hinge_contribution -
theorem
regge_sum_append_trivial -
theorem
regge_sum_append -
theorem
regge_sum_nil -
structure
SimplicialRefinement -
theorem
regge_sum_refinement_invariant -
theorem
refinement_discharge_inherits -
theorem
refinement_calibrated -
structure
CubicSimplicialInvarianceCert -
theorem
cubicSimplicialInvarianceCert