regge_equations_statement
plain-language theorem explainer
regge_equations_statement encodes the stationarity condition for the Regge action on the discrete lattice. Discrete gravity researchers cite it when deriving the simplified Einstein equations after the Schläfli identity removes the area-weighted dihedral derivative term. The definition directly asserts that for any collection of hinges a matching list of area derivatives exists whose weighted sum with the deficit angles vanishes.
Claim. For every list of hinges there exists a list of real numbers of equal length such that the sum of each entry times the deficit angle of the corresponding hinge equals zero.
background
The module sets up exact Regge calculus on the Recognition Science lattice, replacing smooth spacetime by a piecewise-flat simplicial complex whose curvature resides only at codimension-2 hinges. The Regge action is the sum over hinges of area times deficit angle, with edge lengths fixed by the J-cost defect field on the Z^3 × Z lattice. HingeData collects the area and deficit angle at each hinge; deficit_angle extracts the angular defect from the dihedral data.
proof idea
This is a direct definition. The body states the Regge equations as the existence, for every list of hinge data, of a list of area derivatives whose dot product with the list of deficit angles is identically zero. No lemmas or tactics are invoked; the expression simply transcribes the simplified stationarity condition obtained once the Schläfli identity has eliminated the second term in the variation.
why it matters
The definition supplies the precise statement of the discrete Einstein equations inside the Recognition Science framework. It supports the module results on nonnegativity of the Regge action for flat configurations and the Gauss-Bonnet relation for closed surfaces. It replaces the linearized deficit-angle ansatz with the full nonlinear Regge machinery and aligns with the three spatial dimensions and eight-tick structure of the underlying lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.