`omega_0`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.AsteroidOreSpectroscopy on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  29/-! ## §1. Ore class ladder -/
  30
  31/-- Reference spectral peak `ω_0` (silicate baseline). -/
  32def omega_0 : ℝ := 1
  33
  34theorem omega_0_pos : 0 < omega_0 := by unfold omega_0; norm_num
  35
  36/-- Peak frequency at φ-rung `k`. -/
  37def peakFrequency (k : ℕ) : ℝ := omega_0 * phi ^ k
  38
  39theorem peakFrequency_pos (k : ℕ) : 0 < peakFrequency k :=
  40  mul_pos omega_0_pos (pow_pos phi_pos _)
  41
  42theorem peakFrequency_zero : peakFrequency 0 = omega_0 := by
  43  unfold peakFrequency; simp
  44
  45theorem peakFrequency_succ (k : ℕ) :
  46    peakFrequency (k + 1) = peakFrequency k * phi := by
  47  unfold peakFrequency; rw [pow_succ]; ring
  48
  49theorem peakFrequency_strict_mono {k₁ k₂ : ℕ} (h : k₁ < k₂) :
  50    peakFrequency k₁ < peakFrequency k₂ := by
  51  unfold peakFrequency
  52  exact (mul_lt_mul_iff_of_pos_left omega_0_pos).mpr
  53    (pow_lt_pow_right₀ one_lt_phi h)
  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

papers checked against this theorem

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