`ore_spectroscopy_one_statement`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.AsteroidOreSpectroscopy on GitHub at line 123.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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.