regge_calculus_cert
plain-language theorem explainer
The certificate establishes that the Regge action vanishes on flat hinge sets, the cubic lattice has zero deficit, deficits carry the correct sign from angle sums, and kappa equals 8 phi^5. Discrete gravity researchers cite it to confirm the simplicial RS lattice reproduces the Einstein-Hilbert action in the continuum limit. The proof is a direct term-mode structure construction that assigns the supporting lemmas to each field of ReggeCalculusCert.
Claim. The structure ReggeCalculusCert holds: the Regge action vanishes whenever all deficit angles are zero; the cubic lattice satisfies $2π - 4(π/2) = 0$; deficit angles are positive when the sum of dihedral angles is less than $2π$ and negative when greater; and $κ = 8φ^5$ with $κ > 0$.
background
The module formalizes exact Regge calculus on the RS lattice $Z^3 × Z$, with curvature at codimension-2 hinges. The Regge action is $S = ∑ A_h δ_h$ where $A_h$ is hinge area and $δ_h$ the deficit angle. Edge lengths come from the J-cost defect field. Key definitions are HingeData (area and dihedral angles) and rs_kappa := 8 φ^5, which appears in the continuum limit $S_{Regge} → (1/2 κ) ∫ R √g d^4x$.
proof idea
The proof is a term-mode structure construction. It populates flat_vanishes with regge_action_flat, cubic_flat with cubic_lattice_flat, deficit_positive with deficit_pos_of_angle_deficit, deficit_negative with deficit_neg_of_angle_excess, kappa_positive with rs_kappa_pos, and kappa_derived with rs_kappa_value.
why it matters
This certificate supplies the core properties needed to replace the linearized deficit ansatz with full Regge machinery in the RS discrete gravity programme. It inherits κ = 8 φ^5 from the defect-to-metric mapping and aligns with the eight-tick octave and D = 3 spatial dimensions. No downstream theorems are recorded yet, but the result grounds the continuum limit to the Einstein-Hilbert action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.