coshRemainder_zero
plain-language theorem explainer
The result shows that the nonlinear correction term in the J-cost action vanishes exactly at the flat vacuum. Researchers extending the Regge-J-cost bridge to strong fields cite it as the base case confirming the quadratic approximation holds with zero error on flat space. The proof is a direct one-line wrapper that unfolds the definition and simplifies.
Claim. Let $r(x) := 2^{-1}x^{2} - 1 + 2^{-1}(e^{x} + e^{-x})$. Then $r(0) = 0$.
background
The NonlinearBridge module constructs the exact J-cost action as the sum over edges of weights times (cosh(ε_i - ε_j) - 1). This expression equals the quadratic Laplacian action plus a quartic remainder at all orders, addressing the weak-field limitation noted in Beltracchi §6. The remainder function is defined directly as cosh(x) - 1 - x²/2 and quantifies the nonlinear correction that is O(x⁴) for small deviations.
proof idea
One-line wrapper that unfolds the definition of coshRemainder and applies simp to evaluate the expression at zero.
why it matters
This base case anchors the exact decomposition exactJCostAction = laplacian_action + quartic_remainder used throughout the nonlinear bridge. It confirms the remainder vanishes on the flat vacuum, consistent with J-uniqueness (T5) forcing the cosh form. The result supports the claim that the J-cost side of the identification requires no weak-field assumption, while the Regge side remains a separate hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.