regge_sum_append
plain-language theorem explainer
The theorem establishes additivity of the Regge sum under concatenation of hinge lists. Researchers formalizing the cubic-to-simplicial equivalence in Regge calculus cite it when separating original and refinement hinges. The proof is a direct one-line wrapper that expands the sum definition and applies the standard append rules for mapped lists and their totals.
Claim. Let $D$ be a deficit-angle functional and $L$ an edge-length field. For any two lists of hinge data $h_1$ and $h_2$, the Regge sum over their concatenation equals the sum of the separate Regge sums: $S(D,L,h_1++h_2)=S(D,L,h_1)+S(D,L,h_2)$, where $S$ denotes the sum of area times deficit supplied by $D$.
background
In the module establishing cubic-simplicial equivalence for Regge calculus, the Regge sum is the total action obtained by summing, over a list of hinges, the product of the area and the deficit angle at each hinge. A DeficitAngleFunctional supplies both the deficit map and the area map from an edge-length field to each hinge datum. An EdgeLengthField records positive symmetric lengths on ordered pairs of vertices, while a HingeDatum records the edges incident to the hinge together with nonnegative weights. The upstream definition of the Regge sum is exactly this finite sum of area-deficit products.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the Regge sum, then rewrites by the append law for list mapping and the append law for summation of reals.
why it matters
This theorem supplies the regge_append field of the CubicSimplicialInvarianceCert. That certificate certifies the structural invariance needed to equate the cubic ledger with its simplicial triangulation. It directly addresses the module's resolution of Beltracchi §5 by showing that the total Regge sum is unaffected by concatenation with zero-deficit refinement hinges, thereby confirming that the passage between the two discretizations introduces no new content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.