coshRemainder
plain-language theorem explainer
coshRemainder isolates the order-x^4 and higher terms in the expansion of cosh x beyond the quadratic Taylor piece. Researchers deriving the exact J-cost action on simplicial complexes cite it to separate the weak-field Laplacian from strong-field corrections. The definition is a direct algebraic subtraction of the standard real hyperbolic cosine minus one minus x squared over two.
Claim. The nonlinear remainder function is defined by $r(x) := {cosh} x - 1 - x^2/2$.
background
In the Nonlinear J-Cost / Regge Bridge module the exact coupling between two simplices with log-potentials ε_i, ε_j is given by J(exp(ε_i − ε_j)) = cosh(ε_i − ε_j) − 1. This expression is valid at all orders in the difference, supplying the strong-field completion of the quadratic Laplacian action that uses only (ε_i − ε_j)^2 / 2. The module therefore decomposes the full action as exactJCostAction = laplacian_action + quarticRemainder, where the quartic term is assembled from the present remainder function.
proof idea
One-line definition that subtracts the quadratic Taylor polynomial from the standard Real.cosh implementation.
why it matters
The definition supplies the correction term inside quarticRemainder and therefore inside the unconditional decomposition theorem exact_decomposition. That theorem shows the exact J-cost action equals the Laplacian action plus a non-negative remainder that vanishes on the flat vacuum, answering the weak-field limitation raised in Beltracchi §6. It thereby supports the Recognition Science claim that the J-cost side of the Regge identification holds without a small-ε assumption, feeding directly into the T5 J-uniqueness and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.