ConvectionMode
plain-language theorem explainer
The inductive enumeration of mantle convection regimes lists five standard cases: whole-mantle, layered, episodic, plume-driven, and plate-driven. Geophysicists working on heat transport in planetary interiors cite this list when linking Rayleigh-number thresholds to the phi-ladder. The declaration is a bare inductive type that automatically derives a Fintype instance, so cardinality statements reduce to a decide tactic.
Claim. The set of mantle convection modes is the five-element collection consisting of whole-mantle convection, layered convection, episodic convection, plume-driven convection, and plate-driven convection.
background
Mantle convection drives plate tectonics. The Rayleigh number of order 10^7 sets the vigor of convection. Recognition Science expresses the heat flux ratio between convective and conductive limits via the phi-ladder, with adjacent regimes separated by the factor phi. Five canonical modes realize a configuration dimension of 5. This enumeration provides the discrete set whose size is asserted to be five in the companion cardinality result. The module assumes no axioms and no sorry statements.
proof idea
The declaration consists of the inductive definition of the five modes together with the deriving clause that installs DecidableEq, Repr, BEq, and Fintype. No explicit proof body is present; the instances are generated automatically by the Lean type-class mechanism.
why it matters
This definition supplies the five-element set required by the certification structure, whose five-modes field records cardinality five, and by the companion cardinality theorem. It realizes the configuration-dimension equal to five step in the geophysics tier of the Recognition Science framework. The construction connects to the phi-ladder transitions predicted by the J-uniqueness and self-similar fixed-point steps of the forcing chain, while leaving open the explicit mapping of those transitions onto numerical Rayleigh values derived from the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.