weakDecayCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive numerical decay rates or branching ratios.
- Does not address mixing angles or CP violation.
- Does not compute the explicit value of the Fermi constant.
- Does not extend to strong or electromagnetic channels.
Lean usage
weakForceCert.five_typesformal statement (Lean)
26theorem weakDecayCount : Fintype.card WeakDecayType = 5 := by decide
proof body
Term-mode proof.
27
28/-- φ^10 = 55φ + 34 (Fibonacci). -/