catalystSelectivityCert
plain-language theorem explainer
This definition supplies a certified instance of the CatalystSelectivityCert structure, confirming exactly five selectivity regimes for heterogeneous catalysts under the J-cost model. Researchers in industrial chemistry modeling branching reactions would reference it to anchor the canonical regimes: perfect, primary-dominant, branching, mixed, and non-selective. The construction is a direct instantiation that pulls in the decidable cardinality proof for the SelectivityRegime type.
Claim. Let $C$ be the structure requiring that the finite cardinality of the set of selectivity regimes equals five. The definition supplies an explicit term of this type by setting the field to the theorem establishing $|$SelectivityRegime$| = 5$.
background
The module introduces five canonical selectivity regimes for heterogeneous catalysts, identified with configuration dimension D = 5. These regimes are perfect selectivity, primary-product dominant, branching selectivity, mixed, and non-selective. The Recognition canonical J(φ) band gates the branching point.
proof idea
The definition constructs the structure instance by directly assigning the five_regimes field to the result of the theorem selectivityRegime_count. This is a one-line wrapper that applies the decidable cardinality result.
why it matters
This definition certifies the enumeration of five regimes in the chemistry extension of the Recognition framework. It supports applications of the J-cost model to catalyst selectivity, consistent with the five-regime classification gated by the J(φ) band. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.