OreClass
plain-language theorem explainer
OreClass enumerates seven mineral classes ranked by successive rungs on the phi-ladder for phonon resonance peaks in asteroid spectroscopy. Engineers applying Recognition Science to spectral discrimination would cite it when building certificates that bound peak ratios. The declaration is a direct inductive definition with seven named constructors carrying implicit rung indices 0 through 6.
Claim. The inductive type $OreClass$ consists of seven constructors: silicate at rung 0, carbonate at rung 1, oxide at rung 2, sulfide at rung 3, metallic Fe at rung 4, metallic Ni at rung 5, and platinoid at rung 6.
background
The Asteroid Ore Spectroscopy module derives engineering applications from phi-ladder phonon resonances, where each ore class receives a characteristic peak frequency $omega_k = omega_0 phi^k$. Supporting definitions include peakFrequency together with its positivity, zero, successor, and strict monotonicity theorems; the list of all classes; and the rung accessor that maps each constructor to its integer index. The module imports Constants (supplying omega_0 and phi) and Cost, and operates under the J3 track of Plan v5.
proof idea
Inductive definition introducing seven constructors with no proof body or lemma applications. The rung association is supplied by a later sibling definition rather than being part of the inductive declaration itself.
why it matters
OreClass populates the finite set required by AsteroidOreSpectroscopyCert, all, and the one-statement theorem ore_spectroscopy_one_statement that asserts seven classes, exact phi ratios between adjacent rungs, and strict monotonicity. It supplies the concrete enumeration needed to state the module falsifier (spectra with more than five peaks whose ratios fall outside the phi band). This places the phi-ladder (T6 self-similar fixed point) into an applied spectroscopy setting while feeding the eight-tick octave structure downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.