omega_0_pos
plain-language theorem explainer
The theorem establishes that the reference spectral peak frequency ω₀ is strictly positive. Asteroid ore spectroscopy models would cite this positivity to guarantee that all derived peak frequencies ω_k = ω₀ · φ^k remain positive on the φ-ladder. The proof is a one-line term that unfolds the definition of ω₀ to the constant 1 and applies norm_num.
Claim. $0 < ω_0$ where $ω_0$ denotes the reference spectral peak frequency for the silicate baseline.
background
The Asteroid Ore Spectroscopy module derives mineral identification from φ-ladder phonon resonances, with each ore class assigned a rung k and peak frequency ω_k = ω_0 · φ^k. The reference ω_0 is defined as the real number 1. The rung function maps silicate to rung 0, carbonate to 1, oxide to 2, sulfide to 3, and metallic_Fe to 4. Upstream results include the rung definitions from AnchorPolicy and RSBridge that supply the integer ladder positions used in mass and frequency formulas.
proof idea
The proof is a one-line term wrapper that unfolds the definition of omega_0 to the constant 1 and applies norm_num to confirm 0 < 1.
why it matters
This result is invoked by peakFrequency_pos via mul_pos omega_0_pos (pow_pos phi_pos _) and by peakFrequency_strict_mono to establish strict increase. It supplies the base positivity for the φ-ladder model in Track J3 of Plan v5. Within the Recognition framework it anchors the positivity required for the eight-tick octave and the D = 3 spatial dimensions that follow from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.