HingeData
plain-language theorem explainer
HingeData packages the area and incident dihedral angles for a codimension-2 hinge in a Regge-calculus triangulation on the RS lattice. Discrete gravity workers cite it when assembling the action or verifying curvature signs via deficit formulas. The declaration is a plain structure with an area field, an angle list, and a positivity witness.
Claim. A hinge carries a positive area $A > 0$ and a list of dihedral angles $θ_i$ whose sum determines the curvature deficit via $2π - ∑ θ_i$.
background
The module replaces smooth spacetime by a simplicial complex on the $ℤ^3 × ℤ$ lattice whose edge lengths come from the J-cost defect field. Curvature concentrates on codimension-2 hinges. HingeData collects the geometric data needed to compute the deficit angle. Upstream lemmas in Geometry.DihedralAngle and Schlaefli define that deficit explicitly as $2π$ minus the sum of the listed angles. The setting follows the full nonlinear Regge calculus, superseding the linearized deficit ansatz of the paper.
proof idea
The declaration introduces the structure directly by enumerating its three fields. No lemmas or tactics are invoked; the definition stands alone as a record type.
why it matters
Downstream results such as deficit_angle, regge_action, and flat_deficit_zero apply this structure to form the discrete Einstein-Hilbert action $S = ∑ A_h δ_h$. It supplies the input type for the discrete conservation statement in DiscreteBianchi. Within the framework it realizes the Regge step that concentrates curvature on hinges while preserving the eight-tick periodicity and three spatial dimensions of the underlying lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.