Documentation

Lean 4 Proof

theorem monotone_activation_chain
    {c₀ α Q₁ Q₂ T₀ a_base β Fbar sigma : ℝ}
    (hc₀ : 0 < c₀) (hα : 0 < α)
    (hQ₁ : 0 < Q₁) (hQ₂ : 0 < Q₂) (hQ : Q₁ < Q₂)
    (hT₀ : 0 < T₀)
    (ha : 0 < a_base) (_hβ : 0 < β) (hF : 0 < Fbar) (hs : 0 < sigma) :
    -- Using K_eff ~ (Tstar - T) as a simplified effective curvature
    -- and T = T₀ · c(Q), the NGM entry at Q₂ exceeds that at Q₁
    let T₁ := T₀ * (c₀ * Q₁ ^ (-α))
    let T₂ := T₀ * (c₀ * Q₂ ^ (-α))
    a_base * (- T₁) * Fbar ^ β / sigma < a_base * (- T₂) * Fbar ^ β / sigma := by
  -- Step 1: Q₁ < Q₂ implies c(Q₁) > c(Q₂) (Wright's Law)
  have hc_dec := wright_law_decreasing hc₀ hα hQ₁ hQ₂ hQ
  -- Step 2: c(Q₁) > c(Q₂) implies T(Q₁) > T(Q₂) (friction-cost monotonicity)
  have hT_dec := friction_increases_with_cost hT₀ hc_dec
  -- Step 3: T₁ > T₂ implies -T₁ < -T₂ implies K_eff₁ < K_eff₂
  have hK_inc : -(T₀ * (c₀ * Q₁ ^ (-α))) < -(T₀ * (c₀ * Q₂ ^ (-α))) := by linarith
  -- Step 4: Higher K_eff → higher NGM entry
  apply div_lt_div_of_pos_right _ hs
  apply mul_lt_mul_of_pos_right _ (rpow_pos_of_pos hF β)
  exact mul_lt_mul_of_pos_left hK_inc ha

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:100

Module Section

Proposition: Endogenous Crossing

In the same file