peak
plain-language theorem explainer
The definition peak assigns each asteroid ore class its characteristic spectral peak on the phi-ladder. Engineers and spectroscopists analyzing mineral resonances would cite it to rank seven classes by rung and bound discrimination. It is realized as a one-line composition of the class rung extractor with the base frequency formula omega_0 * phi^k.
Claim. For an ore class $c$, the peak frequency equals $omega_0 phi^{r(c)}$, where $r(c)$ is the integer rung of $c$ (silicate at 0 through platinoid at 6) and $omega_0$ is the base frequency.
background
The Asteroid Ore Spectroscopy module treats mineral identification via phi-ladder phonon resonance, with each of seven ore classes carrying a distinct rung k. The inductive OreClass enumerates silicate (k=0), carbonate (k=1), oxide (k=2), sulfide (k=3), metallic_Fe (k=4), metallic_Ni (k=5), and platinoid (k=6). The sibling rung function maps each constructor to its integer level, while peakFrequency(k) is defined as omega_0 * phi^k. This local setting implements the Recognition Science frequency scaling inside the engineering track of Plan v5.
proof idea
The definition is a one-line wrapper that applies the OreClass rung extractor to the peakFrequency formula.
why it matters
Peak supplies the concrete frequency values consumed by downstream results on CMB acoustic peak ratios and photobiomodulation neutral patterns. It fills the engineering slot in the phi-ladder scaling that originates from the self-similar fixed point phi and the Recognition Composition Law. The module falsifier flags any sample whose observed peak ratios lie outside the interval [1/(2 phi), 2 phi].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.