pith. machine review for the scientific record. sign in
def definition def or abbrev high

peak

show as:
view Lean formalization →

The definition assigns to each asteroid ore class its characteristic spectral peak frequency on the φ-ladder, computed as the base frequency scaled by φ to the power of the class rung. Spectroscopists and cosmologists mapping mineral resonances to acoustic peaks would reference this when certifying discrimination bounds. It is realized as a direct delegation to the rung-indexed peak frequency function.

claimFor an ore class $c$, let $r(c)$ denote its rung index. The peak frequency is $ω_0 φ^{r(c)}$, where $ω_0$ is the base frequency and $φ$ the golden ratio.

background

The module derives asteroid ore identification from φ-ladder phonon resonances. OreClass is an inductive enumeration of seven mineral types, each assigned a rung k from 0 (silicate) to 6 (platinoid). The peak frequency for rung k is defined as ω₀ ⋅ φ^k, with ω₀ the base frequency in RS units. This builds on the rung mapping that sends each ore class to its integer index, and on the general peakFrequency definition that scales the base by powers of φ. Upstream results include the rung definitions from mass anchors and constants that fix φ as the self-similar fixed point. The local setting is the engineering track for spectral discrimination, with the falsifier being observation of peaks outside the φ-ratio band.

proof idea

The definition is a one-line wrapper that applies the peakFrequency function to the rung of the given ore class.

why it matters in Recognition Science

This definition supplies the spectral peak for each ore class in the asteroid spectroscopy track, feeding into downstream certifications such as CMB acoustic peak ratios and photobiomodulation patterns. It realizes the φ-ladder resonance for engineering applications, consistent with the eight-tick octave and D=3 spatial dimensions in the forcing chain. It touches the open question of empirical validation against real asteroid spectra.

scope and limits

formal statement (Lean)

  85def peak (c : OreClass) : ℝ := peakFrequency c.rung

proof body

Definition body.

  86

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.