theorem proved wrapper

`tau_ratio_overshoot`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 233theorem tau_ratio_overshoot :
 234    ratio_tau_e_exp < Constants.phi ^ (17 : ℕ) := by

One-line wrapper that applies linarith.

 235  linarith [phi17_gt, ratio_tau_e_exp_bounds.2]
 236

Lean names referenced from this declaration's body.