axiom kolmogorov_nagumo (J : ℕ) (F : AggFun J)
    (hcont : IsContinuousAgg J F)
    (hsymm : IsSymmetric J F)
    (hincr : IsStrictlyIncreasing J F)
    (hassoc : IsScaleConsistent J F) :
    IsQuasiArithMean J F

axiom aczel (J : ℕ) (F : AggFun J)
    (hqa : IsQuasiArithMean J F)
    (hhom : IsHomogDegOne J F) :
    IsPowerMean J F

theorem emergent_CES (J : ℕ) (F : AggFun J)
    (hcont : IsContinuousAgg J F)
    (hsymm : IsSymmetric J F)
    (hincr : IsStrictlyIncreasing J F)
    (hhom : IsHomogDegOne J F)
    (hsc : IsScaleConsistent J F) :
    IsPowerMean J F := by
  -- Step 1: Scale consistency is associativity.
  -- By the Kolmogorov-Nagumo theorem, F is quasi-arithmetic.
  have hqa : IsQuasiArithMean J F := kolmogorov_nagumo J F hcont hsymm hincr hsc
  -- Step 2: By Aczél's theorem, a homogeneous quasi-arithmetic mean is a power mean.
  exact aczel J F hqa hhom

theorem aggregation_fixed_point (k : ℕ) (F : AggFun k)
    (hcont : IsContinuousAgg k F)
    (hsymm : IsSymmetric k F)
    (hincr : IsStrictlyIncreasing k F)
    (hhom : IsHomogDegOne k F)
    (_hfp : IsAggFixedPoint k F) :
    IsPowerMean k F := by
  -- A fixed point of R_k satisfies scale consistency
  have hsc : IsScaleConsistent k F := by
    intro m n _ x; rfl
  -- By the Emergent CES theorem
  exact aczel k F (kolmogorov_nagumo k F hcont hsymm hincr hsc) hhom