`phi_gt_one`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants
domain: Constants
line: 504 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants on GitHub at line 504.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 501lemma one_lt_phiPointSixOne : (1.6 : ℝ) < phi := by linarith [phi_gt_onePointSixOne]
 502
 503/-- Alias: phi_gt_one ≡ one_lt_phi, for parallel-work compat. -/
 504lemma phi_gt_one : 1 < phi := one_lt_phi
 505
 506/-- φ ≈ 1.618 (coarse upper bound used in some modules). -/
 507lemma phi_approx : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
 508
 509/-- J(φ) = φ - 3/2 (exact, using φ² = φ + 1). -/
 510lemma Jcost_phi_val : Cost.Jcost phi = phi - 3 / 2 := by
 511  rw [Cost.Jcost_eq_sq phi_ne_zero]
 512  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
 513  rw [div_eq_iff (by linarith [phi_pos] : 2 * phi ≠ 0)]
 514  nlinarith [phi_pos, hphi_sq]
 515
 516/-- J(φ) > 0 -/
 517lemma Jcost_phi_pos : 0 < Cost.Jcost phi :=
 518  Cost.Jcost_pos_of_ne_one _ phi_pos phi_ne_one
 519
 520end Constants
 521end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.