peakFrequency_strict_mono
plain-language theorem explainer
The theorem establishes strict monotonicity of peak frequency with rung index k on the phi-ladder for asteroid ore identification. Spectroscopists and engineers would cite it to guarantee distinct spectral peaks for different mineral classes. The proof is a term-mode reduction that unfolds the definition and chains positivity of the base frequency with power monotonicity under phi greater than one.
Claim. For natural numbers $k_1 < k_2$, the peak frequency satisfies $omega_0 phi^{k_1} < omega_0 phi^{k_2}$, where $omega_0 > 0$ is the base frequency and $phi > 1$ is the golden ratio.
background
In the Asteroid Ore Spectroscopy module the peak frequency at rung k is defined by unfolding to $omega_0 phi^k$, with $omega_0$ a positive real constant. The golden ratio satisfies $1 < phi$ by the lemma one_lt_phi imported from Constants and PhiSupport. This construction ranks mineral classes by integer rung and supplies the discrimination floor for phonon-resonance identification.
proof idea
The term proof first unfolds peakFrequency, then applies mul_lt_mul_iff_of_pos_left using the theorem omega_0_pos, and finally invokes pow_lt_pow_right₀ with one_lt_phi together with the hypothesis k1 < k2.
why it matters
The result is invoked inside asteroidOreSpectroscopyCert to certify the full spectroscopy procedure. It supplies the ordering step required by the module's falsifier condition on peak ratios lying inside [1/(2 phi), 2 phi] of phi, closing the engineering derivation in Track J3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.