Documentation

Lean 4 Proof

theorem spectral_hierarchy_justifies_N
    {M : ℕ} (spec : OrderedSpectrum M) (γ : ℝ) (_hγ : 1 < γ)
    (hs : HierarchySpec M) (_hj : hs.isJustified spec γ) :
    -- The spectral analysis justifies hs.levels hierarchical levels,
    -- each with timescale separation ≥ γ from adjacent levels.
    0 < hs.levels ∧
    -- Connection to HierarchicalCESEconomy: schematic
    True :=
  ⟨hs.hlevels, trivial⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:340

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file