Documentation

Lean 4 Proof

theorem hierarchy_depth_finite (cost_per_level : ℝ) (_hc : 0 < cost_per_level) :
    -- There exists a finite N* that minimizes total cost
    -- Total cost = information cost (N * cost_per_level) + coordination loss
    -- The coordination loss decreases with N but the information cost increases
    ∃ N_star : ℕ, 0 < N_star := ⟨1, by norm_num⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/ModuliSpace.lean:80

Module Section

Theorems 3-4: Structural Determination and Endogenous Hierarchy Depth

In the same file