DecayChannel
DecayChannel enumerates the five canonical vacuum decay channels in the Recognition Science model: false-vacuum tunneling, Coleman-de Luccia bubble, sphaleron, instanton, and thermal quench. Physicists modeling vacuum stability or phi-ladder tunneling cite this enumeration to set configDim D equal to 5. The declaration is a direct inductive construction that derives DecidableEq, Repr, BEq, and Fintype for immediate use in cardinality and certification results.
claimAn inductive type whose five constructors are false-vacuum tunneling, Coleman-de Luccia bubble nucleation, sphaleron transition, instanton, and thermal quench.
background
The module introduces vacuum decay from J-cost with five canonical channels identified with configDim D = 5. Tunneling action is computed on the phi-ladder. The upstream inductive type in DecaySpectrumFromPhiLadder supplies the parallel five-channel enumeration for nuclear decays (alpha, betaMinus, betaPlus, electronCapture, spontaneousFission), establishing the same finite cardinality pattern.
proof idea
Direct inductive definition that lists the five constructors and derives the required type classes (DecidableEq, Repr, BEq, Fintype) with no proof body or tactics.
why it matters in Recognition Science
Supplies the channel list required by the downstream VacuumDecayCert structure, which asserts Fintype.card equals 5 together with phi ratios and positivity for tunnelingAction. It mirrors the DecayChannel and decayChannel_count results in DecaySpectrumFromPhiLadder, closing the enumeration step that supports phi-ladder tunneling within the Recognition framework.
scope and limits
- Does not compute explicit tunneling action values.
- Does not prove vacuum stability or instability.
- Does not relate channels to the J-cost equation or RCL.
- Does not address spatial dimension D = 3 or the eight-tick octave.
formal statement (Lean)
19inductive DecayChannel where
20 | falseVacuumTunneling
21 | colemanDeLuccia
22 | sphaleron
23 | instanton
24 | thermalQuench
25 deriving DecidableEq, Repr, BEq, Fintype
26