log_phi_ne_zero

formal source

 113theorem log_phi_pos : 0 < Real.log phi := Real.log_pos phi_gt_one
 114
 115/-- `log φ` is non-zero. -/
 116theorem log_phi_ne_zero : Real.log phi ≠ 0 := ne_of_gt log_phi_pos
 117
 118/-- `log (φ⁻¹) = -log φ`. -/
 119theorem log_phi_inv : Real.log phi⁻¹ = -Real.log phi := by
 120  exact Real.log_inv phi
 121
 122/-! ## The phi-ladder lattice -/
 123
 124/-- The phi-ladder lattice point at integer rung `r`: the value
 125    `r · log φ` on the log-scale (= `log(φ^r)`). -/
 126def phiLatticePoint (r : ℤ) : ℝ := (r : ℝ) * Real.log phi
 127
 128@[simp] theorem phiLatticePoint_zero : phiLatticePoint 0 = 0 := by
 129  unfold phiLatticePoint; simp
 130
 131@[simp] theorem phiLatticePoint_one : phiLatticePoint 1 = Real.log phi := by
 132  unfold phiLatticePoint; simp
 133
 134/-- The phi-lattice is closed under negation, the discrete analog of
 135    reciprocal symmetry. -/
 136theorem phiLatticePoint_neg (r : ℤ) :
 137    phiLatticePoint (-r) = -phiLatticePoint r := by
 138  unfold phiLatticePoint
 139  push_cast
 140  ring
 141
 142/-- The phi-ladder spacing: consecutive lattice points are `log φ` apart. -/
 143theorem phiLatticePoint_succ (r : ℤ) :
 144    phiLatticePoint (r + 1) = phiLatticePoint r + Real.log phi := by
 145  unfold phiLatticePoint
 146  push_cast