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

all

show as:
view Lean formalization →

The definition enumerates the seven ore classes for phi-ladder asteroid spectroscopy, assigning each a rung k from 0 to 6. Engineers applying Recognition Science to spectral peak modeling cite this list when computing omega_0 * phi^k for discrimination. It is assembled by direct listing of the inductive constructors.

claimLet the ore classes be the seven variants silicate ($k=0$), carbonate ($k=1$), oxide ($k=2$), sulfide ($k=3$), metallic Fe ($k=4$), metallic Ni ($k=5$), platinoid ($k=6$). Then all is the list of these classes, each with peak frequency $omega_0 phi^k$.

background

The Asteroid Ore Spectroscopy module derives ore identification from phi-ladder phonon resonance. OreClass is the inductive type with exactly those seven constructors, each linked to rung k. Peak frequency is defined as omega_0 * phi^k, with supporting facts that the value is positive for all k and equals omega_0 at k=0.

proof idea

The definition is a direct enumeration of the seven OreClass constructors in rung order. No lemmas or tactics are invoked; the body is the literal list construction.

why it matters in Recognition Science

This list supplies the domain for the seven-class ranking in the engineering track and is referenced by convexity theorems for the J-action in FunctionalConvexity as well as length and nodup results in NarrativeGeodesic. It implements the phi-ladder step of the module, consistent with the seven-element pattern seen in plot families and Greek modes, and supports the discrimination floor bounds.

scope and limits

formal statement (Lean)

  78def all : List OreClass :=

proof body

Definition body.

  79  [.silicate, .carbonate, .oxide, .sulfide, .metallic_Fe, .metallic_Ni, .platinoid]
  80

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.