action_per_bond
plain-language theorem explainer
For each bond with log-ratio perturbation ε satisfying |ε|<1, the J-cost cosh(ε)−1 differs from the quadratic ε²/2 by at most |ε|⁴/20. Continuum-limit and Regge-gravity arguments cite this bond-level remainder when controlling the lattice action. The proof is a one-line term application of the grounded quadratic approximation for J in log coordinates.
Claim. If $|\varepsilon|<1$, then $\bigl|(\cosh\varepsilon-1)-\varepsilon^2/2\bigr|\le|\varepsilon|^4/20$.
background
Recognition Science forces a unique cost $J$ on positive ratios (T5). In log coordinates one writes $J_{\log}(t)=\cosh t-1$, a convex bowl minimized at $t=0$. On the cubic lattice $\mathbb{Z}^D$ each nearest-neighbor bond carries a small log-ratio $\varepsilon$, and the discrete action is the sum of $J_{\log}$ over bonds.
This module replaces the general Cheeger–Müller–Schrader continuum-limit axiom by a direct RS-specific argument: the lattice is cubic, the cost is exactly $\cosh-1$ with fixed Taylor series $\varepsilon^2/2+\varepsilon^4/24+\cdots$, and the Euler–Lagrange linearization of $\sinh$ is elementary. Tier 1 of the strategy is action convergence, which starts from a uniform per-bond quadratic error bound under $|\varepsilon|<1$.
The upstream quadratic-approximation theorem for $J_{\log}$ supplies that bound. A related continuum-limit result then lifts the quadratic regime to lattice-Laplacian structure on neighbor costs.
proof idea
One-line term proof: apply the grounded quadratic approximation of $J_{\log}$ at the given $\varepsilon$ under the hypothesis $|\varepsilon|<1$. No further algebra is done here; the declaration is a named re-export so the gravity/Regge module can cite a bond-level action error without reaching into Foundation.
why it matters
This is the bond-level remainder that opens Tier 1 (action convergence) of the cubic Regge direct proof. Summing over bonds yields the total comparison $|S_{J\mathrm{cost}}-S_{\mathrm{quadratic}}|\le C,\varepsilon_{\max}^4$, which is the first rung of the path from discrete J-cost variational principles to linearized continuum gravity.
Downstream it is consumed by the unified lattice–manifold correspondence certificate and its main theorem: for every weak-field input and every lattice refinement, the certificate bundles refinement density, positive edge lengths, and continuum matching with zero sorry and no new axioms. In the forcing chain, $J$ is the T5 unique cost and $D=3$ is forced by T8; the present bound is the analytic step that turns that cost into a controlled Regge-to-Einstein–Hilbert limit on $\mathbb{Z}^D$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.