rung
plain-language theorem explainer
The rung definition assigns integer levels 0 through 6 to the seven asteroid ore classes for phi-ladder spectral peak computation. Asteroid spectroscopists and applied physicists cite it to rank mineral resonances as omega_0 times phi to the power k. It is realized by direct pattern matching on the OreClass inductive type.
Claim. The function rung assigns to each ore class an integer $k$ such that the peak frequency satisfies $ω_k = ω_0 φ^k$, with $k=0$ for silicate, $k=1$ for carbonate, $k=2$ for oxide, $k=3$ for sulfide, $k=4$ for metallic Fe, $k=5$ for metallic Ni, and $k=6$ for platinoid.
background
The Asteroid Ore Spectroscopy module treats mineral identification as phi-ladder phonon resonance, with each ore class carrying a characteristic peak frequency omega_0 times phi to the rung power. The OreClass inductive type enumerates the seven classes together with their assigned k values in the comments. This local engineering track extends the general rung constructions appearing in mass anchor policies and RSBridge fermion assignments, which likewise map discrete levels to phi-scaling.
proof idea
The definition proceeds by exhaustive case analysis on the seven constructors of OreClass, returning the successive integers 0 to 6 exactly as annotated on each variant.
why it matters
This definition supplies the discrete rung values consumed by forty downstream results, including hearingLossPenalty_zero in acoustics and GeometricStrain together with E_PBM_bounds in applied coherence and photobiomodulation devices. It realizes the engineering derivation of Track J3 by furnishing the k that enters ω_k = ω_0 · φ^k, thereby connecting ore spectroscopy to the phi-ladder scaling used across the Recognition framework, including the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.