regge_sum_cubicHinges
plain-language theorem explainer
The theorem states that the Regge sum of the cubic deficit functional over the hinges of any weighted ledger graph G, evaluated on conformal edge lengths from a log-potential ε, equals (κ/2) times the Finset sum of G.weights times squared potential differences. Workers discharging the ReggeDeficitLinearizationHypothesis for cubic lattices in Recognition Science cite this identity when reducing curvature to a quadratic form. The proof unfolds the sum and hinges, applies the pointwise singletonHinge_product identity to each term, converts the map
Claim. Let κ = jcost_to_regge_factor. For natural number n, positive real a, log-potential ε on n vertices, and weighted ledger graph G, the sum over hinges h in cubicHinges(G) of (area of h computed from conformal edge lengths of ε) times (deficit of h) equals (κ/2) times ∑_{i,j} G.weight(i,j) (ε_i − ε_j)^2, where the area at each hinge is (κ/2) G.weight(i,j) and the deficit is the squared difference (ε_i − ε_j)^2.
background
The module discharges the ReggeDeficitLinearizationHypothesis for the RS-canonical cubic lattice by constructing a leading-order deficit functional. WeightedLedgerGraph n supplies vertex weights and nonnegativity; LogPotential n is a real-valued function on Fin n. cubicDeficitFunctional n returns, for each hinge, the product of hinge area (κ/2 times weight) and deficit (squared log-potential difference). conformal_edge_length_field a ha ε converts ε to edge lengths via the exponential map. jcost_to_regge_factor is defined as 8 φ^5, the normalization that matches J-cost curvature to the Regge action (1/(8πG) = 1/κ). Upstream, the structure as in ContinuumBridge records the identification (1/2) Σ w_ij (ε_i − ε_j)^2 = (1/κ) Σ δ_h A_h.
proof idea
The tactic proof unfolds regge_sum, cubicHinges and cubicDeficitFunctional, then rewrites the double map. It establishes a pointwise equality h_point for every pair ij by calling singletonHinge_product a ha ε. A second lemma h_sum converts the list sum over Finset.univ.toList into a Finset sum via List.sum_toFinset and toList_toFinset. The main calc applies List.map_congr_left to replace each term, then uses Finset.mul_sum and ring to factor out κ/2.
why it matters
This identity is the exact linearization step required by cubic_linearization_discharge, which in turn feeds field_curvature_identity_under_linearization and thereby the paper's Theorem 5.1. It realizes the quadratic truncation of the Regge deficit that matches the second derivative of J at 1 (T5 J-uniqueness) and the eight-tick octave structure. The result closes Phase A of the four-phase program; higher-order O(ε^3) remainders are deferred to Phase D via CubicReggeProof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.