CubicSimplicialInvarianceCert
plain-language theorem explainer
The CubicSimplicialInvarianceCert structure certifies that Regge sums on cubic hinges are unchanged by simplicial refinement when internal diagonals carry zero deficit, and that the refined sum equals 8 phi^5 times the discrete Laplacian action. Researchers comparing cubic and simplicial presentations of the Recognition Science ledger would cite it to justify that the J-cost to Regge identification is triangulation-independent. The structure is assembled directly from four sibling lemmas establishing additivity, trivial-hinge cancellation, and
Claim. Let $D$ be a deficit-angle functional and $L$ an edge-length field on $n$ vertices. A CubicSimplicialInvarianceCert consists of: (i) additivity of the Regge sum over concatenated hinge lists; (ii) invariance of the Regge sum when a list of trivial hinges (those with zero deficit under $D$ and $L$) is appended; (iii) invariance of the Regge sum under any simplicial refinement whose extra hinges are trivial; (iv) equality of the refined Regge sum to $8phi^5$ times the Laplacian action of a weighted ledger graph $G$ on a log-potential $varepsilon$, when $L$ is the conformal edge-length field scaled by positive $a$.
background
In the Recognition Science ledger the canonical geometry is the integer lattice whose edges carry deficit angles computed from the J-functional. Regge calculus is formulated on simplicial complexes, so the module isolates the structural properties that make the two presentations equivalent. A hinge is trivial when its deficit vanishes on the given edge-length field. A simplicial refinement augments the original cubic hinges by extra internal diagonals, all required to be trivial under the conformal edge-length field. The upstream jcost_to_regge_factor is defined as $8phi^5$, the unique constant matching the second derivative of J at 1 to the conventional $1/(8pi G)$ normalization of the Regge action. The laplacian_action is the quadratic form $frac12 sum_{i,j} w_{ij}(varepsilon_i - varepsilon_j)^2$ that represents the J-cost on the weighted graph.
proof idea
The declaration is a structure definition whose four fields are supplied by sibling lemmas already proved in the same module: regge_sum_append for additivity, regge_sum_append_trivial for dropping trivial hinges, regge_sum_refinement_invariant for invariance under refinement, and the explicit matching in refinement_discharge that invokes jcost_to_regge_factor and laplacian_action. No additional tactics are required; the structure simply packages these four statements.
why it matters
This certificate directly resolves the cubic-versus-simplicial equivalence question raised in Philip Beltracchi's section 5. It shows that the J-cost to Regge identification, with coupling kappa = 8 phi^5, is independent of the choice of triangulation. The downstream theorem cubicSimplicialInvarianceCert assembles the certificate from the four sibling lemmas and thereby closes the invariance argument. In the broader framework the result confirms that the eight-tick octave and three-dimensional spatial structure can be realized equally well on cubic or simplicial lattices without altering the physical content of the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.