bViolationChannel_count
plain-language theorem explainer
The Recognition Science cosmology model enumerates exactly five canonical channels for baryon-number violation. Researchers verifying the phi-ladder trajectory for the baryon asymmetry eta_B would reference this enumeration to confirm completeness of the dynamical closure. The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance derived from the inductive definition.
Claim. The set of canonical B-violation channels has cardinality $5$, consisting of the sphaleron process, the electroweak process, the QCD process, the leptogenesis process, and the neutrino-mass process.
background
The module on baryogenesis from the phi-ladder defines the asymmetry evolution eta_B(T_k) = phi^(k-44) along temperature rungs T_k = T_GUT · phi^(-k), with the observed value reached at rung k=44. BViolationChannel is the inductive type whose five constructors list the processes enabling baryon-number violation: sphaleron, electroweak, QCD, leptogenesis, and neutrinoMass. The module states that this count equals configDim D and supplies the Fintype instance used for cardinality computation.
proof idea
The declaration is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the finite inductive type BViolationChannel.
why it matters
This theorem supplies the five_channels field inside baryogenesisCert, which certifies the complete trajectory via etaB_rung_ratio, etaB_complete at gap-45, and etaB_always_pos. It closes the dynamical part of the phi-ladder prediction eta_B = phi^(-44) and aligns with the eight-tick octave and T8 forcing to three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.