regge_action
plain-language theorem explainer
The declaration defines the Regge action on a list of hinges as the sum of each hinge area multiplied by its deficit angle. Discrete gravity researchers and Recognition Science lattice modelers cite it as the exact combinatorial replacement for the Einstein-Hilbert action. The definition is a direct one-line map-and-sum construction that applies the sibling deficit_angle function to each HingeData record.
Claim. $S(h_1, h_2, ...) = A_1 delta_1 + A_2 delta_2 + ...$ where each $h_i$ is a hinge record carrying area $A_i > 0$ and a list of dihedral angles, and $delta_i = 2 pi - sum theta_j$ is the deficit angle at that hinge.
background
The ReggeCalculus module replaces the linearized deficit ansatz with full nonlinear Regge calculus on a Z^3 x Z lattice whose edge lengths come from the J-cost defect field. HingeData is the structure that records the area of a codimension-2 hinge (triangle in 4D), the list of dihedral angles contributed by adjacent 4-simplices, and the proof that the area is positive. The sibling deficit_angle function then returns 2 pi minus the sum of those dihedral angles.
proof idea
The definition is a one-line wrapper that applies map to the input list, sending each HingeData record to the product of its area field and the value of deficit_angle on that record, then sums the resulting list of reals.
why it matters
This definition supplies the central action functional used by FieldCurvatureBridge to equate the ledger J-cost energy with a kappa-normalized Regge action. It is invoked directly by the theorem jcost_stationarity_implies_regge, which shows that J-cost stationarity implies Regge stationarity, and by ReggeCalculusCert, which records that the action vanishes on flat configurations and inherits kappa = 8 phi^5 in the continuum limit. The construction closes the link from the phi-ladder mass formula to the Einstein-Hilbert action while remaining purely combinatorial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.