Documentation

Lean 4 Proof

structure SextupleRoleStatement (J : ℕ) (ρ : ℝ) where
  /-- K > 0 when ρ < 1 and J ≥ 2 -/
  K_pos : 2 ≤ J → ρ < 1 → 0 < curvatureK J ρ
  /-- (a) Superadditivity: the Hessian is negative definite on 1⊥,
      so any reallocation from the symmetric point reduces output -/
  superadd : 2 ≤ J → ρ < 1 → ∀ (c : ℝ), 0 < c →
    ∀ (v : Fin J → ℝ), orthToOne J v → (∃ j, v j ≠ 0) →
    cesHessianQF J ρ c v < 0
  /-- (b) Correlation robustness: the diversity-encoding correction
      is proportional to K · idiosyncratic variance -/
  corr_robust : 2 ≤ J → ρ < 1 →
    ∀ (m : EquicorrModel),
    let correction := -(curvatureK J ρ) / (2 * m.c) * m.idioVar
    correction = cesEigenvaluePerp J ρ m.c * (↑J - 1) * m.idioVar / 2
  /-- (c) Strategic independence: the Hessian is negative on 1⊥,
      so no coalition benefits from manipulation -/
  strategic : 2 ≤ J → ρ < 1 → ∀ (c : ℝ), 0 < c →
    ∀ (δ : Fin J → ℝ), orthToOne J δ → (∃ j, δ j ≠ 0) →
    cesHessianQF J ρ c δ < 0
  /-- (d) Network scaling: G(J) = J^{1/ρ} · c -/
  network : 0 < J → ρ ≠ 0 → ∀ (c : ℝ), 0 < c →
    unnormCES J ρ (symmetricPoint J c) = (↑J : ℝ) ^ (1 / ρ) * c
  /-- (e) Statistical estimation: production curvature = bridge ratio × Fisher info.
      -Hess(log F)|_⊥ = ((1-ρ)/ρ²) · I_Fisher -/
  estimation : ρ ≠ 0 → ∀ (c : ℝ), c ≠ 0 → (↑J : ℝ) ≠ 0 →
    -hessLogFEigenvalue J ρ c = bridgeRatio ρ * escortFisherEigenvalue J ρ c
  /-- (f) Phase ordering: K_eff = K · max(0, 1-T/T*).
      K sets the scale of the order parameter. -/
  phase : ∀ (T Tstar : ℝ),
    effectiveCurvatureKeff J ρ T Tstar = curvatureK J ρ * reducedOrderParam T Tstar

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/QuadrupleRole.lean:32

Module Section

The CES Sextuple Role theorem (Paper 1, Section 9):

In the same file