RockState
plain-language theorem explainer
RockState enumerates the five canonical states of the rock cycle, matching configDim D = 5 in the Recognition framework. Geologists modeling J-cost gated transitions on temperature-pressure ratios would cite this type to fix the state space. The declaration is a direct inductive definition deriving Fintype, DecidableEq, and related classes for immediate cardinality use.
Claim. The rock states are the finite inductive set with elements igneous, sedimentary, metamorphic, partial melt, and magma, equipped with decidable equality and Fintype structure.
background
The module sets the rock cycle as five states tied to configDim D = 5, with transitions governed by recognition J-cost on the temperature-pressure ratio. This follows the Recognition Science derivation of dimensions from the forcing chain (T0-T8) and the Recognition Composition Law, here specialized to geology without spatial D = 3 constraints. The definition imports only Mathlib and Constants, establishing a zero-axiom foundation for state enumeration.
proof idea
The declaration introduces an inductive type with five explicit constructors and derives Fintype, DecidableEq, Repr, and BEq in a single step to enable direct cardinality proofs.
why it matters
RockState supplies the state space required by the downstream RockCycleCert structure (which asserts Fintype.card RockState = 5) and the rockState_count theorem. It realizes the configDim = 5 clause in the geology module, connecting to the framework's T8 dimension forcing and the phi-ladder mass formulas via the shared J-cost mechanism. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.