theorem damping_cancellation_algebraic {phi_prev sigma_n c_n : ℝ}
    (hsigma : sigma_n ≠ 0) :
    c_n * (phi_prev / sigma_n) * sigma_n = c_n * phi_prev := by
  field_simp

theorem upstream_reform_beta {sigma_prev delta beta1 beta2 : ℝ}
    (hs : 0 < sigma_prev) (hdelta : delta ≠ 0)
    (hb1 : 0 < beta1) (_hb2 : 0 < beta2) (h12 : beta1 < beta2) :
    welfareContribution sigma_prev delta beta2 <
    welfareContribution sigma_prev delta beta1 := by
  simp only [welfareContribution]
  apply div_lt_div_of_pos_left _ hb1 h12
  exact mul_pos hs (sq_pos_of_ne_zero hdelta)

theorem activation_two_level {k10 k21 : ℝ} (hk10 : 0 < k10) (hk21 : 0 < k21) :
    1 < Real.sqrt (k10 * k21) ↔ 1 < k10 * k21 := by
  constructor
  · intro h
    have hsq := sq_lt_sq' (by linarith : -Real.sqrt (k10 * k21) < 1) h
    rw [one_pow, sq_sqrt (mul_nonneg (le_of_lt hk10) (le_of_lt hk21))] at hsq
    exact hsq
  · intro h
    rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
    exact Real.sqrt_lt_sqrt (by linarith) h

theorem large_gap_implies_separation {rSlow rFast γ : ℝ}
    (hSlow : 0 < rSlow) (hFast : 0 < rFast) (_hγ : 0 < γ)
    (hgap : γ < spectralGapRatio rSlow rFast) :
    γ < timescaleFromRate rSlow / timescaleFromRate rFast := by
  rwa [timescale_ratio_eq_rate_ratio hSlow hFast]

theorem aggregateWelfareLoss_nonneg (w z : Fin N → ℝ)
    (hw : ∀ n, 0 < w n) (hz : ∀ n, 0 < z n) :
    0 ≤ aggregateWelfareLoss w z := by
  simp only [aggregateWelfareLoss]
  exact Finset.sum_nonneg fun n _ =>
    mul_nonneg (le_of_lt (hw n)) (welfareDistanceFn_nonneg (hz n))

theorem monotone_activation_chain
    {c₀ α Q₁ Q₂ T₀ a_base β Fbar sigma : ℝ}
    (hc₀ : 0 < c₀) (hα : 0 < α)
    (hQ₁ : 0 < Q₁) (hQ₂ : 0 < Q₂) (hQ : Q₁ < Q₂)
    (hT₀ : 0 < T₀)
    (ha : 0 < a_base) (_hβ : 0 < β) (hF : 0 < Fbar) (hs : 0 < sigma) :
    -- Using K_eff ~ (Tstar - T) as a simplified effective curvature
    -- and T = T₀ · c(Q), the NGM entry at Q₂ exceeds that at Q₁
    let T₁ := T₀ * (c₀ * Q₁ ^ (-α))
    let T₂ := T₀ * (c₀ * Q₂ ^ (-α))
    a_base * (- T₁) * Fbar ^ β / sigma < a_base * (- T₂) * Fbar ^ β / sigma := by
  -- Step 1: Q₁ < Q₂ implies c(Q₁) > c(Q₂) (Wright's Law)
  have hc_dec := wright_law_decreasing hc₀ hα hQ₁ hQ₂ hQ
  -- Step 2: c(Q₁) > c(Q₂) implies T(Q₁) > T(Q₂) (friction-cost monotonicity)
  have hT_dec := friction_increases_with_cost hT₀ hc_dec
  -- Step 3: T₁ > T₂ implies -T₁ < -T₂ implies K_eff₁ < K_eff₂
  have hK_inc : -(T₀ * (c₀ * Q₁ ^ (-α))) < -(T₀ * (c₀ * Q₂ ^ (-α))) := by linarith
  -- Step 4: Higher K_eff → higher NGM entry
  apply div_lt_div_of_pos_right _ hs
  apply mul_lt_mul_of_pos_right _ (rpow_pos_of_pos hF β)
  exact mul_lt_mul_of_pos_left hK_inc ha