module module high

`IndisputableMonolith.Engineering.AsteroidOreSpectroscopy`

This module supplies reference definitions for spectral peaks in asteroid ore analysis under Recognition Science. It centers on ω₀ as the silicate baseline peak frequency together with rung-indexed peakFrequency and OreClass. Engineers applying RS constants to spectroscopy would cite these objects. The module is purely definitional with supporting positivity and monotonicity lemmas.

claimLet τ₀ = 1 tick be the RS time quantum. The module defines ω₀ as the reference spectral peak for the silicate baseline, peakFrequency(r) as the frequency at rung r on the phi-ladder, and OreClass as the classification of ores by spectral rung.

background

The module belongs to the Engineering domain and imports the fundamental RS time quantum τ₀ = 1 tick from Constants together with cost structures from Cost. It introduces ω₀ as the silicate baseline peak, peakFrequency as a function of rung, and OreClass as a spectral classification. These objects rest on the phi-ladder and the eight-tick octave conventions of the framework.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the baseline ω₀ and rung-based frequency definitions that ground engineering spectroscopy in RS-native units. It supports downstream models that combine the phi-ladder with mass formulas and the Recognition Composition Law. No used-by edges are recorded in the current graph.

scope and limits

Does not derive ω₀ from the T0-T8 forcing chain.
Does not process raw observational spectra.
Does not extend to non-silicate ore classes.
Does not compute numerical values outside RS units.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (19)

class has L11
def omega_0 L32
theorem omega_0_pos L34
def peakFrequency L37
theorem peakFrequency_pos L39
theorem peakFrequency_zero L42
theorem peakFrequency_succ L45
theorem peakFrequency_strict_mono L49
inductive OreClass L57
def rung L69
def all L78
theorem all_length L81
theorem all_nodup L83
def peak L85
theorem peak_pos L87
theorem adjacent_class_ratio L93
structure AsteroidOreSpectroscopyCert L100
def asteroidOreSpectroscopyCert L111
theorem ore_spectroscopy_one_statement L123