adjacent_class_ratio
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the base frequency omega_0 or the numerical value of phi.
- Does not address non-adjacent classes or rung differences other than +1.
- Does not incorporate measurement noise or finite spectral resolution.
- Does not prove that the seven-class assignment is the only possible ladder.
Lean usage
have h := adjacent_class_ratio c1 c2 rung_hypformal statement (Lean)
93theorem adjacent_class_ratio (c₁ c₂ : OreClass)
94 (h : c₂.rung = c₁.rung + 1) :
95 OreClass.peak c₂ = OreClass.peak c₁ * phi := by
proof body
Term-mode proof.
96 unfold OreClass.peak; rw [h]; exact peakFrequency_succ _
97
98/-! ## §4. Master certificate -/
99