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)
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) :=
proof body
Term-mode proof.
128 ⟨OreClass.all_length, peakFrequency_succ, adjacent_class_ratio⟩
129
130end
131
132end AsteroidOreSpectroscopy
133end Engineering
134end IndisputableMonolith
depends on (18)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all_length
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
all_length
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
adjacent_class_ratio
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
all_length
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
OreClass
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
peak
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
peakFrequency
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
peakFrequency_succ
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
all_length
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use