sourced_efe_statement
plain-language theorem explainer
Packages the RS-sourced Einstein field equation claim as the proposition that the Einstein coupling κ on full nonlinear EFE data is positive and exactly 8φ⁵. Gravity-chain authors cite it as the target Prop for the matter-coupled continuum limit. Pure definition: a two-conjunct predicate on FullEFEData, no proof obligations.
Claim. For full nonlinear Einstein-field-equation data $d$ (recording spacetime dimension $4$, Einstein coupling $\kappa>0$, and a cosmological constant), the sourced-EFE statement is the proposition $0 < \kappa \wedge \kappa = 8\varphi^{5}$.
background
The module derives the complete nonlinear, sourced Einstein field equations from the RS discrete ledger, conditional on Regge-convergence axioms. The chain runs from J-cost minimization on the ledger, through the Regge action and its continuum limit to the Einstein-Hilbert action, Hilbert variation (vacuum EFE), and finally matter coupling.
FullEFEData is the structure carrying that continuum data: dimension fixed at 4, a real coupling $\kappa$ with a positivity field, and a cosmological constant. Unlike linearized scalar placeholders, it records the tensor setting explicitly.
In standard GR one has $\kappa = 8\pi G$. RS fixes $G = \varphi^{5}/\pi$ in native units, so $\kappa = 8\varphi^{5}$ is forced rather than fitted. The matter side is the non-gravitational J-cost (defect density above vacuum); the stress-energy tensor is the metric variation of that action, carried to the discrete setting by the convergence axiom.
proof idea
Definition, not a theorem. The body is the bare conjunction $0 < d.\mathrm{kappa} \wedge d.\mathrm{kappa} = 8\varphi^{5}$. No tactics, no lemmas: it simply names that two-part predicate so downstream theorems can target it.
why it matters
Closes steps 6 and 8 of the module chain: adding matter yields the sourced EFE, and $\kappa = 8\varphi^{5}$ is derived from $\varphi$, not fitted. The immediate consumer is rs_sourced_efe, which discharges the predicate on the RS-specific data bundle by pairing the positivity and exact-value lemmas for $\kappa$.
That places the declaration on the path from the vacuum Hilbert variation through matter coupling to energy-momentum conservation ($\nabla^{\mu}T_{\mu\nu}=0$) via the Bianchi identity. Framework landmarks: $\varphi$ from T6, $D=3$ spatial (hence 4D spacetime) from T8, and $G=\varphi^{5}/\pi$ in RS-native units. The remaining open hinge is full nonlinear Regge convergence, still axiomatized rather than formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.