decayMode_count
plain-language theorem explainer
The finite set of radioactive decay modes has cardinality five, matching the five canonical modes alpha, beta-minus, beta-plus, gamma, and spontaneous fission. Nuclear physicists working in the Recognition Science framework cite this when fixing the dimension of the decay configuration space. The proof is a direct computation via the decide tactic on the Fintype instance derived from the inductive definition.
Claim. The cardinality of the set of decay modes satisfies $|D| = 5$ where $D = {alpha, beta^-, beta^+, gamma, spontaneous fission}$.
background
DecayMode is the inductive type whose five constructors are alpha, betaMinus, betaPlus, gamma, and spontaneousFission; a Fintype instance is derived automatically from this definition. The module identifies these five modes with configDim D = 5 and states that the Lean development contains zero sorry or axiom. The sole upstream dependency is the inductive definition of DecayMode itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the cardinality directly from the Fintype derivation on the inductive type.
why it matters
This theorem supplies the five_modes field inside the radioactiveDecayCert definition, anchoring the nuclear-physics layer of the Recognition Science framework to the value five for the decay configuration dimension. It realizes the module claim that five canonical modes equal configDim D = 5 and feeds the downstream certificate used by higher-level physics constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.