rs_kappa
The RS Regge coupling constant is defined as eight times the fifth power of the golden ratio. Discrete gravity researchers matching the simplicial Regge action to the Einstein-Hilbert action in the continuum limit would cite this value when extracting the prefactor from the defect-to-metric map. The definition is a direct assignment with no lemmas or computation required.
claimThe Regge coupling constant is defined by $k_{RS} := 8 phi^5$, where $phi$ is the golden ratio fixed point.
background
In the Recognition Science lattice the spacetime is a Z^3 x Z simplicial complex whose edge lengths are set by the J-cost defect field. Regge calculus concentrates curvature on codimension-2 hinges; the action is the sum over hinges of (area times deficit angle). The continuum limit replaces this sum by (1/2 kappa) times the integral of the scalar curvature times sqrt(g) d^4x. The module imports Constants to obtain phi and the forcing-chain results that fix its value. Upstream results on the phi-ladder and the eight-tick octave supply the numerical coefficient that appears in the defect-to-metric mapping.
proof idea
The declaration is a direct definition that assigns the constant 8 * phi ^ 5 to rs_kappa. No tactics or lemmas are invoked; the body is a single expression that later theorems unfold to obtain positivity and equality statements.
why it matters in Recognition Science
This supplies the explicit value of kappa required by the RSReggeConvergence structure and the NonlinearConvergenceCert, which together assert that the Regge action converges to the Einstein-Hilbert action with second-order error controlled by this kappa. It thereby closes the matching between discrete defect dynamics and continuum gravity inside the Recognition framework. The same constant appears in ReggeCalculusCert and is used to certify flat configurations and positive deficits. The value 8 phi^5 is inherited from the defect-to-metric map and is consistent with the T8 forcing step that yields three spatial dimensions.
scope and limits
- Does not prove convergence of the Regge action to the Einstein-Hilbert integral.
- Does not derive the numerical coefficient from J-cost minimization.
- Does not compute explicit numerical approximations beyond the symbolic expression in phi.
Lean usage
theorem rs_kappa_value : rs_kappa = 8 * phi ^ 5 := rflformal statement (Lean)
217noncomputable def rs_kappa : ℝ := 8 * phi ^ 5
proof body
Definition body.
218