phiLatticePoint

formal source

 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
 147  ring
 148
 149/-! ## Reciprocal involution on the phi-ladder -/
 150
 151/-- The reciprocal involution on phi-rungs: `r ↦ -r`.  This is the
 152    discrete analog of the cost reciprocal `x ↦ 1/x`. -/
 153def phiLatticeReciprocal (r : ℤ) : ℤ := -r
 154
 155@[simp] theorem phiLatticeReciprocal_involutive (r : ℤ) :
 156    phiLatticeReciprocal (phiLatticeReciprocal r) = r := by