rs_kappa_value
The declaration equates the Regge coupling constant to eight times phi to the fifth. Discrete gravity researchers cite it when matching the simplicial Regge action to the continuum Einstein-Hilbert term under the RS defect-to-metric map. The proof is a direct reflexivity step on the upstream definition of the constant.
claimIn the Recognition Science Regge calculus the coupling constant satisfies $k = 8 phi^5$.
background
The module formalizes exact Regge calculus on the RS lattice, replacing the linearized deficit-angle ansatz with full simplicial geometry on a Z^3 x Z lattice whose edge lengths are set by the J-cost defect field. Curvature is concentrated on codimension-2 hinges; the Regge action is the sum over hinges of area times deficit angle, and the continuum limit recovers the Einstein-Hilbert term with a specific prefactor.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity directly to the definition of rs_kappa.
why it matters in Recognition Science
This supplies the explicit value of kappa required by the Regge calculus certificate and the nonlinear convergence certificate. It closes the link between the discrete defect field and the continuum gravitational constant, consistent with the phi-ladder scaling. The parent theorems invoke it to certify flat configurations and second-order convergence of the action.
scope and limits
- Does not derive the numerical value of phi^5 from the forcing chain.
- Does not address higher-order lattice corrections beyond the continuum limit.
- Does not compute the Regge action for any specific simplex configuration.
Lean usage
kappa := rs_kappa_valueformal statement (Lean)
222theorem rs_kappa_value : rs_kappa = 8 * phi ^ 5 := rfl
proof body
Term-mode proof.
223
224/-! ## Regge Calculus Certificate -/
225