proved_convergence_chain
plain-language theorem explainer
A single certificate packages the full eight-step derivation from J-cost gravity on the cubic lattice to the linearized Einstein equations, with every step a proved theorem and no axioms. It covers quadratic cost approximation, neighbor-cost to lattice Laplacian, linearized EL identity, flat solutions, sinh linearization, continuum Laplacian limit, closed-form RS coupling, and vanishing cubic flat deficit. Anyone citing the RS weak-field continuum limit would point here. The proof is a structure inhabitant that wires eight existing lemmas.
Claim. There is a fully proved convergence chain from Recognition Science lattice gravity to the linearized Einstein equations: for $|\varepsilon|<1$, $|J_{\log}(\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/20$; nearest-neighbor J-cost equals a sum of squared bond differences up to $O(\varepsilon^4)$; the linearized Euler-Lagrange operator equals the negative lattice Laplacian; constant fields solve the EL equation; $\sinh'(0)=1$; the lattice Laplacian converges to $\nabla^2$ with error $O(a^2)$; the RS gravitational coupling has a closed form; and the cubic lattice has vanishing flat deficit.
background
The module replaces the general Cheeger-Muller-Schrader continuum-limit axiom by a direct argument specialized to Recognition Science: J-cost interactions on the cubic lattice $\mathbb{Z}^D$. The cost is known explicitly, $J(e^\varepsilon)=\cosh\varepsilon-1$, so its Taylor series $\varepsilon^2/2+\varepsilon^4/24+\cdots$ is fixed, and the Euler-Lagrange equation involves $\sinh$, whose linearization at zero is elementary.
Upstream, the quadratic approximation of $J_{\log}$ states that for $|\varepsilon|<1$, $|J_{\log}\varepsilon-\varepsilon^2/2|\le|\varepsilon|^4/20$. The neighbor-cost theorem then shows that, when all nearest-neighbor field jumps are smaller than 1, the local J-cost reduces to a sum of squared differences (the discrete Dirichlet energy). Continuum-limit second order supplies the classical finite-difference identity: $(f(x+a)+f(x-a)-2f(x))/a^2=f''(x)+O(a^2)$ for $C^4$ fields.
The certificate structure records eight such links, from quadratic cost through EL linearization and continuum Laplacian to the closed-form RS coupling and the geometric fact that a flat cubic lattice has zero deficit.
proof idea
Term-mode structure inhabitant: each field of the certificate is filled by an existing lemma (or a thin lambda around one).
Step 1 is the quadratic bound on $J_{\log}$. Step 2 applies the neighbor-cost-to-Laplacian theorem under the small-jump hypothesis. Step 3 is the identity that the linearized EL operator equals the negative lattice Laplacian. Step 4 records that constant (flat) fields satisfy the EL equation. Step 5 is $\sinh'(0)=1$. Step 6 unpacks continuum-limit second order and returns the $O(a^2)$ error witness. Step 7 plugs in the closed-form RS gravitational coupling. Step 8 is vanishing deficit on the flat cubic lattice.
No new analysis is performed here; the certificate only assembles the chain.
why it matters
This certificate is the master object that retires three axioms from the nonlinear-convergence module: action convergence (Regge to Einstein-Hilbert), Ricci/EL-to-Laplacian convergence, and Riemann/deficit-angle geometry. The module doc states the combined claim: the J-cost variational principle on $\mathbb{Z}^D$ converges to the continuum variational principle (linearized EFE) at $O(a^2)$.
It sits in the gravity domain of the RS forcing picture, where the unique cost $J(x)=(x+x^{-1})/2-1$ (T5) and the discrete ledger structure force a lattice whose weak-field continuum limit must recover Einstein gravity without free parameters. The regime covered is all weak-field physics (solar system, galaxies, gravitational waves, CMB perturbations). What remains open is the strong-field regime $|h|\sim O(1)$ (black-hole interiors, cosmological singularities), where nonlinear matching of cosh coefficients to Regge coefficients on the cubic lattice is structural but not yet fully formalized. No downstream dependents are recorded yet; the certificate is the terminal proved object of this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.