cubicSimplicialInvarianceCert
plain-language theorem explainer
The cubic and simplicial Regge sums coincide for the same ledger data when internal refinement hinges carry zero deficit. A physicist comparing discrete gravity models to the Recognition Science J-cost would cite this result to treat cubic and simplicial discretizations as interchangeable. The proof is a term-mode wrapper that populates the four fields of the CubicSimplicialInvarianceCert structure by direct application of four prior lemmas.
Claim. Let $D$ be a deficit-angle functional and $L$ an edge-length field on an $n$-dimensional ledger. The Regge sum is additive under concatenation of hinge lists, drops any list of trivial hinges, remains unchanged under simplicial refinement of the underlying cubic structure, and the cubic linearization discharge extends automatically to refinements whose extra hinges satisfy the zero-deficit condition.
background
Recognition Science models the ledger either as a hypercubic lattice or as a simplicial complex. The module proves their structural equivalence without constructing the full Freudenthal triangulation of each 3-cube. The SimplicialLedger is defined as a nonempty set of 3-simplices that cover a manifold; internal diagonals introduced by subdivision carry zero deficit on the conformal field, so only the original cube edges contribute to the Regge action. The CubicSimplicialInvarianceCert is the master diagnostic asserting that the J-cost to Regge identification is identical in both presentations under this zero-deficit hypothesis on internal hinges.
proof idea
The proof is a one-line term-mode wrapper. It supplies the regge_append field by regge_sum_append, the trivial_hinge_drop field by regge_sum_append_trivial, the refinement_invariant field by regge_sum_refinement_invariant, and the refinement_discharge field by refinement_discharge_inherits.
why it matters
This theorem supplies the Lean-level answer to Beltracchi §5 by certifying that the cubic and simplicial presentations of the ledger yield the same J-cost ↔ Regge identification. It closes the structural gap between the ℤ³ lattice and Regge calculus on simplicial complexes while preserving the eight-tick octave and D=3 landmarks of the forcing chain. The result is a prerequisite for any downstream claim that the Recognition Science action is discretization-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.