referenceGap

formal source

  32noncomputable section
  33
  34/-- Reference gap-to-asymptote for any event (RS-native 1). -/
  35def referenceGap : ℝ := 1
  36
  37/-- Predicted gap at improvement step `N`. -/
  38def gapAt (N : ℕ) : ℝ := referenceGap * phi ^ (-(N : ℤ))
  39
  40theorem gapAt_pos' (N : ℕ) : 0 < gapAt N := by
  41  unfold gapAt referenceGap
  42  have h : 0 < phi ^ (-(N : ℤ)) := zpow_pos Constants.phi_pos _
  43  linarith
  44
  45theorem gapAt_succ_ratio (N : ℕ) :
  46    gapAt (N + 1) = gapAt N * phi⁻¹ := by
  47  unfold gapAt
  48  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  49  have : phi ^ (-((N : ℤ) + 1)) = phi ^ (-(N : ℤ)) * phi⁻¹ := by
  50    rw [show (-((N : ℤ) + 1)) = -(N : ℤ) + (-1 : ℤ) by ring]
  51    rw [zpow_add₀ hphi_ne]; simp
  52  have hcast : ((N + 1 : ℕ) : ℤ) = (N : ℤ) + 1 := by push_cast; ring
  53  rw [hcast, this]; ring
  54
  55/-- The ratio of consecutive gaps is exactly 1/φ. -/
  56theorem consecutive_gap_ratio (N : ℕ) :
  57    gapAt (N + 1) / gapAt N = phi⁻¹ := by
  58  rw [gapAt_succ_ratio]
  59  field_simp [(gapAt_pos' N).ne']
  60
  61/-- Consecutive gaps are strictly decreasing. -/
  62theorem gapAt_strictly_decreasing (N : ℕ) :
  63    gapAt (N + 1) < gapAt N := by
  64  rw [gapAt_succ_ratio]
  65  have hk : 0 < gapAt N := gapAt_pos' N