rs_efe_kappa
plain-language theorem explainer
In the RS-derived Einstein equations the coupling equals $8\phi^5$, fixed by the golden ratio rather than fitted. Gravity theorists auditing the continuum limit cite this for the sourced-EFE normalization. The proof is a one-line appeal to the already-proved Regge-calculus evaluation of kappa.
Claim. The Einstein coupling constant in the RS full-EFE data package equals $8\phi^{5}$.
background
Classical GR writes $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$ with $\kappa=8\pi G/c^4$. Recognition Science works in native units $c=1$ and $G=\phi^5/\pi$, so $\kappa$ collapses algebraically to $8\phi^5$. The same $\phi$ is forced earlier in the chain (T5 J-uniqueness, T6 self-similar fixed point), and $\hbar=\phi^{-5}$ sits in the same unit system.
Module FullEFE packages the nonlinear sourced EFE from the RS discrete ledger, conditional on Regge convergence. Its derivation chain lists eight steps; step 8 is precisely "kappa = 8*phi^5 is derived (from phi, not fitted)." The data record holding dimension and couplings is the carrier of that constant.
Upstream, ReggeCalculus already evaluates the discrete-action coupling as $8\phi^5$. This theorem simply installs that value into the FullEFE data package.
proof idea
One-line term proof. The goal is definitionally the statement already proved as rs_kappa_value in ReggeCalculus, so the proof is just that lemma. No fresh algebra occurs here; FullEFE inherits the Regge identity.
why it matters
Closes step 8 of the FullEFE chain: the Einstein coupling is derived from $\phi$, not fitted. Downstream, full_gr_certificate records it as the kappa_derived field of the FullGRCertificate (alongside dimension, positivity, and Bianchi conservation). The dark-energy extension reuses it verbatim as lambda_efe_kappa. Together these complete the claim that RS recovers the full sourced Einstein equations with a parameter-free $\kappa=8\phi^5$, consistent with native $G=\phi^5/\pi$ and $c=1$. The remaining open piece of the parent chain is nonlinear Regge convergence, still axiomatized rather than formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.