Singularity Time

def proved Curvature Roles

Documentation

Lean 4 Proof

def singularityTime (gamma K_0 : ℝ) : ℝ :=
  1 / ((gamma - 1) * K_0)

Dependency Graph

Used by

singularity_time_pos

Location

thesis/CESProofs/Applications/AITransition.lean:156

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