ReggeCalculusCert
ReggeCalculusCert packages the consistency properties of the Regge action on the RS lattice: the action vanishes on flat configurations, deficit angles carry the expected sign relative to the sum of dihedral angles, and the coupling equals 8 phi^5. A lattice-gravity researcher cites it to confirm that the discrete curvature measure reproduces the Einstein-Hilbert term in the continuum limit. The structure is assembled directly from the definitions of deficit_angle, regge_action, and rs_kappa.
claimA certificate ReggeCalculusCert asserts: for any list of hinges, if every deficit angle vanishes then the Regge action on those hinges is zero; the identity $2π - 4·(π/2) = 0$ holds; for hinge data $h$, if the sum of dihedral angles is less than $2π$ then the deficit angle is positive; if the sum exceeds $2π$ then the deficit is negative; the constant $κ$ satisfies $0 < κ$ and $κ = 8φ^5$.
background
Regge calculus replaces smooth spacetime with a piecewise-flat simplicial complex in which curvature is concentrated on codimension-2 hinges. In this module the underlying lattice is the RS $Z^3 × Z$ grid whose edge lengths are fixed by the J-cost defect field. HingeData records the area of a hinge together with the list of dihedral angles contributed by the simplices meeting there; the deficit angle is then defined as $2π$ minus the sum of those dihedral angles. The regge_action sums area times deficit over all hinges and supplies the discrete analog of the Einstein-Hilbert action. The upstream definition rs_kappa fixes the coupling at $8φ^5$ so that the continuum limit reads $S_{Regge} → (1/2κ) ∫ R √g d^4x$.
proof idea
The declaration is a structure definition with no proof body. Each field is supplied by an upstream lemma already proved in the same module: flat_vanishes follows from the definition of regge_action, cubic_flat is an elementary trigonometric identity, deficit_positive and deficit_negative are immediate from the definition of deficit_angle, and both kappa fields are direct consequences of the definition of rs_kappa.
why it matters in Recognition Science
ReggeCalculusCert supplies the verified properties required to construct the theorem regge_calculus_cert that packages the full consistency of Regge calculus on the RS lattice. It directly implements the continuum-limit statement quoted in the module documentation, where the action inherits $κ = 8φ^5$ from the defect-to-metric mapping. Within the broader Recognition Science framework it links the discrete eight-tick octave (T7) and the emergence of three spatial dimensions (T8) to the Einstein-Hilbert action via the Recognition Composition Law.
scope and limits
- Does not derive explicit edge lengths from the underlying J-cost defect field.
- Does not prove convergence of the discrete action to the continuum integral.
- Does not address the path-integral measure or quantum corrections.
- Does not establish positivity of the action for arbitrary configurations.
Lean usage
theorem regge_calculus_cert : ReggeCalculusCert where flat_vanishes := regge_action_flat cubic_flat := cubic_lattice_flat deficit_positive := deficit_pos_of_angle_deficit deficit_negative := deficit_neg_of_angle_excess kappa_positive := rs_kappa_pos kappa_derived := rs_kappa_valueformal statement (Lean)
226structure ReggeCalculusCert where
227 flat_vanishes : ∀ hinges,
228 (∀ h ∈ hinges, deficit_angle h = 0) → regge_action hinges = 0
229 cubic_flat : 2 * Real.pi - 4 * (Real.pi / 2) = 0
230 deficit_positive : ∀ h : HingeData,
231 h.dihedral_angles.sum < 2 * Real.pi → 0 < deficit_angle h
232 deficit_negative : ∀ h : HingeData,
233 2 * Real.pi < h.dihedral_angles.sum → deficit_angle h < 0
234 kappa_positive : 0 < rs_kappa
235 kappa_derived : rs_kappa = 8 * phi ^ 5
236