peakFrequency_zero
plain-language theorem explainer
The zero-rung spectral peak equals the silicate baseline frequency exactly. Asteroid ore classification models cite this when initializing the φ-ladder for mineral identification. The proof is a one-line wrapper that unfolds the peak-frequency definition and reduces via simplification.
Claim. The peak frequency at rung zero equals the reference frequency: $ω(0) = ω_0$, where $ω(k) = ω_0 φ^k$ for rung $k$.
background
The Asteroid Ore Spectroscopy module models phonon resonances for ore identification on the φ-ladder. Each mineral class receives a rung $k$ with characteristic peak $ω_k = ω_0 φ^k$. The reference $ω_0$ is the silicate baseline frequency, fixed at 1 in native units. The upstream definition of the peak-frequency function encodes this scaling directly from the self-similar fixed point φ.
proof idea
One-line wrapper that unfolds the peak-frequency definition and applies simplification to reduce φ^0 to 1.
why it matters
This anchors the φ-ladder at the base rung for the seven mineral classes ranked by k in the J3 track. It supplies the starting point for the module's discrimination floor and falsifier condition on peak ratios near φ. The result sits inside the Recognition Science engineering derivation that begins from the T6 fixed-point forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.