relative_convergence_rate
plain-language theorem explainer
When bond strains scale as ε = O(a) on a cubic lattice of spacing a, the ratio of the quartic J-cost remainder to the quadratic action equals (Ma)²/10. Anyone bounding relative Regge-to-Einstein–Hilbert error cites this identity. The proof is a two-line field simplification after ruling out a zero denominator.
Claim. For real $M,a$ with $0 < a < 1$ and $M > 0$, $$\frac{(Ma)^4/20}{(Ma)^2/2} = \frac{(Ma)^2}{10}.$$ Thus if bond perturbations satisfy $|\varepsilon| \le Ma$, the relative action error bound $|S_{J}-S_{\mathrm{quad}}|/|S_{\mathrm{quad}}|$ is at most $(Ma)^2/10$, hence $O(a^2)$.
background
The module gives a direct cubic-lattice proof that J-cost Regge calculus on $\mathbb{Z}^D$ converges to the continuum variational principle, replacing the general Cheeger–Müller–Schrader axiom. The cost is fixed: $J(e^\varepsilon)=\cosh\varepsilon-1$, with Taylor expansion $\varepsilon^2/2+\varepsilon^4/24+\cdots$.
Tier 1 of the strategy bounds the absolute action gap by a multiple of $\varepsilon_{\max}^4$ (from the quartic remainder of $J$). For a smooth field on spacing $a$, bond strains scale as $\varepsilon=O(a)$, written $\varepsilon\le Ma$. The absolute bound is then $(Ma)^4/20$ per bond against quadratic scale $(Ma)^2/2$.
This declaration is the pure arithmetic step that turns those two monomials into a relative $O(a^2)$ rate. Downstream lattice–manifold correspondence packages the same identity as the relative action deviation.
proof idea
Term-mode proof. From $M>0$ and $a>0$, mul_pos gives $Ma\neq 0$, so the denominator $(Ma)^2/2$ is nonzero. Then field_simp clears the nested divisions and ring reduces both sides to the common monomial $(Ma)^2/10$. No analytic estimates enter; the $a<1$ hypothesis is unused in the algebra (it is carried for call-site uniformity with the $\varepsilon$-bound lemmas).
why it matters
Closes Tier 1 of the cubic Regge program: absolute $O(\varepsilon^4)$ control upgrades to relative $O(a^2)$ when $\varepsilon=O(a)$. The unified lattice–manifold correspondence cites it verbatim as relativeActionDeviation, and the per-bond deviation lemma records that this ratio is the source of the global $O(a^2)$ rate.
It feeds the zero-axiom certificate cubic_regge_convergence_cert, which assembles action quadratic approximation, EL linearization to the lattice Laplacian, and continuum limit into a single proved package. In the broader RS gravity stack this is the concrete rate that lets J-cost dynamics on $\mathbb{Z}^D$ approach linearized Einstein–Hilbert without importing CMS compactness machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.