pith. machine review for the scientific record. sign in
def definition def or abbrev

asteroidOreSpectroscopyCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 111def asteroidOreSpectroscopyCert : AsteroidOreSpectroscopyCert where
 112  omega_0_eq := rfl

proof body

Definition body.

 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. -/

depends on (14)

Lean names referenced from this declaration's body.