peakFrequency_succ
The theorem states that peak frequency on the phi-ladder advances by exactly the factor phi when the rung index increases by one. Asteroid ore spectroscopy derivations cite it to confirm adjacent-class spectral separation. The proof is a one-line wrapper that unfolds the peak-frequency definition, rewrites the power successor, and simplifies algebraically.
claimFor every natural number $k$, the peak frequency at rung $k+1$ equals the peak frequency at rung $k$ multiplied by the golden ratio: $ω_{k+1} = ω_k · φ$, where $ω_k := ω_0 φ^k$.
background
The module treats asteroid-ore identification as φ-ladder phonon resonance. Each ore class is assigned a rung index $k$ and a characteristic peak frequency defined by $ω_k = ω_0 φ^k$, with $ω_0$ the base frequency and $φ$ the golden ratio. The upstream definition supplies exactly this expression for peak frequency at rung $k$. The local setting is Track J3 of Plan v5, which ranks seven mineral classes by rung and bounds discrimination via the ratio $φ$.
proof idea
One-line wrapper that unfolds the definition of peak frequency, rewrites using the successor power rule, and closes with ring simplification.
why it matters in Recognition Science
It supplies the inductive step required by adjacent_class_ratio, which equates peaks of ore classes whose rungs differ by one. The same fact appears in the master certificate asteroidOreSpectroscopyCert and in the one-statement summary ore_spectroscopy_one_statement. The result therefore closes the engineering derivation for φ-ladder spectroscopy, consistent with the self-similar fixed-point property of $φ$ and the eight-tick octave structure.
scope and limits
- Does not prove that exactly seven ore classes exist.
- Does not verify the falsifier condition on samples with more than five peaks.
- Does not derive a numerical value for the base frequency $ω_0$.
- Does not extend the relation to non-integer rung values.
Lean usage
exact peakFrequency_succ _formal statement (Lean)
45theorem peakFrequency_succ (k : ℕ) :
46 peakFrequency (k + 1) = peakFrequency k * phi := by
proof body
One-line wrapper that applies unfold.
47 unfold peakFrequency; rw [pow_succ]; ring
48