has
plain-language theorem explainer
Asteroid ore classes receive characteristic spectral peaks at frequencies ω_k = ω_0 φ^k on the phi ladder, with seven minerals ranked by integer rung k. Spectroscopists and asteroid mission analysts would cite the assignment when modeling phonon resonances for ore discrimination. The declaration is a direct class definition that encodes the rung-to-peak map with no computational steps or lemmas.
Claim. Each ore class $c$ is assigned a spectral peak frequency satisfying $ω(c) = ω_0 φ^{r(c)}$ where $r(c)$ denotes the rung of $c$ and $ω_0$ is the silicate reference frequency.
background
The module treats asteroid ore identification as an engineering application of φ-ladder phonon resonance. The local rung map sends silicate to rung 0, carbonate to 1, oxide to 2, sulfide to 3 and metallic Fe to 4; the peak map then evaluates peakFrequency at that rung. This setting draws on the discrete tier structure of physical quantities supplied by NucleosynthesisTiers.of and the phi-forcing calibration in PhiForcingDerived.of.
proof idea
Direct definition with empty proof body. The class has is introduced by referencing the sibling rung and peak definitions together with the imported Constants and PreTemporalForcingOrder.rank.
why it matters
The definition supplies the concrete engineering interface that realizes the self-similar fixed point (T6) for spectral data. It is referenced by downstream convexity results such as actionJ_convex_on_interp and by aesthetic constructions such as acceptanceBandRatio_eq and pentatonicSize that reuse the same φ-ratio structure. It thereby closes one engineering track of the Recognition Science derivation while leaving empirical falsification of the discrimination floor open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.