rs_vacuum_efe
plain-language theorem explainer
For the RS Einstein-field data package, the vacuum sector is well-posed: cosmological constant zero, gravitational coupling exactly $8\phi^5$, and that coupling strictly positive. Gravity and continuum-limit workers cite it as the vacuum certificate on the FullEFE chain. The proof is a one-line term that packages the derived $\kappa$ value with its positivity lemma.
Claim. On the Recognition Science Einstein-field data package, the vacuum Einstein field equations hold: the cosmological constant vanishes ($\Lambda = 0$), the gravitational coupling equals $\kappa = 8\phi^5$, and $\kappa > 0$.
background
The FullEFE module derives the complete nonlinear, sourced Einstein field equations from the RS discrete ledger, conditional on Regge convergence axioms. The chain runs: J-cost minimization on the ledger, Regge action from J-cost on $\mathbb{Z}^3$, continuum limit to the Einstein-Hilbert action, Hilbert variation giving vacuum EFE, then matter coupling for the sourced equation $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$, with $\kappa=8\phi^5$ derived rather than fitted.
Vacuum well-posedness is the certificate that the vacuum sector is not a placeholder: $\Lambda=0$ and $\kappa$ is the positive RS-native coupling. Upstream, defect and recognition costs are instances of the J-cost $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness); the same $\phi$ fixed point that forces the eight-tick octave and $D=3$ also fixes $\kappa$ via $\phi^5$ (cf. RS units $G=\phi^5/\pi$). The data package rs_efe_data packages dimension, $\kappa$, and the Hilbert/matter closure hypotheses used by the rest of the module.
proof idea
Term-mode one-liner. The predicate vacuum_efe_holds on the RS data package asks only for the vacuum coupling facts. The proof ignores the dummy continuum/index argument and returns the pair ⟨rs_kappa_value, rs_kappa_pos⟩: the equality $\kappa=8\phi^5$ together with the positivity certificate $\kappa>0$. No Regge or Bianchi reasoning is invoked at this leaf; those live in the surrounding derivation-chain and sourced-EFE declarations.
why it matters
Closes the vacuum half of steps 5 and 8 in the module chain: Hilbert variation yields vacuum EFE, and $\kappa=8\phi^5$ is the derived coupling (from $\phi$, not fitted). It replaces an earlier True placeholder with actual content so the vacuum sector is well-posed. Downstream the module builds the sourced equation $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$ from matter J-cost above vacuum defect density; this theorem is the vacuum anchor those closures sit on. Framework landmarks: T5 J-uniqueness, T6 $\phi$ fixed point, and the RS-native constants ($G\sim\phi^5$). No used_by edges yet; it is a leaf certificate inside FullEFE rather than a widely re-used lemma. Open remainder of the chain is still the nonlinear Regge-convergence axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.