FullDerivationChain
plain-language theorem explainer
Bundles the eight-step path from the Recognition Science ledger (J-cost on the discrete lattice) to the full nonlinear, sourced Einstein field equations. Gravity and continuum-limit workers cite it as the single certificate object that records which links are proved, which are linearized, and which remain external. It is a pure structure of propositions and named closures, not a proved theorem.
Claim. A derivation-chain certificate is a record of eight propositions: (1) $J$-cost is quadratic to fourth order near the identity; (2) vanishing deficit angles imply vanishing Regge action; (3) Regge action converges to the Einstein--Hilbert action; (4) the linearized variational limit holds; (5) a Hilbert-variation certificate ($\delta S_{\mathrm{EH}}=0$ yields vacuum EFE); (6) a stress-energy certificate (matter coupling yields $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$); (7) Bianchi identity implies $\nabla^\mu T_{\mu\nu}=0$; (8) $\kappa=8\varphi^5$.
background
The FullEFE module aims to derive the complete nonlinear, sourced Einstein field equations from the RS discrete ledger, conditional on Regge-convergence axioms. The module doc lays out an eight-step chain: ledger evolution by $J$-cost minimization; $J$-cost on $\mathbb{Z}^3$ producing the Regge action; continuum convergence of Regge to Einstein--Hilbert; passage of the variational principle to the limit; Hilbert variation giving vacuum EFE; matter coupling giving the sourced EFE; Bianchi identity giving stress-energy conservation; and derivation of $\kappa=8\varphi^5$ from the golden ratio rather than a fit.
$J$-cost is the recognition cost of an event (ObserverForcing: cost of a recognition event is its $J$-cost; related multiplicative and rung-coarsened costs appear upstream). In RS, $J(x)=(x+x^{-1})/2-1$ is the unique cost forced by the Recognition Composition Law (forcing chain T5). HilbertVariationClosure is an abbreviation for the Hilbert-variation certificate from EinsteinHilbertAction; MatterCouplingClosure abbreviates the stress-energy certificate from StressEnergyTensor.
Steps 1--2 are unconditional in ContinuumLimit and ReggeCalculus. Step 3 is axiomatized in the full nonlinear regime. Step 4 carries an explicit second-order linearized error estimate. Steps 5--6 now hold theorem-backed certificates rather than bare Props. Steps 7--8 are proved.
proof idea
No proof body: this is a structure declaration. Each field is a Prop (or a named certificate type) that a concrete instance must supply. Fields 5 and 6 are typed as HilbertVariationClosure and MatterCouplingClosure, i.e. the existing EinsteinHilbertAction and StressEnergyTensor certificates, so instantiation reuses those modules rather than re-proving variation and coupling. Field 4 is typed as the linearized-convergence flag from ReggeConvergence. The remaining fields are open Props whose mathematical content is fixed by the inline comments and by the module chain description. Downstream, rs_derivation_chain fills every field with an RS-specific statement (e.g. the cosh fourth-order bound for step 1, and vanishing Regge action at zero deficit for step 2).
why it matters
This is the bookkeeping spine of the FullEFE program: one object that states what "RS derives the full EFE" means as a finite list of obligations. The sole direct consumer is rs_derivation_chain, which instantiates the chain with RS-native values and thereby turns the abstract checklist into a concrete RS claim.
In the broader framework it sits at the gravity end of the forcing chain: T5 uniqueness of $J$, the eight-tick and $D=3$ landmarks (T7--T8) that fix the lattice, and the RS-native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) that make $\kappa=8\varphi^5$ a derived rather than fitted coupling. The open hinge remains step 3: full nonlinear Regge-to-EH convergence is an established analytic result not yet formalized in any proof assistant; the module treats it as an external axiom while the linearized variational limit (step 4) is already certificate-backed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.