exactJCostAction

formal source

  95    This is what the Recognition Composition Law actually prescribes.
  96    The quadratic `laplacian_action G ε` is the leading-order
  97    truncation (see `exact_decomposition` below). -/
  98def exactJCostAction {n : ℕ} (G : WeightedLedgerGraph n)
  99    (ε : LogPotential n) : ℝ :=
 100  ∑ i : Fin n, ∑ j : Fin n,
 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