ProvedConvergenceChain
plain-language theorem explainer
Packages eight statements that take the RS J-cost action on a cubic lattice to the linearized Einstein equation: quadratic J-expansion, neighbor-cost bound, EL equals minus lattice Laplacian, flat baseline, sinh'(0)=1, continuum second-difference limit, kappa=8 phi^5, and vanishing cubic deficit. Gravity continuum-limit arguments cite this bundle. It is a pure structure type; the inhabitant is assembled from named lemmas.
Claim. A proved convergence chain is a record of eight claims: (1) for $|\varepsilon|<1$, $|J_{\log}\varepsilon-\varepsilon^2/2|\le|\varepsilon|^4/20$; (2) if all nearest-neighbor log-ratio jumps of a lattice field $f$ on $\mathbb{Z}^D$ are $<1$, the neighbor $J$-cost differs from $\sum_k(\varepsilon_{k,+}^2+\varepsilon_{k,-}^2)/2$ by at most the sum of fourth-power remainders; (3) the discrete linearized EL operator equals $-\Delta_{\mathrm{lat}}f$; (4) every constant field has vanishing EL; (5) $\frac{d}{dx}\sinh(0)=1$; (6) for $a\ne0$ and $f\in C^4$, the centered second difference over $a^2$ approximates $f''(x)$ with $O(a^2)$ error; (7) $\kappa_{\mathrm{RS}}=8\phi^5$; (8) $2\pi-4(\pi/2)=0$ (cubic lattice is flat).
background
The module replaces the general Cheeger–Müller–Schrader continuum axiom by a direct argument specialized to Recognition Science: J-cost interactions on the cubic lattice $\mathbb{Z}^D$. The general CMS theorem handles arbitrary simplicial meshes; here the lattice is cubic, the cost is fixed as $J(e^\varepsilon)=\cosh\varepsilon-1$, and the EL equation linearizes through $\sinh$.
A lattice field is a map $f:\mathbb{Z}^D\to\mathbb{R}$ (log-ratio perturbations at sites). Nearest-neighbor shifts along axis $k$ define the lattice Laplacian $\Delta_{\mathrm{lat}}f(x)=\sum_k\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)$ and the neighbor cost $\sum_k\bigl(J_{\log}(f(x+e_k)-f(x))+J_{\log}(f(x-e_k)-f(x))\bigr)$. In the small-jump regime the quadratic part of $J_{\log}$ turns that cost into Laplacian structure.
The three tiers in the module doc are action convergence ($|S_{J}-S_{\mathrm{quad}}|\le C\varepsilon_{\max}^4$), EL linearization to $\Delta_{\mathrm{lat}}$ via $\sinh'(0)=1$, and $\Delta_{\mathrm{lat}}/a^2\to\nabla^2$ at $O(a^2)$. Combined, the discrete variational principle converges to linearized EFE.
proof idea
No proof body: this is a structure whose fields are the eight propositions above. It is the type of a complete chain, not a derivation.
The downstream inhabitant proved_convergence_chain fills each field by a named lemma: step 1 by the quartic Taylor bound on $J_{\log}$; step 2 by the neighbor-cost-to-Laplacian comparison under the unit-jump hypothesis; step 3 by the identity equating linearized EL to $-\Delta_{\mathrm{lat}}$; step 4 by the constant-field EL vanishing lemma; step 5 by $\sinh'(0)=1$; with continuum second-order limit, derived $\kappa_{\mathrm{RS}}=8\phi^5$, and the elementary cubic deficit identity completing the record. Discharge is assembly, not a new argument.
why it matters
This record is the RS-native substitute for the CMS convergence axiom in the gravity stack: it states exactly which eight facts turn J-cost on $\mathbb{Z}^D$ into linearized Einstein dynamics at $O(a^2)$. The sole direct consumer is the theorem that builds an instance of the structure from the sibling lemmas (quadratic $J$ approx, neighbor-cost structure, EL–Laplacian identity, flat EL, $\sinh$ linearization, continuum limit, derived coupling, cubic flatness).
Framework landmarks touched: T5 J-uniqueness supplies $J_{\log}$ and its Taylor spine $\varepsilon^2/2+O(\varepsilon^4)$; T8 forces $D=3$ as the spatial dimension of the lattice; the coupling field records $\kappa_{\mathrm{RS}}=8\phi^5$ from the zero-parameter gravity side (consistent with $G\sim\phi^5$ in RS units). Closing this chain is what lets cubic Regge/J-cost arguments claim continuum GR without an external convergence axiom. Open residual is only whether every named filler lemma is free of sorry in the current build; the structure itself merely names the obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.