IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence
The CubicSimplicialEquivalence module defines trivial hinges within cubic simplicial ledgers and establishes their zero contribution to the Regge sum whenever the deficit vanishes on the supplied edge-length field. Discrete gravity researchers in Recognition Science cite it when reducing Regge action computations on cubic lattices. The structure consists of direct predicate definitions plus append lemmas that inherit from the imported deficit discharge and continuum bridge results.
claimA hinge $h$ is trivial when its deficit vanishes, i.e., when the edge-length field satisfies the zero-deficit condition on $h$, so that the hinge contributes zero to the Regge sum.
background
The module belongs to Foundation.SimplicialLedger and imports Constants (where τ₀ = 1 tick), ContinuumBridge (which identifies the J-cost functional with the Regge action up to κ = 8φ⁵ and shows stationarity yields the Regge equations), EdgeLengthFromPsi (which maps the recognition potential ψ on 3-simplices to the full set of edge lengths), and CubicDeficitDischarge (which unconditionally discharges the ReggeDeficitLinearizationHypothesis for the RS-canonical cubic lattice). The local theoretical setting is the cubic presentation of the simplicial ledger used to promote the draft paper's Theorem 5.1 from pattern matching to a Lean theorem.
proof idea
This is a definition module, no proofs. It introduces the HingeTrivial predicate together with the supporting lemmas trivial_hinge_contribution, regge_sum_append_trivial, and regge_sum_append through direct construction from the imported edge-length and deficit objects.
why it matters in Recognition Science
The module supplies the cubic-case trivial-hinge and refinement lemmas that feed the invariance certificates (CubicSimplicialInvarianceCert) and the parent results in ContinuumBridge. It thereby advances Phase A of the four-phase program that discharges the linearization hypothesis and closes the discrete-to-EFE gap for the cubic lattice.
scope and limits
- Does not treat non-cubic lattices or general triangulations.
- Does not derive the Einstein field equations themselves.
- Does not compute numerical values of constants or alpha.
- Does not address time-dependent or evolving edge-length fields.
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