weakDecayCount
plain-language theorem explainer
The theorem fixes the number of weak nuclear decay channels at five in the Recognition Science model, matching the configuration dimension for the weak sector. A physicist deriving the Fermi constant from the phi-ladder would cite this count to confirm the discrete channel structure. The proof is a one-line decision that enumerates the finite inductive type.
Claim. The cardinality of the set of weak decay types is five: $|W| = 5$ where $W = $ {beta-minus, beta-plus, electron capture, muon decay, tau decay}.
background
The module derives the weak force from Recognition Science by expressing the Fermi constant as $G_F = phi^{-10}/(8 m_W^2)$ in native units, with $phi^{10} = 55 phi + 34$ from the Fibonacci relation. WeakDecayType is the inductive enumeration of the five canonical processes that realizes configDim D = 5 for this sector. The upstream inductive definition supplies the complete list of constructors together with its Fintype instance.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card goal on the enumerated inductive type.
why it matters
This supplies the five_types field inside the weakForceCert definition that certifies the RS expression for $G_F$. It anchors the discrete channel count to the eight-tick octave and D = 3 spatial dimensions of the forcing chain. The result closes the weak-sector enumeration with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.