all_length
plain-language theorem explainer
The theorem confirms that the list of ore classes for asteroid spectroscopy contains exactly seven elements. Engineers deriving mineral identification from φ-ladder resonances cite this count to bound spectral discrimination. The proof is a one-line decision procedure that unfolds the explicit list and verifies its length.
Claim. Let $L$ be the list of seven ore classes ordered by rung on the φ-ladder: silicate, carbonate, oxide, sulfide, metallic Fe, metallic Ni, platinoid. Then $|L| = 7$.
background
The Asteroid Ore Spectroscopy module (Track J3 of Plan v5) models asteroid-ore identification via φ-ladder phonon resonance. Each ore class has a characteristic spectral peak ω_k = ω_0 · φ^k, and the definition all enumerates seven mineral classes ranked by rung: silicate through platinoid. The module doc states the falsifier as a sample with more than five distinct peaks whose ratios lie outside [1/(2φ), 2φ] of φ.
proof idea
The proof is a one-line wrapper that applies the decide tactic. It unfolds the definition of all to the explicit seven-element list and computes the length directly.
why it matters
This supplies the ore_count field in asteroidOreSpectroscopyCert and is used in ore_spectroscopy_one_statement to assert seven classes with adjacent ratios exactly φ. It parallels all_length results from NarrativeGeodesic (seven plot families) and ModalPreferenceFromPhi (seven modes). In the Recognition framework it fixes the discrete count on the φ-ladder, supporting the self-similar fixed point and seven-element structures across domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.