theorem superadditivity_qualitative
    (F : AggFun J) (hhom : IsHomogDegOne J F)
    (hconcave : ∀ (x y : Fin J → ℝ) (t : ℝ),
      (∀ j, 0 < x j) → (∀ j, 0 < y j) → 0 ≤ t → t ≤ 1 →
      F (fun j => t * x j + (1 - t) * y j) ≥ t * F x + (1 - t) * F y)
    (x y : Fin J → ℝ) (hx : ∀ j, 0 < x j) (hy : ∀ j, 0 < y j)
    (hFx : 0 < F x) (hFy : 0 < F y) :
    F (fun j => x j + y j) ≥ F x + F y := by
  set s := F x + F y with hs_def
  have hs_pos : 0 < s := by linarith
  set t := F x / s with ht_def
  have ht_ge : 0 ≤ t := div_nonneg (le_of_lt hFx) (le_of_lt hs_pos)
  have ht_le : t ≤ 1 := by rw [ht_def, div_le_one₀ hs_pos]; linarith
  have h1t : 1 - t = F y / s := by
    rw [ht_def]; field_simp; linarith
  set x' := fun j => x j / F x
  set y' := fun j => y j / F y
  have hx' : ∀ j, 0 < x' j := fun j => div_pos (hx j) hFx
  have hy' : ∀ j, 0 < y' j := fun j => div_pos (hy j) hFy
  have hFx' : F x' = 1 := by
    have h1 := hhom x (F x)⁻¹ (inv_pos.mpr hFx)
    rw [show (fun j => (F x)⁻¹ * x j) = x' from by
      ext j; simp [x', div_eq_inv_mul]] at h1
    rw [h1, inv_mul_cancel₀ (ne_of_gt hFx)]
  have hFy' : F y' = 1 := by
    have h1 := hhom y (F y)⁻¹ (inv_pos.mpr hFy)
    rw [show (fun j => (F y)⁻¹ * y j) = y' from by
      ext j; simp [y', div_eq_inv_mul]] at h1
    rw [h1, inv_mul_cancel₀ (ne_of_gt hFy)]
  have mix_eq : ∀ j, x j + y j = s * (t * x' j + (1 - t) * y' j) := by
    intro j; simp only [x', y', ht_def]
    have hFxne : F x ≠ 0 := ne_of_gt hFx
    have hFyne : F y ≠ 0 := ne_of_gt hFy
    have hsne : s ≠ 0 := ne_of_gt hs_pos
    field_simp; ring
  have hconc := hconcave x' y' t hx' hy' ht_ge ht_le
  rw [hFx', hFy'] at hconc
  have hge1 : F (fun j => t * x' j + (1 - t) * y' j) ≥ 1 := by linarith
  have := hhom (fun j => t * x' j + (1 - t) * y' j) s hs_pos
  rw [show (fun j => s * (t * x' j + (1 - t) * y' j)) = (fun j => x j + y j) from by
    ext j; rw [mix_eq]] at this
  rw [this]
  calc s * F (fun j => t * x' j + (1 - t) * y' j)
      ≥ s * 1 := by apply mul_le_mul_of_nonneg_left hge1 (le_of_lt hs_pos)
    _ = s := mul_one s

theorem diversity_encoding (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    (m : EquicorrModel) :
    -- The second-order correction to E[F(X)] is:
    -- -(K/(2c)) · τ²(1-r) = cesEigenvaluePerp J ρ c · (J-1)/J · τ²(1-r) / 2
    let correction := -(curvatureK J ρ) / (2 * m.c) * m.idioVar
    -- This equals the trace of H · Σ restricted to 1⊥, divided by 2
    correction = cesEigenvaluePerp J ρ m.c * (↑J - 1) * m.idioVar / 2 := by
  simp only [curvatureK, cesEigenvaluePerp, EquicorrModel.idioVar]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hcne : m.c ≠ 0 := ne_of_gt m.hc
  field_simp

theorem eigenvaluePerp_sq_proportional_to_K_sq (hJ : 2 ≤ J) (ρ c : ℝ) :
    cesEigenvaluePerp J ρ c ^ 2 =
      curvatureK J ρ ^ 2 / ((↑J - 1) ^ 2 * c ^ 2) := by
  simp only [cesEigenvaluePerp, 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 ces_log_supermodular (J : ℕ) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) (hJ : 0 < J)
    {i j : Fin J} (hij : i ≠ j) :
    0 < cesHessianEntry J ρ c i j := by
  simp only [cesHessianEntry, hij, ite_false, sub_zero, mul_one]
  apply div_pos
  · linarith
  · apply mul_pos
    · positivity
    · exact hc

theorem gainsFromVariety_gt_one (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) :
    1 < gainsFromVariety J ρ := by
  simp only [gainsFromVariety]
  have hJpos : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
  have hexp : 0 < 1 / ρ - 1 := by
    rw [sub_pos, lt_div_iff₀ hρ, one_mul]
    exact hρ1
  calc (1 : ℝ) = 1 ^ (1 / ρ - 1) := (one_rpow _).symm
    _ < (↑J : ℝ) ^ (1 / ρ - 1) := by
        exact rpow_lt_rpow zero_le_one hJpos hexp

theorem diversity_premium_proportional_to_K_logJ (hJ : 2 ≤ J)
    {ρ : ℝ} (hρ : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    Real.log (unnormCES J ρ (symmetricPoint J c) / c) - Real.log ↑J =
      (1 - ρ) / ρ * Real.log ↑J := by
  rw [network_log_premium (by omega) hρ hc]
  field_simp

theorem bridge_theorem {J : ℕ} {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : c ≠ 0) (hJ : (↑J : ℝ) ≠ 0) :
    -hessLogFEigenvalue J ρ c =
    bridgeRatio ρ * escortFisherEigenvalue J ρ c := by
  simp only [hessLogFEigenvalue, escortFisherEigenvalue, bridgeRatio]
  field_simp
  ring

theorem fifth_role_of_K (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) (hρ0 : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    -- K is positive (economic curvature exists)
    0 < curvatureK J ρ ∧
    -- K decomposes as bridge × geometry × Fisher
    curvatureK J ρ =
      bridgeRatio ρ * (↑J - 1) * c ^ 2 * escortFisherEigenvalue J ρ c ∧
    -- The bridge theorem holds
    -hessLogFEigenvalue J ρ c =
      bridgeRatio ρ * escortFisherEigenvalue J ρ c :=
  ⟨curvatureK_pos hJ hρ,
   curvatureK_eq_bridge_times_fisher hρ0 hc.ne' (Nat.cast_ne_zero.mpr (by omega)),
   bridge_theorem hρ0 hc.ne' (Nat.cast_ne_zero.mpr (by omega))⟩

theorem keff_below_critical (J : ℕ) (ρ T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : T < Tstar) :
    effectiveCurvatureKeff J ρ T Tstar =
      curvatureK J ρ * (1 - T / Tstar) := by
  simp only [effectiveCurvatureKeff]
  congr 1
  exact max_eq_right (by rw [sub_nonneg, div_le_one hTs]; exact le_of_lt hT)

theorem order_parameter_exponent_one (J : ℕ) (ρ T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : T < Tstar) :
    effectiveCurvatureKeff J ρ T Tstar =
      curvatureK J ρ * ((Tstar - T) / Tstar) := by
  rw [keff_below_critical J ρ T Tstar hTs hT]
  congr 1; field_simp

theorem landau_minimizer_optimal (t m : ℝ) (hm : 0 ≤ m) :
    landauPotential t (max 0 (-t)) ≤ landauPotential t m := by
  unfold landauPotential
  by_cases ht : 0 ≤ t
  · -- Super-critical: minimizer is 0, V(0) = 0 ≤ V(m)
    rw [max_eq_left (by linarith : -t ≤ 0)]
    nlinarith [sq_nonneg m, mul_nonneg ht hm]
  · -- Sub-critical: V(m) - V(-t) = (m+t)²/2 ≥ 0
    push_neg at ht
    rw [max_eq_right (by linarith : 0 ≤ -t)]
    nlinarith [sq_nonneg (m + t), neg_sq t]

theorem ces_sextuple_role (ρ : ℝ) : SextupleRoleStatement J ρ where
  K_pos := fun hJ hρ => curvatureK_pos hJ hρ
  superadd := fun hJ hρ c hc v hv hv_ne =>
    ces_strict_concavity_on_perp hJ hρ hc v hv hv_ne
  corr_robust := fun hJ hρ m => diversity_encoding hJ hρ m
  strategic := fun hJ hρ c hc δ hδ hδ_ne =>
    ces_strict_concavity_on_perp hJ hρ hc δ hδ hδ_ne
  network := fun hJ hρne c hc =>
    network_scaling hJ hρne hc
  estimation := fun hρ c hc hJ => bridge_theorem hρ hc hJ
  phase := fun T Tstar => keff_eq_K_times_reduced J ρ T Tstar