quarticRemainder

formal source

 174/-- The quartic remainder of the full action (the "non-linear
 175    correction" to the weak-field Laplacian). It vanishes on the
 176    flat vacuum and is `O(|ε|⁴)` for small `ε`. -/
 177def quarticRemainder {n : ℕ} (G : WeightedLedgerGraph n)
 178    (ε : LogPotential n) : ℝ :=
 179  ∑ i : Fin n, ∑ j : Fin n,
 180    G.weight i j * coshRemainder (ε i - ε j)
 181
 182/-- The quartic remainder is non-negative. -/
 183theorem quarticRemainder_nonneg {n : ℕ} (G : WeightedLedgerGraph n)
 184    (ε : LogPotential n) : 0 ≤ quarticRemainder G ε := by
 185  unfold quarticRemainder
 186  apply Finset.sum_nonneg
 187  intro i _
 188  apply Finset.sum_nonneg
 189  intro j _
 190  exact mul_nonneg (G.weight_nonneg i j) (coshRemainder_nonneg _)
 191
 192/-- Helper: the laplacian action as the product-sum of quadratic terms. -/
 193private theorem laplacian_action_prod_form {n : ℕ}
 194    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 195    laplacian_action G ε
 196      = (1 / 2) * ∑ i : Fin n, ∑ j : Fin n,
 197          G.weight i j * (ε i - ε j) ^ 2 := by
 198  unfold laplacian_action
 199  congr 1
 200
 201/-- **DECOMPOSITION THEOREM.** The exact J-cost action equals the
 202    Laplacian action plus the non-negative quartic remainder:
 203
 204      `exactJCostAction = laplacian_action + quarticRemainder`.
 205
 206    This decomposition is **unconditional** — it holds for all `ε`,
 207    not just small `ε`. In the weak-field regime the remainder is