AsteroidOreSpectroscopyCert
plain-language theorem explainer
AsteroidOreSpectroscopyCert defines a record structure that bundles the assertions omega_0 equals 1, peak frequencies omega_k equal phi to the power k are positive and strictly monotone, exactly seven distinct ore classes exist on the phi-ladder, and adjacent-rung classes satisfy the exact phi ratio. Engineers validating asteroid mineral identification via phonon resonances would cite this certificate to confirm their spectral assignments match the Recognition Science phi-ladder. As a plain structure definition it records the properties without
Claim. A structure certifying that the reference frequency satisfies $omega_0 = 1$, that the peaks $omega_k = phi^k$ obey $0 < omega_k$, $omega_{k+1} = omega_k phi$, and strict monotonicity in $k$, that the list of seven ore classes is duplicate-free, and that any two classes differing by one rung satisfy peak$(c_2) =$ peak$(c_1) phi$.
background
The module models asteroid-ore identification by assigning each of seven mineral classes a characteristic spectral peak on the phi-ladder. peakFrequency is defined by $omega_k = omega_0 phi^k$ with the reference $omega_0$ fixed at 1; OreClass is the inductive type whose constructors are silicate (rung 0) through platinoid (rung 6). Upstream results supply the length-7 list of all classes together with the positivity, recurrence, and strict-monotonicity lemmas for peakFrequency.
proof idea
The declaration is a structure definition whose fields are simply the required propositions; there is no proof body. The downstream construction asteroidOreSpectroscopyCert populates the fields by direct reference to the already-proved lemmas peakFrequency_pos, peakFrequency_succ, peakFrequency_strict_mono and OreClass.all_length.
why it matters
The structure supplies the engineering certificate for Track J3 of Plan v5, confirming that asteroid spectroscopy can be read off the phi-ladder with exactly seven classes and exact phi ratios between adjacent rungs. It is instantiated by asteroidOreSpectroscopyCert and aligns with the self-similar fixed point phi (T6) and the eight-tick octave. The module states an explicit falsifier: any sample exhibiting more than five distinct peaks whose ratios lie outside the interval $[1/(2phi), 2phi]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.