`rung`

definition

show as: view math explainer →

module: IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
domain: Engineering
line: 69 · 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 69.

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

  66
  67namespace OreClass
  68
  69def rung : OreClass → ℕ
  70  | .silicate    => 0
  71  | .carbonate   => 1
  72  | .oxide       => 2
  73  | .sulfide     => 3
  74  | .metallic_Fe => 4
  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

papers checked against this theorem

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