Documentation

Lean 4 Proof

theorem scaling_idempotency {γ : ℝ}
    (hγ_pos : 0 < γ)
    -- Scale consistency: nested aggregation must scale as λ^γ, not λ^{γ²}
    (hsc : γ * γ = γ) :
    γ = 1 := by
  -- γ·γ = γ means γ(γ-1) = 0
  have h : γ * (γ - 1) = 0 := by nlinarith
  rcases mul_eq_zero.mp h with h1 | h1
  · linarith -- γ = 0 contradicts γ > 0
  · linarith -- γ - 1 = 0 gives γ = 1

Dependency Graph

Location

thesis/CESProofs/Potential/IRS.lean:50

Module Section

Increasing returns to scale results (Paper 1, Section 11):

In the same file