`all_nodup`

proved

show as: view math explainer →

module: IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
domain: Engineering
line: 83 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Engineering.AsteroidOreSpectroscopy on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  80
  81theorem all_length : all.length = 7 := by decide
  82
  83theorem all_nodup : all.Nodup := by decide
  84
  85def peak (c : OreClass) : ℝ := peakFrequency c.rung
  86
  87theorem peak_pos (c : OreClass) : 0 < peak c := peakFrequency_pos _
  88
  89end OreClass
  90
  91/-! ## §3. Adjacent-class peak ratio -/
  92
  93theorem adjacent_class_ratio (c₁ c₂ : OreClass)
  94    (h : c₂.rung = c₁.rung + 1) :
  95    OreClass.peak c₂ = OreClass.peak c₁ * phi := by
  96  unfold OreClass.peak; rw [h]; exact peakFrequency_succ _
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.