regge_sum_append_trivial
plain-language theorem explainer
Appending hinges with vanishing deficit to any hinge list leaves the Regge sum unchanged. Workers on simplicial refinements of cubic lattices in Recognition Science cite the result to drop internal edges without altering the action. The proof unfolds the sum, splits the appended list via map_append and sum_append, then shows the extra sum vanishes by sum_eq_zero applied to the trivial-hinge lemma.
Claim. Let $D$ be a deficit-angle functional and $L$ an edge-length field. For hinge lists $H$ and $E$, if $D(L,h)=0$ for every hinge datum $h$ in $E$, then the Regge sum of area times deficit over $H$ concatenated with $E$ equals the sum over $H$ alone.
background
HingeTrivial is the predicate that a hinge datum $h$ satisfies $D.deficit L h = 0$ for the given functional and edge-length field; the companion lemma trivial_hinge_contribution then states that every such hinge contributes exactly zero to the Regge sum. The module establishes structural invariance between the cubic ledger and its simplicial triangulation, showing that only the original cube edges carry nonzero deficit while internal diagonals sum to $2π$ and drop out. Upstream results supply the list-append and sum identities (add_zero, List.sum_append) together with the DeficitAngleFunctional interface that defines area and deficit.
proof idea
The tactic proof unfolds regge_sum, rewrites the map over the appended list, applies List.sum_append to separate the two blocks, then invokes List.sum_eq_zero on the extra block. Inside that block it uses List.mem_map to recover each hinge datum and applies trivial_hinge_contribution to obtain zero for every term, after which add_zero finishes the equality.
why it matters
The theorem supplies the trivial-hinge-drop clause inside cubicSimplicialInvarianceCert, which in turn certifies that the Regge sum is invariant under simplicial refinement. It therefore closes one of the three structural-invariance steps required to equate the cubic ledger with the Freudenthal triangulation of the 3-cube, directly addressing the Beltracchi §5 question on whether the passage between the two formulations is content-free. The result sits inside the eight-tick octave and D=3 setting of the forcing chain, where only original hinges survive in the action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.