peakFrequency_pos
plain-language theorem explainer
Proves that the peak frequency at rung k on the phi-ladder is strictly positive for every natural number k. Engineers modeling asteroid ore spectroscopy and mineral discrimination would cite this to guarantee all spectral peaks exceed zero. The proof is a one-line wrapper that applies multiplication positivity to the base frequency and the phi power.
Claim. For every natural number $k$, if the peak frequency at rung $k$ is defined by $w_k = w_0 phi^k$, then $0 < w_k$.
background
The Asteroid Ore Spectroscopy module models asteroid-ore identification via phi-ladder phonon resonance. Each ore class has a characteristic spectral peak given by $w_k = w_0 cdot phi^k$, with seven mineral classes ranked by k-rung to bound the discrimination floor. The module states this as an engineering derivation with falsifier for samples whose peak ratios fall outside the interval $[1/(2phi), 2phi]$ of phi.
proof idea
This is a one-line wrapper that applies mul_pos to omega_0_pos and pow_pos of phi_pos.
why it matters
Supplies the required positivity for asteroidOreSpectroscopyCert and for peak_pos on each OreClass. It completes the positivity step inside the engineering derivation of spectral peaks on the phi-ladder. The result connects to the self-similar fixed point phi from the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.