ore_spectroscopy_one_statement
plain-language theorem explainer
The theorem states that asteroid ore classes number exactly seven, with peak frequencies forming a geometric sequence of ratio phi and adjacent rung classes differing by precisely that factor. Mineral spectroscopists modeling phonon resonances in asteroid samples would cite the result to bound distinguishable classes under the phi-ladder. The proof is a direct term-mode tuple that packages the class-list length lemma, the peak-frequency successor rule, and the adjacent-ratio theorem.
Claim. The set of ore classes has cardinality seven, the peak frequency satisfies $ω(k+1) = ω(k) ⋅ ϕ$ for every natural number $k$, and for any two ore classes whose rungs differ by one the peak frequency of the higher class equals the peak frequency of the lower class multiplied by ϕ.
background
OreClass is the inductive type with seven constructors (silicate at rung 0 through platinoid at rung 6). Its peak frequency is defined by peakFrequency(k) := omega_0 ⋅ ϕ^k, with the successor rule peakFrequency(k+1) = peakFrequency(k) ⋅ ϕ following from the definition. The module treats asteroid-ore identification as φ-ladder phonon resonance, ranking seven mineral classes by rung and bounding the discrimination floor. Upstream results supply parallel length lemmas: NarrativeGeodesic.all_length establishes a seven-element list of plot families, while KinshipGraphCohomology.all_length gives length eight for kinship systems; adjacent_class_ratio supplies the rung-to-frequency step used here.
proof idea
The proof is a term-mode construction that directly assembles the three conjuncts: OreClass.all_length for the cardinality claim, peakFrequency_succ for the universal successor rule on frequencies, and adjacent_class_ratio for the rung-difference implication. No tactics are invoked; the term simply packages the three already-proved facts into the conjunction.
why it matters
This declaration completes the master certificate for Track J3 of the engineering derivation, supplying the single-statement summary of the seven-class phi-ladder. It mirrors the seven-element lists appearing in NarrativeGeodesic and the eight-tick structure from the forcing chain (T7), reinforcing the self-similar fixed point phi (T6). The module doc-comment supplies the concrete falsifier: spectroscopy revealing more than five distinct peaks whose ratios fall outside [1/(2ϕ), 2ϕ] of ϕ would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.