theorem unique_equilibrium_complements
    (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v)
    (hv_ne : ∃ j, v j ≠ 0) :
    cesHessianQF J ρ c v < 0 :=
  ces_strict_concavity_on_perp hJ hρ hc v hv hv_ne

theorem saddle_point_substitutes
    (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 1 < ρ)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v)
    (hv_ne : ∃ j, v j ≠ 0) :
    0 < cesHessianQF J ρ c v := by
  rw [cesHessianQF_on_perp (by omega) ρ c hc v hv]
  apply mul_pos
  · simp only [cesEigenvaluePerp]
    apply div_pos (by linarith)
    exact mul_pos (by exact_mod_cast (by omega : 0 < J)) hc
  · exact Finset.sum_pos'
      (fun j _ => sq_nonneg (v j))
      (by obtain ⟨j₀, hj₀⟩ := hv_ne
          exact ⟨j₀, Finset.mem_univ _, by positivity⟩)

theorem symmetric_equilibrium_share [NeZero J]
    {a₀ cost₀ : ℝ} {ρ : ℝ}
    (ha : 0 < a₀) (hcost : 0 < cost₀) :
    equilibriumShare (fun _ : Fin J => a₀) (fun _ => cost₀) ρ ⟨0, NeZero.pos J⟩ =
      1 / ↑J := by
  simp only [equilibriumShare, agentFitness]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hω : a₀ * cost₀ ^ (-ρ) ≠ 0 := by
    apply mul_ne_zero (ne_of_gt ha)
    exact ne_of_gt (rpow_pos_of_pos hcost _)
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne J)
  field_simp

theorem deviationGain_eq_K (hJ : 2 ≤ J) (ρ c : ℝ)
    (hc : c ≠ 0) :
    deviationGain J ρ c =
      curvatureK J ρ / (2 * (↑J - 1) * c) := by
  simp only [deviationGain, curvatureK]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr
    (by omega)
  have hJm1_ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast
      (by omega : 1 < J)
    linarith
  field_simp

theorem folkThreshold_valid {ρ : ℝ}
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    {c : ℝ} (hc : 0 < c) (hJ : 2 ≤ J) :
    0 < folkThreshold J ρ c ∧
    folkThreshold J ρ c < 1 := by
  unfold folkThreshold
  have hg : 0 < deviationGain J ρ c := by
    unfold deviationGain
    exact div_pos (by linarith) (mul_pos
      (mul_pos (by norm_num) (by exact_mod_cast
        (by omega : 0 < J))) hc)
  have hp := knockoutPunishment_pos hρ0 hρ1 hc hJ
  exact ⟨div_pos hg (by linarith),
    (div_lt_one (by linarith)).mpr (by linarith)⟩

theorem fitness_advantage_expands_basin {ρ : ℝ} (hρ : 1 < ρ)
    {ωi ωj : ℝ} (_hωi : 0 < ωi) (hωj : 0 < ωj)
    (hadv : ωj < ωi) :
    1 < separatrixRatio ωi ωj ρ := by
  unfold separatrixRatio
  exact Real.one_lt_rpow ((one_lt_div hωj).mpr hadv)
    (amplification_pos hρ)