decayChannel_count
plain-language theorem explainer
decayChannel_count fixes the number of exotic decay channels at five in the phi-ladder model. It is referenced by the decay spectrum certificate to anchor the channel count before assigning lifetimes on successive rungs. The proof is a direct decision procedure on the inductive type with five constructors.
Claim. The finite type of decay channels has cardinality five, where the channels are alpha decay, beta-minus decay, beta-plus decay, electron capture, and spontaneous fission.
background
The module sets the decay spectrum from the phi-ladder with five canonical exotic channels (configDim D = 5). Each lifetime sits one rung up the phi-ladder. The upstream inductive definition enumerates alpha, betaMinus, betaPlus, electronCapture, spontaneousFission and derives Fintype, DecidableEq. A parallel enumeration with different channels appears in the vacuum decay module and yields the same cardinality theorem.
proof idea
The proof is a one-line wrapper that applies the decidable Fintype.card computation to the inductive type with exactly five constructors.
why it matters
This count populates the five_channels field of decaySpectrumCert, which also requires lifetime_ratio and lifetime_pos. It supplies the fixed channel count for the Recognition framework's phi-ladder decay spectrum, consistent with the module's claim of zero sorrys. The result parallels the vacuum decay certificate in the sibling module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.