rockState_count
plain-language theorem explainer
The result establishes that the finite type of rock states in the Recognition Science geology model has cardinality five. Researchers modeling the rock cycle under configDim constraints cite this when verifying the five-state structure. The proof is a decision procedure that enumerates the five inductive constructors.
Claim. The set of canonical rock states has cardinality five: $|$ {igneous, sedimentary, metamorphic, partial melt, magma} $| = 5$.
background
The module defines the rock cycle from configDim, with five canonical rock states (= configDim D = 5): igneous, sedimentary, metamorphic, partial melt, magma. Transition rates are gated by recognition J-cost on the temperature/pressure ratio. The upstream result is the inductive definition of the rock state type with these five constructors, from which a Fintype instance is derived.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the cardinality of the Fintype instance generated from the inductive definition.
why it matters
This supplies the five_states field in the rock cycle certificate definition. It realizes the module's assertion that the rock cycle has five states matching configDim D = 5. It touches no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.