AsteroidOreSpectroscopyCert

formal source

  97
  98/-! ## §4. Master certificate -/
  99
 100structure AsteroidOreSpectroscopyCert where
 101  omega_0_eq : omega_0 = 1
 102  peak_freq_pos : ∀ k, 0 < peakFrequency k
 103  peak_freq_succ : ∀ k, peakFrequency (k + 1) = peakFrequency k * phi
 104  peak_freq_strict_mono : ∀ {k₁ k₂ : ℕ}, k₁ < k₂ →
 105    peakFrequency k₁ < peakFrequency k₂
 106  ore_count : OreClass.all.length = 7
 107  ore_distinct : OreClass.all.Nodup
 108  adjacent_ratio : ∀ (c₁ c₂ : OreClass), c₂.rung = c₁.rung + 1 →
 109    OreClass.peak c₂ = OreClass.peak c₁ * phi
 110
 111def asteroidOreSpectroscopyCert : AsteroidOreSpectroscopyCert where
 112  omega_0_eq := rfl
 113  peak_freq_pos := peakFrequency_pos
 114  peak_freq_succ := peakFrequency_succ
 115  peak_freq_strict_mono := @peakFrequency_strict_mono
 116  ore_count := OreClass.all_length
 117  ore_distinct := OreClass.all_nodup
 118  adjacent_ratio := adjacent_class_ratio
 119
 120/-- **ASTEROID ORE SPECTROSCOPY ONE-STATEMENT.** Seven ore classes with
 121peak frequencies on the φ-ladder; adjacent classes differ by exactly
 122factor φ; strictly monotonic. -/
 123theorem ore_spectroscopy_one_statement :
 124    OreClass.all.length = 7 ∧
 125    (∀ k, peakFrequency (k + 1) = peakFrequency k * phi) ∧
 126    (∀ (c₁ c₂ : OreClass), c₂.rung = c₁.rung + 1 →
 127       OreClass.peak c₂ = OreClass.peak c₁ * phi) :=
 128  ⟨OreClass.all_length, peakFrequency_succ, adjacent_class_ratio⟩
 129
 130end