adjacent_class_ratio
plain-language theorem explainer
Adjacent ore classes on the phi-ladder satisfy a peak-frequency ratio of exactly phi when their rungs differ by one. Asteroid mineral spectroscopists would cite the result to certify geometric progression in observed spectral lines for the seven enumerated classes. The proof is a one-line wrapper that unfolds the peak definition and invokes the successor property of the frequency sequence.
Claim. Let $c_1$ and $c_2$ be ore classes with rung$(c_2)=$ rung$(c_1)+1$. Then peak$(c_2)=$ peak$(c_1)cdot phi$.
background
The Asteroid Ore Spectroscopy module models mineral identification via phi-ladder phonon resonances. OreClass is the inductive enumeration of seven classes (silicate at rung 0 through platinoid at rung 6) equipped with the rung function that maps each constructor to its integer index. Peak frequency for a class is defined by peak$(c):=$ peakFrequency(rung$(c))$, where peakFrequency$(k):=$ omega_0 cdot phi^k.
proof idea
The proof is a one-line wrapper. It unfolds OreClass.peak on both sides, rewrites the rung hypothesis, and applies the upstream lemma peakFrequency_succ which states peakFrequency$(k+1)=$ peakFrequency$(k)cdot phi$.
why it matters
The lemma supplies the adjacent-class step inside ore_spectroscopy_one_statement and is packaged into the master certificate asteroidOreSpectroscopyCert. It realizes the phi-ladder for the J3 engineering track, consistent with the self-similar fixed point forced at T6 of the UnifiedForcingChain. The result directly supports the discrimination floor stated in the module falsifier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.