SmallDeviationState

formal source

  46/-! ## Small-Deviation States -/
  47
  48/-- A state near equilibrium: bond multipliers are 1 + εᵢ with |εᵢ| small. -/
  49structure SmallDeviationState (N : ℕ) where
  50  deviations : Fin N → ℝ
  51  small : ∀ i, |deviations i| ≤ 1 / 2
  52
  53/-- The total J-cost of a small-deviation state is the sum of per-bond costs. -/
  54def totalJcost (s : SmallDeviationState N) : ℝ :=
  55  Finset.univ.sum fun i => Jcost (1 + s.deviations i)
  56
  57/-! ## Quadratic Emergence (PROVED) -/
  58
  59/-- The scalar J-cost expansion: J(1+ε) = ε²/2 + c·ε³ with |c| ≤ 2.
  60    This is the fundamental lemma: J-cost IS a quadratic form near unity. -/
  61theorem quadratic_emergence (ε : ℝ) (hε : |ε| ≤ 1 / 2) :
  62    ∃ c : ℝ, Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 :=
  63  Jcost_one_plus_eps_quadratic ε hε
  64
  65/-- The leading-order energy of a small-deviation state is ½ Σ εᵢ². -/
  66def quadraticEnergy (s : SmallDeviationState N) : ℝ :=
  67  Finset.univ.sum fun i => (s.deviations i) ^ 2 / 2
  68
  69/-- The cubic remainder per bond is bounded. -/
  70theorem per_bond_remainder_bounded (ε : ℝ) (hε : |ε| ≤ 1 / 2) :
  71    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ 2 * |ε| ^ 3 := by
  72  obtain ⟨c, hc_eq, hc_bound⟩ := quadratic_emergence ε hε
  73  rw [hc_eq]
  74  have : ε ^ 2 / 2 + c * ε ^ 3 - ε ^ 2 / 2 = c * ε ^ 3 := by ring
  75  rw [this, abs_mul]
  76  calc |c| * |ε ^ 3|
  77      ≤ 2 * |ε ^ 3| := by nlinarith [abs_nonneg (ε ^ 3)]
  78    _ = 2 * |ε| ^ 3 := by rw [abs_pow]
  79