refinement_calibrated
plain-language theorem explainer
The theorem shows that for any weighted ledger graph G and simplicial refinement R_at of its cubic hinges under a conformal edge length field with scale a, the Regge sum computed on the full refined hinge list equals the J-cost-to-Regge factor times the Laplacian action of G on every log potential ε. Researchers formalizing Regge calculus inside Recognition Science would cite it to confirm that triangulation choices leave the calibrated ledger identity unchanged. The proof is a direct one-line application of the discharge inheritance lemma.
Claim. Let $n$ be a natural number, $a>0$, $G$ a weighted ledger graph, and let $R$ be a simplicial refinement of the cubic deficit functional on the conformal edge-length field of scale $a$ whose extra hinges carry zero deficit. Then for every log potential $ε$, the Regge sum of the cubic deficit functional over the refined hinge list equals $κ$ times the Laplacian action of $G$ on $ε$, where $κ$ is the J-cost-to-Regge conversion factor.
background
A simplicial refinement of a cubic hinge list consists of the original cubic hinges together with additional internal hinges (face diagonals and body diagonals) that are required to carry zero deficit on any conformal edge-length field; this structure abstracts the Freudenthal triangulation of the 3-cube while preserving the vertex set. The local setting is the cubic-to-simplicial equivalence module, which addresses Beltracchi §5 by proving structural invariance: zero-deficit internal hinges drop out of the Regge sum and the original cubic deficits are recovered unchanged. The result rests on the upstream lemma refinement_discharge_inherits together with the additive decomposition of the Regge sum over hinge classes.
proof idea
The proof is a one-line wrapper that applies the lemma refinement_discharge_inherits to the parameters a, ha, G and the refinement hypothesis R_at.
why it matters
This corollary establishes that the CalibratedAgainstGraph predicate carries over from the cubic presentation to its simplicial refinement, so the J-cost ↔ Regge identification remains the same equation with the same coupling $κ=8φ^5$. It directly fills the invariance step required by the Recognition Science ledger framework (T8 fixing D=3 and the RCL) and answers the triangulation-independence question raised in Beltracchi §5. The result closes one open presentation choice in the forcing chain without introducing new physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.