decayChannel_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive lifetimes or rung assignments from the J-cost equation.
- Does not prove uniqueness of these five channels outside the given enumeration.
- Does not address branching ratios or stability criteria.
- Does not connect the count to spatial dimensions D = 3 or the eight-tick octave.
Lean usage
example : Fintype.card DecayChannel = 5 := decayChannel_countformal statement (Lean)
26theorem decayChannel_count : Fintype.card DecayChannel = 5 := by decide
proof body
27