peakFrequency_pos
The theorem establishes strict positivity of the peak frequency at every natural-number rung k on the phi-ladder. Asteroid-ore spectroscopy derivations cite it to guarantee all resonance lines lie above zero. The proof is a one-line wrapper that invokes mul_pos on the already-proved positivity of the base frequency omega_0 and the positivity of phi^k.
claimFor every natural number $k$, the peak frequency defined by $0 < omega_0 phi^k$ holds, where $omega_0 > 0$ is the base frequency and $phi$ is the golden ratio.
background
The module treats asteroid-ore identification as phi-ladder phonon resonances, with each mineral class assigned a characteristic peak $omega_k = omega_0 phi^k$. The definition peakFrequency unfolds directly to the product of the base frequency and the power of phi. Upstream, omega_0_pos is obtained by unfolding omega_0 and applying norm_num, supplying the first positive factor.
proof idea
One-line wrapper that applies mul_pos to omega_0_pos and pow_pos phi_pos _.
why it matters in Recognition Science
The result is invoked inside asteroidOreSpectroscopyCert to populate the peak_freq_pos field of the certification record and inside peak_pos to obtain positivity for each OreClass. It closes the positivity requirement for the seven-class phi-ladder model described in the module header, supporting the engineering derivation track that ranks ores by rung.
scope and limits
- Does not compute explicit numerical values of any peak.
- Does not address complex or negative frequencies.
- Does not prove that the listed peaks are the only observable lines.
- Does not extend the positivity claim below rung zero.
Lean usage
example (k : ℕ) : 0 < peakFrequency k := peakFrequency_pos kformal statement (Lean)
39theorem peakFrequency_pos (k : ℕ) : 0 < peakFrequency k :=
proof body
One-line wrapper that applies mul_pos.
40 mul_pos omega_0_pos (pow_pos phi_pos _)
41