lemma proved term proof

`one_lt_phiPointSixOne`

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

formal statement (Lean)

 501lemma one_lt_phiPointSixOne : (1.6 : ℝ) < phi := by linarith [phi_gt_onePointSixOne]

Term-mode proof.

 502
 503/-- Alias: phi_gt_one ≡ one_lt_phi, for parallel-work compat. -/

From the project-wide theorem graph. These declarations reference this one in their body.

settlementPopRatio_in_Christaller_band in IndisputableMonolith.Archaeology.UrbanDensityFromPhiLadder decl_use
amocTimescale_in_band in IndisputableMonolith.Oceanography.ThermohalineCirculationFromJCost decl_use
injuryTipPoint_in_band in IndisputableMonolith.Sport.InjuryRiskFromJCost decl_use

Lean names referenced from this declaration's body.

one_lt_phi in IndisputableMonolith.Constants decl_use
phi_gt_onePointSixOne in IndisputableMonolith.Constants decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use