IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence
CubicSimplicialEquivalence assembles the cubic-lattice case of the simplicial ledger, defining trivial hinges via vanishing deficit on edge-length fields and proving refinement invariance. Researchers linking discrete recognition potentials to Regge calculus cite it when specializing the continuum bridge. The module collects short lemmas on hinge contributions and invariance certificates, drawing directly on imported deficit discharge and psi-derived lengths.
claimA hinge on a cubic simplicial complex is trivial (contributes zero to the Regge sum) precisely when its deficit vanishes on the edge-length field obtained from the recognition potential $\psi$. The cubic simplicial invariance certificate asserts that the Regge sum remains unchanged under refinement once the linearization hypothesis is discharged for the cubic lattice.
background
The module operates inside the Foundation.SimplicialLedger layer. Edge lengths on each tetrahedron are obtained from a scalar recognition potential $\psi$ defined on 3-simplices, as constructed in the upstream EdgeLengthFromPsi module. The J-cost functional on this ledger coincides with the Regge action (normalized by $\kappa=8\phi^5$). A hinge is trivial exactly when its deficit vanishes on the given edge-length field, contributing zero to the sum. The cubic deficit discharge module removes the linearization hypothesis unconditionally for the RS-canonical cubic presentation.
proof idea
The module is a library of small definitions and lemmas rather than one large proof. It first defines trivial hinges and the append operations on Regge sums, then shows that trivial hinges contribute zero. Refinement lemmas establish invariance by inheriting the discharged linearization property and calibrating the cubic case. All steps apply results imported from CubicDeficitDischarge and EdgeLengthFromPsi.
why it matters in Recognition Science
The module supplies the cubic simplicial invariance certificate required by the field-curvature identity (draft paper Theorem 5.1). It feeds the ContinuumBridge module, which identifies J-cost stationarity with the Regge equations and thereby with the Einstein field equations. It completes Phase A of the four-phase program that promotes the pattern-matching argument of Theorem 5.1 to a full Lean theorem.
scope and limits
- Does not treat non-cubic lattices.
- Does not derive the Einstein field equations.
- Does not include numerical lattice simulations.
- Does not address simplices in dimension greater than three.
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