`asteroidOreSpectroscopyCert`

definition

show as: view math explainer →

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

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

formal source

 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
 114  peak_freq_succ := peakFrequency_succ
 115  peak_freq_strict_mono := @peakFrequency_strict_mono
 116  ore_count := OreClass.all_length
 117  ore_distinct := OreClass.all_nodup
 118  adjacent_ratio := adjacent_class_ratio
 119
 120/-- **ASTEROID ORE SPECTROSCOPY ONE-STATEMENT.** Seven ore classes with
 121peak frequencies on the φ-ladder; adjacent classes differ by exactly
 122factor φ; strictly monotonic. -/
 123theorem ore_spectroscopy_one_statement :
 124    OreClass.all.length = 7 ∧
 125    (∀ k, peakFrequency (k + 1) = peakFrequency k * phi) ∧
 126    (∀ (c₁ c₂ : OreClass), c₂.rung = c₁.rung + 1 →
 127       OreClass.peak c₂ = OreClass.peak c₁ * phi) :=
 128  ⟨OreClass.all_length, peakFrequency_succ, adjacent_class_ratio⟩
 129
 130end
 131
 132end AsteroidOreSpectroscopy
 133end Engineering
 134end IndisputableMonolith

papers checked against this theorem

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