radioactiveDecayCert
plain-language theorem explainer
This definition instantiates the certificate structure for radioactive decay modes by setting its cardinality field to five. Nuclear physicists working in Recognition Science would cite it to anchor the five canonical modes (alpha, beta-minus, beta-plus, gamma, spontaneous fission) to configDim D equals 5. The construction is a direct one-line assignment that pulls the count from the upstream theorem establishing the cardinality of the decay mode type.
Claim. The certificate structure for radioactive decay modes is the instance whose sole field requires that the finite cardinality of the set of decay modes equals five, obtained by direct assignment from the theorem that computes this cardinality.
background
The module identifies five canonical radioactive decay modes that correspond to configuration dimension D equals 5: alpha decay, beta-minus decay, beta-plus decay, gamma emission, and spontaneous fission. The structure RadioactiveDecayCert is defined to hold precisely when the finite type cardinality of the decay mode type equals five. This count is supplied by the upstream theorem decayMode_count, which establishes the equality by a decision procedure.
proof idea
The definition is a one-line wrapper that constructs the structure by assigning its five_modes field directly to the result of the theorem decayMode_count.
why it matters
This definition supplies the certified count of decay modes that ties nuclear processes to the configuration dimension in the Recognition Science framework. It completes the local certification step for radioactive decay types without introducing axioms or sorry placeholders. No downstream theorems currently depend on it, leaving open its integration into broader mass or forcing-chain calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.