pith. machine review for the scientific record. sign in
theorem proved tactic proof

phi_gt_one

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  32theorem phi_gt_one : 1 < φ := by

proof body

Tactic-mode proof.

  33  unfold φ
  34  have h5 : (1 : ℝ) < Real.sqrt 5 := by
  35    rw [show (1:ℝ) = Real.sqrt 1 from Real.sqrt_one.symm]
  36    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  37  linarith
  38
  39/-- Scale change μ → μ·eᵗ corresponds to rung shift r → r + t/ln(φ) (definitional). -/
  40example (t : ℝ) : t / Real.log φ = t / Real.log φ := rfl
  41
  42/-- **RS β-FUNCTION STRUCTURE**: For a coupling g with ladder dependence g(r),
  43    β(g) = dg/dt = (1/ln φ) × dg/dr -/

depends on (6)

Lean names referenced from this declaration's body.