RockCycleCert
plain-language theorem explainer
RockCycleCert packages the assertion that the rock cycle state space has cardinality five. Geologists applying Recognition Science to transition rates would cite this to confirm configDim D equals five for the domain. The declaration is a bare structure whose single field records the Fintype cardinality of the RockState inductive type.
Claim. A certificate structure whose sole field asserts that the cardinality of the rock-state set equals five, where the states are the five constructors igneous, sedimentary, metamorphic, partialMelt, and magma.
background
The module models the rock cycle with five canonical states whose transitions are controlled by the J-cost function on temperature-pressure ratios. RockState is the inductive type enumerating igneous, sedimentary, metamorphic, partialMelt, and magma, and the certificate records that this type has Fintype cardinality five, matching the module convention configDim D = 5. The upstream RockState definition supplies the enumeration; no further lemmas are required for the cardinality fact.
proof idea
The declaration is a structure definition with a single field. It directly encodes the proposition Fintype.card RockState = 5 without invoking any lemmas or tactics.
why it matters
The certificate supplies the dimensionality fact consumed by the downstream rockCycleCert definition, which constructs an explicit instance via rockState_count. It anchors the geological application to the five-state rock cycle inside the Recognition framework, consistent with the module's configDim D = 5 setting. No open questions or scaffolding are indicated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.