Collapse At J1

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem collapse_at_J1 (rho : ℝ) :
    (1 - rho) / rho * ((↑(1 : ℕ) - 1) / ↑(1 : ℕ)) = 0 := by
  simp

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:226

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file

effectiveTrainingProductivity phieff_exceeds_phi0 phieff_ge_one_condition gcFunction gc_trivial_solution adoptionR0 adoption_threshold baumolGrowthRate baumol_limit baumol_bounded_below singularityTime singularity_time_pos two_period_overinvestment saturation_escape_rate effectiveAlpha_monotone_J crossing_threshold_reexport