pith. machine review for the scientific record. sign in
structure definition def or abbrev high

CatalystSelectivityCert

show as:
view Lean formalization →

The selectivity certification structure asserts that heterogeneous catalysis admits exactly five canonical regimes under the J-cost model. Industrial chemists modeling branching and selectivity would cite it to anchor their regime enumeration to the Recognition framework. The definition packages a single cardinality assertion derived from the enumerated regime type.

claimA structure certifying that the set of selectivity regimes has cardinality five, where the regimes are perfect selectivity, primary-product dominant, branching selectivity, mixed, and non-selective.

background

The module treats five canonical selectivity regimes for heterogeneous catalysts, identified with configDim 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 between them.

proof idea

The declaration is a structure definition whose single field states the cardinality equality. It relies on the derived Fintype instance for the inductive enumeration of the five regimes.

why it matters in Recognition Science

This definition anchors the chemistry module by certifying the five regimes, which are used by the downstream catalyst selectivity certificate construction. It connects to the Recognition Science framework where configDim D = 5 for chemistry, gated by the J(φ) band. It fills the B10 industrial chemistry depth proposition.

scope and limits

formal statement (Lean)

  30structure CatalystSelectivityCert where
  31  five_regimes : Fintype.card SelectivityRegime = 5
  32

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.