rs_efe_data
plain-language theorem explainer
Packages the Recognition Science Einstein-field data: spacetime dimension 4, gravitational coupling κ = 8φ⁵, and vanishing cosmological constant. Anyone citing the RS vacuum or sourced EFE, conservation, or the full GR certificate pulls this record. The body is a structure instance: dimension equality by reflexivity, κ and positivity from the Regge coupling, Λ set to zero.
Claim. The Recognition Science Einstein-field data is the 4-dimensional package with coupling $\kappa = 8\phi^5 > 0$ and cosmological constant $\Lambda = 0$.
background
Module FullEFE derives the complete nonlinear, sourced Einstein equations from the RS discrete ledger, conditional on Regge continuum convergence. The chain runs J-cost minimization on the lattice to the Regge action, then (under convergence) to the Einstein-Hilbert action, Hilbert variation, matter coupling, and Bianchi conservation, with $\kappa = 8\phi^5$ fixed by $\phi$ rather than fit.
FullEFEData is the explicit nonlinear 4D data record: a natural-number dimension forced equal to 4, a real coupling $\kappa$ with $\kappa > 0$, and a real cosmological constant. Unlike linearized scalar placeholders, it keeps the tensor-level bookkeeping.
Upstream, rs_kappa is defined as $8\phi^5$ and inherits from the defect-to-metric map so that $S_{\mathrm{Regge}}\to (1/(2\kappa))\int R\sqrt{g},d^4x$ in the continuum. Positivity is immediate from $\phi>0$. In RS units this matches the classical $8\pi G$ with $G=\phi^5/\pi$.
proof idea
Definitional structure instance, not a tactic proof. Set dimension := 4 and discharge dim_eq by rfl. Bind kappa to the upstream Regge coupling rs_kappa ($8\phi^5$) and kappa_pos to rs_kappa_pos (product of positive factors). Set cosmological_constant := 0. No further lemmas.
why it matters
This is the single RS parameter pack that every FullEFE theorem consumes. Downstream: vacuum EFE (rs_vacuum_efe: when $\Lambda=0$, $\kappa=8\phi^5>0$), sourced EFE, conservation (rs_conservation via $\kappa\neq 0$), dimension and $\kappa$ extractors, and the master full_gr_certificate. Dark-energy extensions reuse it as the baseline before adding $\Lambda$.
It closes chain step 8 in the module doc ($\kappa=8\phi^5$ derived from $\phi$). Framework landmarks: $D=3$ spatial plus time gives the forced dimension 4; $G=\phi^5/\pi$ yields $\kappa=8\pi G=8\phi^5$. The open gate remains NonlinearConvergence (Regge$\to$EH in the full nonlinear regime), not this data record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.