kappa_RS
plain-language theorem explainer
kappa_RS supplies the Recognition Science value of the Einstein constant in native units as eight times phi raised to the coherence exponent. Researchers deriving gravitational constants from the Recognition framework cite it when verifying consistency with the Einstein relation or assembling Planck-scale quantities. The definition is obtained by direct substitution of the coherence exponent value of five into the algebraic expression.
Claim. $k_{RS} = 8 phi^{5}$, where $phi$ is the golden ratio fixed point and the exponent 5 is the coherence exponent fixed by the three-dimensional forcing chain.
background
The module assembles RS-native constants once the coherence exponent is fixed at 5. In native units with $c=1$, the Planck constant satisfies $hbar = phi^{-5}$. The coherence exponent is defined as the natural number 5, which is forced uniquely at $D=3$ by the Fibonacci route $k_{fib}(D)=2^D - D =5$ and the integration route $k_{int}(D)=D+2=5$, as recorded in the module documentation. The upstream result coherenceExponent from CoherenceExponentUniqueness supplies this value of 5.
proof idea
This is a one-line definition that substitutes the value of coherenceExponent (the natural number 5) into the expression 8 multiplied by phi raised to that power. No lemmas or tactics are applied beyond the built-in definition of real exponentiation.
why it matters
The definition supplies the kappa_RS value used to prove the Einstein relation kappa_RS = 8 pi G_RS in the same module, where G_RS = phi^5 / pi. It is bundled into the PlanckConstantCert structure that certifies positivity and structural consistency for the SM constants. In the Recognition framework it realizes the T8 step that fixes D=3 and the resulting k=5, enabling algebraic derivation of gravitational constants without external input. It is referenced in nonlinear convergence and Regge calculus results to maintain dimensional consistency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.