all_length
The theorem records that the explicit list of asteroid ore classes contains exactly seven members. Engineers applying φ-ladder phonon resonance to asteroid mineral identification cite this cardinality when bounding the discrimination floor for spectral peaks. The proof is a one-line decide computation that evaluates the length of the enumerated list.
claimThe list of asteroid ore classes has length 7.
background
The Asteroid Ore Spectroscopy module implements track J3 of Plan v5 for engineering derivations. It enumerates seven mineral classes (silicate, carbonate, oxide, sulfide, metallic Fe, metallic Ni, platinoid) each carrying a rung on the phi ladder that sets its characteristic peak frequency ω_k = ω_0 · φ^k. This enumeration parallels the seven-element lists of narrative plot families, nontrivial kinship systems, and Greek musical modes defined in sibling modules.
proof idea
The proof is a one-line wrapper that unfolds the explicit list definition of all ore classes and applies the decide tactic to compute its length.
why it matters in Recognition Science
This length populates the asteroidOreSpectroscopyCert and supplies the ore count in the ore_spectroscopy_one_statement theorem, which asserts seven classes whose adjacent peaks differ by exactly φ with strict monotonicity. It reinforces the seven-fold structure recurring across Recognition Science (T7 eight-tick octave, seven modes, seven plot families) and supports engineering bounds on φ-ladder discrimination. The module doc flags a falsifier for samples exceeding five distinct peaks outside the [1/(2φ), 2φ] ratio interval.
scope and limits
- Does not derive physical resonance frequencies or phonon couplings.
- Does not prove the list exhausts all possible asteroid minerals.
- Does not compute numerical ω_0 or rung-specific peak values.
- Does not invoke the Recognition Composition Law or J-cost.
Lean usage
rw [OreClass.all_length]formal statement (Lean)
81theorem all_length : all.length = 7 := by decide
proof body
82