rockCycleCert
plain-language theorem explainer
rockCycleCert supplies a concrete witness for the rock cycle certificate by filling its five_states field with the decided cardinality of rock states. Geologists using the Recognition Science framework cite it to anchor the five-state cycle (igneous, sedimentary, metamorphic, partial melt, magma) to configDim. The definition is a one-line wrapper that directly assigns the upstream cardinality theorem.
Claim. The rock cycle certificate is the structure asserting that the finite set of rock states has cardinality exactly five, where the states comprise igneous, sedimentary, metamorphic, partial melt, and magma. This instance is obtained by assigning the value of the theorem that establishes the cardinality by exhaustive decision.
background
The module RockCycleFromConfigDim derives the rock cycle from configDim, fixing five canonical states whose transitions are gated by recognition J-cost on the temperature-pressure ratio. RockCycleCert is the structure whose sole field requires Fintype.card RockState = 5. The upstream theorem rockState_count proves this equality by decide, supplying the concrete value used in the definition.
proof idea
This definition is a one-line wrapper that applies the rockState_count theorem to populate the five_states field of the RockCycleCert structure.
why it matters
This declaration anchors the five-state rock cycle to configDim within the Recognition Science geology module, providing the base certificate for J-cost gated transitions. It fills the D = 5 requirement for rock states and supports downstream modeling of the cycle, though no parent theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.