consecutive_gap_ratio

formal source

  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
  66  have hphi_inv_lt_one : phi⁻¹ < 1 :=
  67    inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
  68  have : gapAt N * phi⁻¹ < gapAt N * 1 :=
  69    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  70  simpa using this
  71
  72structure RecordProgressionCert where
  73  gap_pos : ∀ N, 0 < gapAt N
  74  one_step_ratio : ∀ N, gapAt (N + 1) = gapAt N * phi⁻¹
  75  consecutive_ratio : ∀ N, gapAt (N + 1) / gapAt N = phi⁻¹
  76  strictly_decreasing : ∀ N, gapAt (N + 1) < gapAt N
  77
  78/-- Athletic-record-progression fit certificate. -/
  79def recordProgressionCert : RecordProgressionCert where
  80  gap_pos := gapAt_pos'
  81  one_step_ratio := gapAt_succ_ratio
  82  consecutive_ratio := consecutive_gap_ratio
  83  strictly_decreasing := gapAt_strictly_decreasing
  84
  85end
  86end RecordProgressionFit