expansion_convergence_ratio

The module gives a direct cubic-lattice proof that J-cost Regge calculus on $\mathbb{Z}^D$ converges to the continuum linearized vacuum Einstein equation, replacing the general Cheeger–Müller–Schrader axiom. The cost is fixed: $J(e^\varepsilon)=\cosh\varepsilon-1$, with Taylor series $\varepsilon^2/2+\varepsilon^4/24+\varepsilon^6/720+\cdots$.

Tier 1 of the strategy bounds the action gap by the quartic remainder of that expansion. A standard comparison is that the series converges faster than a geometric series whose common ratio is $|\varepsilon|^2/30$. The present inequality simply records that this ratio is strictly contractive whenever $|\varepsilon|<1$, so the geometric majorant is summable.

Upstream continuum infrastructure (lattice Laplacian, continuum second-order limit) is used later in the module; this lemma is pure real analysis and does not invoke those objects.

From $|\varepsilon|<1$ obtain $\varepsilon^2<1$ by nlinarith using sq_abs and non-negativity of absolute value. Then linarith divides by the positive constant 30 and concludes $\varepsilon^2/30<1$. No external lemmas are required.

The bound underwrites the Tier-1 action estimate $|S_{J\mathrm{-cost}}-S_{\mathrm{quadratic}}|\le C,\varepsilon_{\max}^4$ that opens the cubic Regge convergence argument. Rapid geometric domination of the cosh remainder is what lets the RS-specific proof avoid the full CMS machinery (arbitrary mesh quality, Cayley–Menger determinants). Combined with the later linearization of the Euler–Lagrange equation to the lattice Laplacian and the continuum limit $\Delta_{\mathrm{lat}}/a^2\to\nabla^2$, it closes the chain from discrete J-cost variational principle to linearized vacuum EFE in harmonic gauge. No downstream consumers are recorded in the graph yet; the lemma sits as local scaffolding for the relative-convergence and total-action statements in the same file.