WeakDecayType
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive branching ratios or lifetimes for any channel.
- Does not map individual decays onto specific phi-ladder mass rungs.
- Does not compute the numerical value of the Fermi constant.
- Does not incorporate neutrino flavor mixing or oscillation data.
formal statement (Lean)
22inductive WeakDecayType where
23 | betaMinus | betaPlus | electronCapture | muonDecay | tauDecay
24 deriving DecidableEq, Repr, BEq, Fintype
25