Documentation

Lean 4 Proof

theorem rhoJ_channel_differentiated {ρ ρ_min ρ_max J_dot J_val ξ_J : ℝ}
    (hρ_range : ρ_min < ρ) (hρ_max : ρ < ρ_max)
    (hJ_pos : 0 < J_val) (hJ_growth : 0 < J_dot)
    (hξ_diff : ξ_J < 0) :
    -- Channel 5 contribution: ξ_J · (J_dot/J) · (ρ - ρ_min) < 0
    ξ_J * (J_dot / J_val) * (ρ - ρ_min) < 0 := by
  apply mul_neg_of_neg_of_pos
  · apply mul_neg_of_neg_of_pos hξ_diff
    exact div_pos hJ_growth hJ_pos
  · linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:334

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file