regge_action_flat
plain-language theorem explainer
When every hinge in a Regge triangulation has vanishing deficit angle, the total action formed by summing area times deficit over all hinges is zero. Discrete-gravity calculations in Recognition Science invoke this to confirm that flat space is a critical point of the discrete Einstein-Hilbert action. The proof unfolds the action definition, reduces the list of terms to the zero list by pointwise substitution, and closes with the arithmetic identity that any quantity times zero vanishes.
Claim. If $h$ ranges over a list of hinges and the deficit angle satisfies $2π - ∑ dihedral angles at $h$ equals zero for every $h$, then the Regge action $S = ∑_h A_h δ_h$ equals zero.
background
The module replaces the linearized deficit-angle ansatz of the paper with exact Regge calculus on a Z^3 × Z lattice whose edge lengths are fixed by the J-cost defect field. A HingeData record stores the area of a codimension-2 face together with the list of dihedral angles contributed by the simplices that meet there; the deficit angle is defined as 2π minus that sum. The Regge action is the sum over all such hinges of area times deficit angle, exactly as written in the 1961 Regge formulation.
proof idea
The term-mode proof first unfolds regge_action to expose the explicit sum. It then introduces a suffices goal asserting that the list obtained by mapping area times deficit equals the constant-zero list. List.map_congr_left reduces the goal to a pointwise statement; the flatness hypothesis rewrites each deficit to zero and mul_zero converts the product to zero. A final simp discharges the list equality.
why it matters
regge_calculus_cert imports this result as the flat_vanishes field of its certificate, thereby confirming that the discrete Einstein equations are satisfied in the flat limit. The module documentation states that the construction replaces Assumption A2 of the paper with the full nonlinear Regge machinery, consistent with the eight-tick octave and the emergence of D = 3 spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.