MatterCouplingClosure
plain-language theorem explainer
Aliases the stress-energy certificate that packages vacuum specialization of the sourced EFE, nonvanishing of the RS coupling κ = 8φ⁵, and the conservation implication for nonzero κ. Gravity authors cite it when wiring matter into the full RS→EFE chain. The body is a pure definitional abbreviation of StressEnergyCert.
Claim. Matter-coupling closure is defined to be the stress-energy certificate: a package asserting (i) that the sourced Einstein equation with vanishing stress-energy reduces to the vacuum equation, (ii) that the RS coupling $\kappa = 8\varphi^5$ is nonzero, and (iii) that any nonzero coupling implies the conservation law used for $\nabla^\mu T_{\mu\nu}=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 from J-cost minimization on the lattice through Regge action, continuum limit to Einstein-Hilbert, Hilbert variation (vacuum EFE), then matter coupling to the sourced form $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$, with Bianchi giving conservation and $\kappa=8\varphi^5$ derived rather than fitted.
Steps 5–6 are backed by theorem-carrying certificates in EinsteinHilbertAction and StressEnergyTensor rather than placeholder Props. The upstream structure StressEnergyCert records three facts: vacuum is the zero-source special case of the sourced EFE; $\kappa=8\varphi^5\neq 0$ (proved from $\varphi>0$); and nonzero $\kappa$ yields the conservation implication used for $\nabla^\mu T_{\mu\nu}=0$.
proof idea
Definitional one-liner: the abbreviation is identical to StressEnergyTensor.StressEnergyCert. No tactics, no lemmas applied at this site. The mathematical content lives entirely in the upstream certificate structure and its inhabitant stress_energy_cert.
why it matters
Closes step 6 of the module chain (adding matter action yields the sourced EFE) by naming the stress-energy certificate as the matter-coupling gate. Downstream, FullDerivationChain records it beside Hilbert variation; FullGRCertificate and FullGRCertificateV2 consume the same package for conservation and $\kappa\neq 0$; the theorem matter_coupling_closure supplies the concrete inhabitant. In RS units $\kappa=8\varphi^5$ ties the Einstein coupling to the golden-ratio ladder rather than a free fit, consistent with the primer constants ($G=\varphi^5/\pi$ scale). It does not discharge Regge convergence (still axiomatized in the full nonlinear regime).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.