exactJCostAction_flat

formal source

 101    G.weight i j * (Real.cosh (ε i - ε j) - 1)
 102
 103/-- The exact J-cost action vanishes on the flat vacuum `ε ≡ 0`. -/
 104theorem exactJCostAction_flat {n : ℕ} (G : WeightedLedgerGraph n) :
 105    exactJCostAction G (fun _ => (0 : ℝ)) = 0 := by
 106  unfold exactJCostAction
 107  simp
 108
 109/-- The exact J-cost action is non-negative. -/
 110theorem exactJCostAction_nonneg {n : ℕ} (G : WeightedLedgerGraph n)
 111    (ε : LogPotential n) : 0 ≤ exactJCostAction G ε := by
 112  unfold exactJCostAction
 113  apply Finset.sum_nonneg
 114  intro i _
 115  apply Finset.sum_nonneg
 116  intro j _
 117  apply mul_nonneg (G.weight_nonneg i j)
 118  have h : Real.cosh (ε i - ε j) ≥ 1 := Real.one_le_cosh _
 119  linarith
 120
 121/-! ## §2. J-cost ↔ cosh identity as the non-linear primitive -/
 122
 123/-- **CORE IDENTITY.** For every pair of log-potentials, the J-cost
 124    of the *ratio* `ψ_i / ψ_j = exp(ε_i − ε_j)` equals
 125    `cosh(ε_i − ε_j) − 1`. This is the single-edge formula behind
 126    the exact action above.
 127
 128    This is the full non-linear statement; it is not an
 129    approximation. Proved in `Cost.Jcost_exp_cosh`. -/
 130theorem Jcost_ratio_eq_cosh_minus_one (εi εj : ℝ) :
 131    Jcost (Real.exp (εi - εj)) = Real.cosh (εi - εj) - 1 :=
 132  Cost.Jcost_exp_cosh (εi - εj)
 133
 134/-- The exact J-cost action is a sum of `Jcost`-valued single-edge