rs_kappa_value
plain-language theorem explainer
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.
Claim. In 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.