all
plain-language theorem explainer
The definition enumerates the seven mineral classes ordered by increasing φ-ladder rung for asteroid ore spectroscopy. Planetary engineers and spectroscopists cite it to map observed spectral peaks to ore types through the relation ω_k = ω_0 φ^k. It is a direct list literal that matches the seven constructors of the OreClass inductive type.
Claim. Let OreClass be the inductive type whose constructors are silicate (k=0), carbonate (k=1), oxide (k=2), sulfide (k=3), metallic Fe (k=4), metallic Ni (k=5) and platinoid (k=6). Then all is the list [silicate, carbonate, oxide, sulfide, metallic Fe, metallic Ni, platinoid] ordered by rung index k.
background
The Asteroid Ore Spectroscopy module treats Track J3 of Plan v5 as an engineering derivation. Asteroid-ore identification uses φ-ladder phonon resonance, with each class assigned a peak frequency peakFrequency k := omega_0 * phi ^ k. The OreClass inductive type supplies the seven mineral classes ranked by rung k, and the module states that the list ranks seven mineral classes by their k-rung and bounds the discrimination floor.
proof idea
The definition is a direct list literal that enumerates the seven constructors of OreClass in rung order. It follows the same pattern as the sibling definitions NarrativeGeodesic.all, KinshipGraphCohomology.all and ModalPreferenceFromPhi.all, each supplying a canonical seven-element list.
why it matters
This definition supplies the explicit domain of ore classes that downstream results in Action.FunctionalConvexity rely on when proving convexity of the J-action and unconditional geodesic minimization. It realizes the seven-class φ-ladder ranking required by the engineering track, consistent with the recurring seven-element enumerations and the eight-tick octave structure (T7) across the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.