FullGRCertificate
plain-language theorem explainer
Packages every claim needed to certify that Recognition Science derives the full sourced Einstein field equations in 4D. A gravity theorist cites it as the single interface for the RS→GR chain: dimension and κ=8φ⁵, Hilbert variation, matter coupling, flat Regge and Bianchi checks, and linearized convergence. As a structure it is pure data; inhabitants are assembled by filling each field from upstream certificates.
Claim. A full GR certificate is a record consisting of: 4D Einstein data $(D,\kappa,\Lambda)$ with $D=4$ and $\kappa=8\varphi^5>0$; a Hilbert-variation certificate (vacuum EFE from $\delta S_{\mathrm{EH}}=0$); a stress-energy/matter-coupling certificate (sourced EFE and $\nabla^\mu T_{\mu\nu}=0$); the statements that vanishing hinge deficits imply zero Regge action and that vanishing deficit lists satisfy the linearized Bianchi identity; a linearized Regge-convergence flag; and the elementary identity $(a/2)^2=a^2/4$ for $0<a<1$.
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 ledger → Regge action on $\mathbb{Z}^3$ → continuum limit to the Einstein–Hilbert action → Hilbert variation giving vacuum EFE → matter coupling giving $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$ → Bianchi implying conservation, with $\kappa=8\varphi^5$ fixed (not fitted).
FullEFEData records the nonlinear 4D package $(D,\kappa,\Lambda)$ with $D=4$ and $\kappa>0$. HilbertVariationClosure is the Einstein–Hilbert variation certificate; MatterCouplingClosure is the stress-energy certificate. Upstream, kappa_derived states $\kappa_{\mathrm{RS}}=8\varphi^5$ and kappa_positive that it is positive; linearized_bianchi is the Prop that a list of deficit angles sums to zero.
Steps 1–2 and 7–8 are unconditional in-tree; step 3 (full nonlinear Regge→EH) remains external (CMS-style curvature-measure bounds); steps 4–6 are certificate-backed via linearized convergence, Hilbert variation, and stress-energy modules.
proof idea
No proof body: this is a structure definition. Each field is a typed obligation. Dimension and $\kappa$ facts point at FullEFEData plus the closed-form theorems kappa_derived / kappa_positive. Hilbert and matter fields are abbreviations for HilbertVariationCert and StressEnergyCert. Flatness fields are universal statements over hinge lists and deficit lists using deficit_angle, regge_action, and linearized_bianchi. Linearized convergence is a boolean/Prop flag from ReggeConvergence; the last field is a trivial algebraic identity used as a second-order error marker. An inhabitant is built by supplying proofs or certificates for every field (see full_gr_certificate).
why it matters
This is the top-level packaging of the RS→full-GR claim inside Gravity.FullEFE. Downstream, full_gr_certificate constructs a concrete inhabitant from rs_efe_data, rs_efe_dimension, rs_efe_kappa, and the conservation/positivity lemmas, so any audit of "does RS derive GR?" routes through this type.
It sits at the end of the module chain (steps 1–8): J-cost → Regge → continuum → variation → sourced EFE → Bianchi → derived $\kappa=8\varphi^5$. Framework landmarks: $\varphi$ from the forcing chain (T6), $D=3$ spatial plus time giving 4D spacetime data, and $G\sim\varphi^5$ in RS-native units matching $\kappa=8\varphi^5$.
Open remainder is explicit in the doc-comment: full nonlinear Regge→EH convergence is still axiomatized (CMS supplies weaker $\eta^{1/2}$ bounds; $O(a^2)$ is a stronger special hypothesis). When Mathlib gains Riemannian geometry and Regge calculus, those external steps can be discharged without changing this certificate interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.