DecayChannel
plain-language theorem explainer
The inductive definition enumerates the five canonical exotic decay channels whose lifetimes occupy successive rungs on the phi-ladder: alpha, beta-minus, beta-plus, electron capture, and spontaneous fission. Modelers of nuclear decay spectra in the Recognition framework cite this enumeration to anchor cardinality and ratio statements. The construction is a direct inductive type that automatically derives the Fintype instance needed for downstream decision procedures.
Claim. Let $D$ be the inductive type whose constructors are the five decay channels: alpha decay, beta-minus decay, beta-plus decay, electron capture, and spontaneous fission.
background
In the module on decay spectra from the phi-ladder, the inductive type lists the five channels whose lifetimes form a geometric sequence with common ratio phi. The phi-ladder itself encodes the self-similar scaling fixed point, with each rung separated by one step in the ladder. This enumeration parallels the vacuum-decay channel type in the companion module, which instead lists false-vacuum tunneling, Coleman-De Luccia, sphaleron, instanton, and thermal quench.
proof idea
The declaration is a direct inductive definition of the five constructors together with automatic derivation of DecidableEq, Repr, BEq, and Fintype. No lemmas or tactics are invoked; the Fintype instance is generated by the deriving clause to support immediate cardinality proofs.
why it matters
The definition supplies the finite set required by DecaySpectrumCert, which asserts five channels, phi ratios between consecutive lifetimes, and strict positivity. It mirrors the structure of VacuumDecayCert. Within the Recognition framework the five channels realize configDim D = 5 for the decay spectrum, consistent with the phi-ladder scaling that descends from the J-uniqueness and self-similar fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.