regge_sum
plain-language theorem explainer
regge_sum defines the discrete Regge action on a simplicial complex as the sum over a list of hinges of area times deficit angle, both evaluated from a given edge-length field. Researchers citing the field-curvature identity in the Recognition Science draft would reference this definition when writing the right-hand side of the J-cost to Regge bridge. The definition is a direct one-line sum that applies the area and deficit maps of the supplied DeficitAngleFunctional to each HingeDatum.
Claim. $S(D, L, h) = ∑_h A(L, h) · δ(L, h)$, where $A$ and $δ$ are the area and deficit maps of the functional $D$, $L$ is the conformal edge-length field on the graph, and the sum runs over the supplied list of hinge data.
background
DeficitAngleFunctional is a structure supplying two maps from an EdgeLengthField and a HingeDatum to reals: one for the deficit angle at the hinge and one for the associated area (with a positivity axiom on the area). EdgeLengthField is a structure that records a base spacing together with a symmetric positive length function on ordered pairs of vertices; the canonical conformal case sets each length to base_spacing times exp of the average log-potential on its endpoints. HingeDatum packages the list of edges incident to a hinge together with nonnegative weights on those edges.
proof idea
This is a one-line wrapper that applies the map sending each hinge datum to the product of its area and deficit under the given functional and edge-length field, then takes the sum of the resulting list of reals.
why it matters
The definition supplies the right-hand side of the field-curvature identity theorems in ContinuumTheorem (field_curvature_identity_einstein and the cubic variant), where the J-cost Dirichlet energy equals (1/κ) times this sum with κ fixed to 8 φ^5. It is invoked directly by bridge_chain_complete, ContinuumFieldCurvatureCert, flat_regge_sum_zero, and the cubic discharge certificates. The surrounding module supplies the missing geometric map from the recognition potential to edge lengths so that the draft's Theorem 5.1 becomes a genuine identity once the linearization hypothesis is discharged via Piran–Williams or Cheeger–Müller–Schrader.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.