WeakDecayType
plain-language theorem explainer
Recognition Science models the weak nuclear force through an enumeration of five canonical decay channels that fix the configuration dimension at D equals 5. A physicist deriving Fermi-constant relations or phi-ladder particle counts from RS would cite this definition when establishing the weak-force structure. The declaration is a direct inductive enumeration that automatically derives decidability, representation, equality, and finiteness instances.
Claim. The weak decay types are the five processes: $beta^-$ decay, $beta^+$ decay, electron capture, muon decay, and tau decay.
background
The module treats the weak nuclear force in 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. Five canonical decay channels are identified with the configuration dimension D equals 5. No upstream lemmas are required; the definition stands alone as the type whose cardinality is later asserted to be five.
proof idea
The declaration is a direct inductive definition enumerating the five constructors betaMinus, betaPlus, electronCapture, muonDecay, and tauDecay, with derived instances for DecidableEq, Repr, BEq, and Fintype supplied automatically by Lean.
why it matters
This definition supplies the type whose cardinality is proved equal to 5 in the downstream theorem weakDecayCount and is required by the structure WeakForceCert that also records the identity $phi^{10} = 55 phi + 34$. It therefore realizes the statement that the five decay modes equal configDim D equals 5 in the A1 SM Depth treatment of the weak force. The enumeration anchors the RS-native constants and the phi-ladder counting that appear throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.