DecayChannel
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assign explicit lifetime values to any channel.
- Does not prove that consecutive lifetimes stand in ratio phi.
- Does not incorporate experimental branching ratios or nuclear data.
- Does not connect channels to the J-cost function or recognition composition law.
formal statement (Lean)
18inductive DecayChannel where
19 | alpha
20 | betaMinus
21 | betaPlus
22 | electronCapture
23 | spontaneousFission
24 deriving DecidableEq, Repr, BEq, Fintype
25