regge_sum_refinement_invariant
plain-language theorem explainer
The theorem establishes invariance of the Regge sum when a cubic hinge list is extended by a simplicial refinement whose extra hinges each carry zero deficit. Discrete gravity researchers formalizing Regge calculus on lattices would cite it to justify that triangulation leaves the action unchanged under the zero-deficit condition on internal diagonals. The proof is a one-line wrapper that unfolds the hinges field and invokes the append-trivial lemma.
Claim. Let $D$ be a deficit-angle functional and $L$ an edge-length field. Let original be a list of hinge data and let $R$ be a simplicial refinement of original (so that every extra hinge in $R$ satisfies the zero-deficit predicate). Then the Regge sum over the refined hinge list equals the sum over the original list: $regge_sum(D,L,R.hinges)=regge_sum(D,L,original)$.
background
The CubicSimplicialEquivalence module addresses the passage from cubic to simplicial formulations of the Regge action. A simplicial refinement of an original hinge list consists of the original hinges together with extra hinges on internal diagonals; the structure SimplicialRefinement requires that every extra hinge carries zero deficit on the given conformal edge-length field, witnessed by the predicate that each extra hinge is trivial under $D$ and $L$. This abstracts the Freudenthal triangulation of the 3-cube, in which internal edges have vanishing deficit because the six tetrahedra meet with dihedral angles summing to $2π$. The upstream lemma regge_sum_append_trivial states that appending any list of trivial hinges leaves the Regge sum unchanged.
proof idea
The proof is a one-line wrapper. It unfolds the definition of SimplicialRefinement.hinges (which concatenates original with the extra list) and then applies the theorem regge_sum_append_trivial to the original list, the extra list, and the extra_trivial witness.
why it matters
The result is invoked inside cubicSimplicialInvarianceCert to assemble the full invariance certificate and inside refinement_discharge_inherits to extend the cubic linearization discharge to any refinement. It supplies the structural invariance needed for cubic-simplicial equivalence, confirming that the Regge sum depends only on the original cubic edges when internal diagonals are trivial, consistent with the eight-tick octave and three-dimensional spatial structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.