matter_coupling_closure
plain-language theorem explainer
Matter couples to curvature through a certified stress-energy source, closing the sourced Einstein equation step in the RS gravity chain. Anyone assembling the full GR certificate or the RS derivation chain cites this. The proof is a one-line term wrapper that re-exports the StressEnergyTensor certificate.
Claim. The matter-coupling closure holds: the stress-energy certificate is satisfied, so the continuum limit of the RS ledger with matter action yields the sourced Einstein field equations $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$.
background
Module FullEFE 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, then Hilbert variation for the vacuum EFE, and finally matter coupling for the sourced equation.
MatterCouplingClosure is an abbreviation for the stress-energy certificate from StressEnergyTensor. That certificate packages the claim that adding a matter action produces the right-hand side $T_{\mu\nu}$ with the RS-derived coupling. Spatial dimension is fixed at $D=3$ by the forcing chain (T8).
Upstream status: steps 5-6 of the module chain now rest on theorem-backed certificates (EinsteinHilbertAction, StressEnergyTensor) rather than placeholder Props. Conservation via Bianchi and the value $\kappa=8\varphi^5$ are handled elsewhere in the same module.
proof idea
One-line term wrapper. The goal type MatterCouplingClosure reduces by abbreviation to StressEnergyTensor.StressEnergyCert, and the proof is exactly the existing term StressEnergyTensor.stress_energy_cert. No local tactics or algebraic work.
why it matters
Fills step 6 of the FullEFE chain: adding matter action gives the sourced EFE $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$. Downstream, full_gr_certificate_v2 sets matter_coupling := matter_coupling_closure alongside hilbert_variation_closure, and rs_derivation_chain / full_gr_certificate consume the same closure in the assembled GR certificate.
Together with the Hilbert-variation closure, this replaces placeholder Props by IndisputableMonolith certificates for the vacuum and sourced sectors. The coupling constant itself is the RS-native $\kappa=8\varphi^5$ (from $\varphi$, not fitted), with $c=1$ and $G=\varphi^5/\pi$ in RS units. The remaining open piece of the chain is full nonlinear Regge convergence (axiomatized in NonlinearConvergence), not this matter step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.