schlafli_identity
plain-language theorem explainer
The declaration encodes the Schläfli identity from Regge calculus as the proposition that the sum over hinges of area times the partial derivative of deficit angle with respect to edge length vanishes identically. Discrete gravity modelers in the Recognition Science programme would cite it when constructing the Regge action or checking flat configurations on the simplicial lattice. The definition is a direct packaging of the geometric statement into a universal quantification over hinge lists and derivative lists.
Claim. The Schläfli identity asserts that for any list of hinge data and any list of real numbers $d_delta_dL$, the sum of the products of each hinge area and the corresponding derivative of its deficit angle vanishes: $∑_h A_h (d δ_h / d L_e) = 0$.
background
The module formalizes exact Regge calculus on the RS lattice, replacing linearized deficit-angle approximations with the full nonlinear machinery. Curvature is concentrated on codimension-2 hinges; HingeData records the area and deficit angle at each such hinge. Edge lengths are set by the J-cost defect field, with the defect functional defined as defect(x) := J(x) and recognition-event costs given by Cost.Jcost. The local setting is the piecewise-flat simplicial complex on Z^3 × Z, with the Regge action S_Regge = ∑ A_h δ_h.
proof idea
This is a direct definition that packages the universal quantification over hinge lists and derivative lists into a single Prop. No lemmas or tactics are invoked; the body is the mathematical statement of the identity itself.
why it matters
The definition supplies the geometric identity that underpins the Regge action and its flatness properties in the Recognition Science discrete gravity programme. It supports module results such as regge_action_nonneg_flat and regge_action_gauss_bonnet. In the broader framework it ensures consistency of the piecewise-flat lattice with the J-cost defect field that determines the metric perturbation h in g = η + h, linking to the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.