theorem proved term proof

`phi_inv_lt_one`

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

formal statement (Lean)

 154theorem phi_inv_lt_one : 1/φ < 1 := by

proof body

Term-mode proof.

 155  have h := phi_gt_one
 156  have hp := phi_pos
 157  rw [div_lt_one hp]
 158  linarith
 159
 160/-- The sum φ^(-1) + φ^(-2) + ... converges to φ -/

used by (4)

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

phi_series_sum in IndisputableMonolith.Foundation.PhiEmergence decl_use
lexicon_ratio_lt_one in IndisputableMonolith.Linguistics.LexiconRatio decl_use
passive_fraction_pos in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_lt_one in IndisputableMonolith.Linguistics.LexiconRatio decl_use

depends on (1)

Lean names referenced from this declaration's body.

phi_inv_lt_one in IndisputableMonolith.Linguistics.LexiconRatio decl_use