flat_regge_sum_zero
plain-language theorem explainer
The theorem shows that the Regge sum of the cubic deficit functional vanishes on the conformal edge-length field generated by the zero perturbation. Researchers assembling the linearized Einstein equations from the Recognition Composition Law would cite it to anchor the flat-vacuum baseline. The term proof reduces the sum via the cubic linearization discharge to a multiple of the Laplacian action on the zero field, which is zero by the flat-action lemma.
Claim. Let $n$ be a natural number, $a>0$ a real scalar, and $G$ a weighted ledger graph. Then the Regge sum of the cubic deficit functional on the conformal edge-length field produced by the zero perturbation equals zero: $$regge_sum(cubicDeficitFunctional(n), conformal_edge_length_field(a, zero), cubicHinges(G)) = 0.$$
background
The ContinuumTheorem module assembles Phase D of the program to realize the paper's Theorem 5.1 as an unconditional result. It composes the cubic linearization discharge with the normalization of the bridge factor to the Einstein coupling. The J-cost Dirichlet energy is realized as the Laplacian action on a perturbation field ε, while the Regge sum integrates the cubic deficit over the hinges of G. The upstream cubic_linearization_discharge equates the Regge sum to the scaled Dirichlet energy for arbitrary ε, and laplacian_action_flat records that the action on the zero field is identically zero. The module documentation states that the construction yields the exact linearized identity with the Einstein coupling and the flat-vacuum baseline.
proof idea
The proof is a short term-mode reduction. It applies cubic_linearization_discharge a ha G (zero field) to obtain equality with jcost_to_regge_factor times laplacian_action G (zero field), then rewrites the second factor via laplacian_action_flat and concludes by multiplication with zero.
why it matters
The corollary supplies the flat_regge component inside the ContinuumFieldCurvatureCert and is invoked by bridge_chain_complete. It confirms the vanishing at the flat vacuum required by the module documentation on the complete cubic bridge chain. The result closes the zero-energy case in the forcing sequence that runs from the Recognition Composition Law through J-uniqueness and φ-forcing to the linearized Einstein equations with coupling κ_Einstein = 8 φ^5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.