weakForceCert
plain-language theorem explainer
weakForceCert assembles the certificate for the weak nuclear force in Recognition Science by supplying the five decay types together with the exact Fibonacci value and bound for phi to the tenth. A physicist deriving Standard Model couplings from the phi-ladder would cite it when confirming that weak processes match configuration dimension five. The definition is a direct structure record that pulls the three fields from the sibling theorems weakDecayCount, phi10_fibonacci and phi10_gt_100.
Claim. The weak force certificate is the structure whose fields assert that the cardinality of weak decay types equals five, that $phi^{10}=55phi+34$, and that $phi^{10}>100$.
background
The module states that the Fermi constant takes the form $G_F=phi^{-10}/(8m_W^2)$ in RS-native units, with $phi^{10}$ fixed by the Fibonacci identity $55phi+34$ and with five canonical weak decays (beta-minus, beta-plus, electron capture, muon decay, tau decay) corresponding to configuration dimension five. WeakForceCert is the structure that packages these three assertions. Upstream, weakDecayCount proves the cardinality equals five by decision, phi10_fibonacci establishes the exact equality by successive nlinarith reductions starting from the square relation for phi, and phi10_gt_100 confirms the numerical bound by rewriting to the Fibonacci form and applying linarith.
proof idea
The definition is a direct one-line structure builder that assigns the five_types field to weakDecayCount, the phi10_val field to phi10_fibonacci, and the phi10_bound field to phi10_gt_100.
why it matters
This definition supplies the concrete certificate required for the weak nuclear force section of the A1 SM Depth. It verifies that the number of decay channels equals the five-dimensional configuration space and that the phi power satisfies the Fibonacci identity needed for the $G_F$ expression. No downstream uses are recorded, leaving open its later integration into larger mass or coupling derivations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.