regge_sum_flat_under_linearization
plain-language theorem explainer
The theorem shows that whenever the Regge deficit linearization hypothesis holds, the Regge sum vanishes for the flat vacuum configuration of the conformal edge-length field. Researchers deriving the field-curvature identity between J-cost Dirichlet energy and linearized Regge action cite it to confirm normalization of the overall constant. The proof is a one-line wrapper that instantiates the hypothesis at zero log-potential, substitutes the flat Laplacian identity, and reduces by algebraic simplification.
Claim. Let $D$ be a deficit-angle functional on $n$ vertices, let $a>0$, let $H$ be a list of hinge data, and let $G$ be a weighted ledger graph. If the linearization hypothesis holds for these data, then the Regge sum of $D$ evaluated on the conformal edge-length field at zero log-potential equals zero.
background
A DeficitAngleFunctional supplies, for any edge-length field, the deficit angle and area at each hinge; the Regge sum is then the weighted sum of area times deficit. The ReggeDeficitLinearizationHypothesis is the statement that this sum equals a fixed multiple of the Laplacian action of the log-potential around the flat vacuum. The conformal_edge_length_field converts a log-potential ε into an edge-length assignment via the scale a and the exponential map, so that ε ≡ 0 recovers the flat metric. The module supplies the missing map from recognition potential ψ to geometric edge lengths that turns the J-cost Dirichlet energy into a genuine Regge action once the linearization hypothesis is discharged. Upstream results include the definition of the gravitational constant G in RS-native units and the flat Laplacian identity laplacian_action_flat.
proof idea
The proof is a one-line wrapper. It applies the linearization hypothesis to the zero log-potential, rewrites the resulting expression using the flat Laplacian identity, and concludes by ring simplification.
why it matters
The result is invoked inside edgeLengthFromPsiCert as the flat_regge component that completes the field-curvature identity. It corresponds to the consistency check in the Gravity from Recognition draft §5 that fixes the constant in the identification of J-cost with the linearized Regge action at coupling κ = 8 φ^5. It touches the open question of discharging the linearization hypothesis itself via explicit Cayley-Menger determinants or the Piran-Williams 3+1 split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.