rs_derivation_chain
plain-language theorem explainer
Packages the eight-step RS lattice-to-EFE derivation as one structure value with RS-native certificates. Gravity and continuum-limit workers cite it as the single handle for J-cost quadraticity through kappa = 8 phi^5. The body is a field-by-field wiring of proved bounds, theorem-backed closures, and the remaining Regge-convergence axiom.
Claim. The RS derivation chain is the record whose eight fields assert: (1) $|\cosh\varepsilon-1-\varepsilon^2/2|\le|\varepsilon|^4/20$ for $|\varepsilon|<1$; (2) vanishing Regge action on deficit-free hinges; (3) the Regge-to-Einstein-Hilbert continuum axiom; (4) linearized variational convergence; (5) Hilbert-variation closure; (6) matter-coupling closure; (7) discrete Bianchi conservation; (8) $\kappa=8\phi^5$.
background
Module Gravity.FullEFE derives the complete nonlinear, sourced Einstein field equations from the RS discrete ledger, conditional on Regge continuum axioms. The ledger evolves by J-cost minimization; on a spatial lattice the small-defect expansion of that cost is quadratic and matches the Regge action (deficit angles on hinges). Continuum passage of the Regge action yields the Einstein-Hilbert action; its variation gives vacuum EFE, and adding a matter action yields the sourced equation $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$.
FullDerivationChain is the structure that records one proposition (or certificate type) per step, annotated PROVED or AXIOM in the module status note. Steps 1-2 are unconditional; step 3 is the external nonlinear Regge-to-EH axiom; step 4 is the linearized second-order estimate; steps 5-6 are theorem-backed Hilbert and stress-energy closures; steps 7-8 (Bianchi conservation and $\kappa=8\phi^5$) are proved. Upstream cost infrastructure (observer J-cost, multiplicative recognizer cost, rung-coarsen cost) supplies the ledger side of step 1.
proof idea
Definitional structure instance, not a tactic proof. Each field is filled by a concrete proposition or named certificate: step 1 is the explicit quartic remainder bound for $\cosh\varepsilon-1$ versus $\varepsilon^2/2$; step 2 is the implication that zero deficits force zero Regge action; step 3 points at regge_to_eh_convergence_axiom; step 4 at ReggeConvergence.linearized_convergence; steps 5-6 at the in-module Hilbert-variation and matter-coupling closures; step 7 at discrete_conservation; step 8 at the equality rs_kappa = 8 * phi^5. No further reduction is performed here.
why it matters
This is the RS-native packaging of the full gravity derivation chain in the module that claims the complete EFE from the ledger. It sits at the end of the forcing story for gravity: J-uniqueness (T5) and the Recognition Composition Law fix the cost whose quadratic defect limit becomes Regge; continuum and variational limits recover Hilbert variation; matter coupling and Bianchi close the sourced, conserved system; and $\kappa=8\phi^5$ (with $G=\phi^5/\pi$ in RS units) is derived rather than fitted. No downstream Lean users are recorded yet; the object is the citation handle for the conditional claim that RS derives the full EFE once nonlinear Regge convergence is discharged. The open formal gap remains step 3 in the full nonlinear regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.