Singularity Time Pos

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem singularity_time_pos {gamma K_0 : ℝ}
    (hgamma : 1 < gamma) (hK : 0 < K_0) :
    0 < singularityTime gamma K_0 :=
  div_pos one_pos (mul_pos (by linarith) hK)

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:160

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 two_period_overinvestment saturation_escape_rate effectiveAlpha_monotone_J collapse_at_J1 crossing_threshold_reexport