`OreClass`

definition

show as: view math explainer →

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

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

used by

formal source

  54
  55/-! ## §2. Named ore classes -/
  56
  57inductive OreClass where
  58  | silicate     -- k=0
  59  | carbonate    -- k=1
  60  | oxide        -- k=2
  61  | sulfide      -- k=3
  62  | metallic_Fe  -- k=4
  63  | metallic_Ni  -- k=5
  64  | platinoid    -- k=6
  65  deriving DecidableEq, Repr
  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 _

papers checked against this theorem

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