refinement_discharge_inherits
plain-language theorem explainer
The theorem shows that if every simplicial refinement of the cubic hinges satisfies the zero-deficit condition on extra hinges for a conformal edge-length field, then the Regge sum over the full refined hinge list equals the calibrated Laplacian action on the ledger graph. Researchers comparing cubic and simplicial discretizations of Recognition Science gravity would cite it to justify triangulation invariance. The proof is a one-line wrapper that rewrites via the refinement-invariance lemma and discharges with the cubic linearization result.
Claim. Let $n$ be a natural number, $a>0$, $G$ a weighted ledger graph, and suppose that for every log-potential $ε$ the structure $R_ε$ is a simplicial refinement of the cubic hinges under the conformal edge-length field of scale $a$, so that every extra hinge carries zero deficit. Then for every $ε$, the Regge sum of the cubic deficit functional over the refined hinge list equals $8φ^5$ times the discrete Laplacian action of $G$ on $ε$.
background
The SimplicialRefinement structure augments the original cubic hinges with an extra list of internal hinges, each required to satisfy the HingeTrivial predicate (zero deficit) on the given conformal edge-length field; this encodes the Freudenthal triangulation of the 3-cube without altering vertex sets. The constant jcost_to_regge_factor is defined as $8φ^5$, the unique normalization matching J-cost to Regge action via the calibration axiom that J''(1)=1. The laplacian_action on a weighted graph $G$ is the quadratic form $(1/2)∑{i,j} w{ij}(ε_i-ε_j)^2$ that represents the discrete J-cost energy.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side by applying regge_sum_refinement_invariant to the cubicDeficitFunctional, the conformal field, the cubic hinges, and the supplied refinement R_at ε; the resulting expression is then discharged exactly by the upstream cubic_linearization_discharge lemma.
why it matters
The result is invoked inside the construction of CubicSimplicialInvarianceCert and inside the proof of the refinement_calibrated corollary. It supplies the structural invariance step that answers Beltracchi §5 by showing the Regge action is unchanged under zero-deficit refinement, thereby supporting the D=3 ledger equivalence in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.