full_gr_certificate_v2
plain-language theorem explainer
Packages the full Recognition-Science-to-general-relativity certificate: Einstein coupling equals 8 phi^5, is positive and nonzero, Hilbert and matter-coupling closures hold, flat Regge/Bianchi/Riemann/Einstein identities hold, and linearized Regge convergence is recorded. Gravity auditors cite it as the single structure that assembles the discrete-ledger derivation of the Einstein field equations. The proof is a pure structure inhabitant that wires already-proved component certificates.
Claim. There exists a complete RS-to-GR certificate asserting: the Einstein coupling satisfies $\kappa_{\mathrm{RS}}=8\phi^5$ with $\kappa_{\mathrm{RS}}>0$ (hence nonzero); the Hilbert-variation and matter-coupling closures hold; the Regge action vanishes on every hinge list with zero deficit angles; the discrete Bianchi identity holds for all-zero deficits; the Riemann tensor is antisymmetric in its last pair and vanishes in the flat case; the Einstein tensor vanishes when flat; and the linearized Regge-to-continuum convergence estimate holds.
background
The module derives the full nonlinear, sourced Einstein field equations from the RS discrete ledger, conditional on Regge continuum-limit axioms. The chain runs: J-cost minimization on the ledger, quadratic limit yielding the Regge action, continuum convergence 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 ensuring $\nabla^\mu T_{\mu\nu}=0$, and $\kappa=8\phi^5$ derived rather than fitted.
FullGRCertificateV2 is the structure that packages the unconditional pieces of that chain: closed-form $\kappa$, positivity, Hilbert and stress-energy certificates, flat Regge vanishing, flat discrete Bianchi, Riemann/Einstein flat identities, and the linearized convergence estimate. Upstream, kappa_derived states that in the gravitational sector the lattice field encodes the metric perturbation and the sourced continuum limit is $\nabla^2 h=-2\kappa T$ with $\kappa=8\phi^5$; flat_bianchi records that zero deficits satisfy the linearized Bianchi identity by induction on the deficit list.
Hilbert and matter closures are thin wrappers around EinsteinHilbertAction.hilbert_variation_cert and StressEnergyTensor.stress_energy_cert. The full nonlinear Regge convergence step remains axiomatized outside this certificate.
proof idea
Term-mode structure construction: each field of FullGRCertificateV2 is filled by an existing lemma. Coupling identity and positivity come from rs_kappa_value / rs_kappa_pos (equivalently the CubicReggeProof closed forms); nonzeroness is ne_of_gt on positivity. Hilbert and matter fields are the local closures hilbert_variation_closure and matter_coupling_closure. Flat Regge vanishing is regge_action_flat; flat Bianchi is flat_bianchi. Riemann antisymmetry and flat vanishing, Einstein-flat vanishing, and linearized Regge convergence are cited directly from RiemannTensor, RicciTensor, and ReggeConvergence. No new algebra is performed.
why it matters
This is the terminal assembly point of the Gravity.FullEFE module: one named certificate that a referee can point to for "RS derives the full EFE, conditional only on Regge continuum convergence." It locks step 8 of the module chain ($\kappa=8\phi^5$, matching the RS-native $G=\phi^5/\pi$ sector up to conventional factors) and step 7 (discrete Bianchi / conservation). Steps 5-6 are no longer placeholder Props; they sit behind theorem-backed Hilbert and stress-energy certificates.
In the broader forcing picture it sits downstream of the J-cost / Regge calculus development rather than T0-T8 themselves, but it is where the discrete ledger meets classical GR. No downstream dependents are recorded yet; the structure is the export surface. The remaining open formalization gap is the full nonlinear CMS-style Regge convergence axiom in NonlinearConvergence, which this certificate deliberately does not claim to discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.