peakFrequency
plain-language theorem explainer
Peak frequency at rung k is defined as the reference frequency omega_0 multiplied by phi to the power k. Asteroid ore spectroscopy work cites this when assigning spectral peaks to mineral classes ranked on the phi-ladder. The definition is a direct abbreviation that multiplies the baseline by the geometric factor phi^k.
Claim. The peak frequency at rung $k$ is given by $ω_0 φ^k$, where $ω_0$ is the reference spectral peak (silicate baseline).
background
The Asteroid Ore Spectroscopy module derives asteroid-ore identification via φ-ladder phonon resonance. Each ore class receives a characteristic spectral peak on the ladder, with seven classes ranked by rung index. The reference frequency omega_0 is fixed at 1 in native units and serves as the silicate baseline for all higher rungs.
proof idea
Direct definition that multiplies the constant reference frequency by the geometric term phi raised to the rung index k. No lemmas or tactics are invoked beyond the built-in definition of real exponentiation.
why it matters
This definition supplies the explicit frequency assignment used by AsteroidOreSpectroscopyCert and ore_spectroscopy_one_statement. The latter asserts seven ore classes whose adjacent peaks differ by exactly the factor phi and are strictly monotonic. It fills the engineering derivation track by providing the phi-ladder scaling required for spectral discrimination bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.