regge_sum_nil
plain-language theorem explainer
The Regge sum over an empty hinge list vanishes for any deficit angle functional and edge length field. Researchers establishing cubic-to-simplicial invariance in the Recognition Science ledger would cite this nil case as the base for inductive arguments on hinge lists. The proof is a one-line wrapper that unfolds the sum definition and simplifies the empty-list case.
Claim. For any natural number $n$, deficit angle functional $D$, and edge length field $L$, the sum of deficit angles over the empty collection of hinges equals zero.
background
The module addresses the cubic-to-simplicial equivalence by showing that the hypercubic ledger is compatible with Regge calculus on simplicial complexes. A deficit angle functional assigns to each hinge the value $2π$ minus the sum of dihedral angles at that hinge; an edge length field supplies the lengths required to evaluate those angles. The Regge sum aggregates these deficits over a list of hinges. Internal diagonals introduced by the Freudenthal triangulation of a cube carry zero deficit because the six tetrahedra meet with dihedral angles summing exactly to $2π$.
proof idea
The proof is a one-line wrapper that unfolds the definition of the Regge sum and applies the simplifier to the empty-list case.
why it matters
This nil case anchors the structural invariance results that establish cubic-simplicial equivalence, directly supporting the claim that only original cube edges carry non-zero deficit while refinement hinges drop out. It fills the base step needed for the module's proofs that the Regge sum is unchanged under addition of zero-deficit hinges, addressing Beltracchi §5 on whether the passage from the ℤ³ ledger to simplicial Regge calculus is content-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.