lemma
proved
K_def
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants on GitHub at line 492.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
489Defined (non-circularly) as \(K = \varphi^{1/2}\). -/
490@[simp] noncomputable def K : ℝ := phi ^ (1/2 : ℝ)
491
492@[simp] lemma K_def : K = phi ^ (1/2 : ℝ) := rfl
493
494lemma K_pos : 0 < K := by
495 -- φ > 0, hence φ^(1/2) > 0
496 simpa [K] using Real.rpow_pos_of_pos phi_pos (1/2 : ℝ)
497
498lemma K_nonneg : 0 ≤ K := le_of_lt K_pos
499
500/-- Alias matching parallel-work naming convention. -/
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