quarticRemainder
plain-language theorem explainer
The quartic remainder supplies the nonlinear correction term in the exact J-cost action on a weighted simplicial ledger graph. Strong-field Regge calculus researchers cite it when decomposing the full action into its quadratic Laplacian piece plus higher-order remainder. The definition is a direct double sum over edge weights times the cosh remainder of each log-potential difference.
Claim. Let $R(G,ε) = ∑_{i,j} w_{ij} · r(ε_i − ε_j)$, where $w_{ij}$ are the symmetric non-negative weights of the ledger graph $G$ and $r(x)$ is the quartic remainder of the hyperbolic cosine, $r(x) = cosh(x) − 1 − x²/2$.
background
The Nonlinear J-Cost / Regge Bridge module constructs the exact J-cost action as ∑ w_{ij} (cosh(ε_i − ε_j) − 1) and shows it equals the quadratic Laplacian action plus this remainder term. WeightedLedgerGraph is the structure carrying a symmetric non-negative weight function on Fin n vertices. LogPotential is the map from vertices to real log-potential values. The upstream laplacian_action_prod_form already expresses the quadratic piece as (1/2) ∑∑ w_{ij} (ε_i − ε_j)².
proof idea
One-line definition that unfolds the double sum over Fin n × Fin n, multiplies each edge weight by the value of coshRemainder on the potential difference, and returns the total as a real number.
why it matters
It supplies the explicit nonlinear correction inside the exact_decomposition theorem, which states exactJCostAction G ε = laplacian_action G ε + quarticRemainder G ε for all ε. This decomposition directly answers Beltracchi §6 by keeping the J-cost side valid at arbitrary field strength while isolating the O(|ε|⁴) remainder. The term appears in the master NonlinearJCostReggeCert and in the strong-field stationarity corollary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.