`all`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.AsteroidOreSpectroscopy on GitHub at line 78.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  75  | .metallic_Ni => 5
  76  | .platinoid   => 6
  77
  78def all : List OreClass :=
  79  [.silicate, .carbonate, .oxide, .sulfide, .metallic_Fe, .metallic_Ni, .platinoid]
  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 →

papers checked against this theorem

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