gf_tree_inv
plain-language theorem explainer
Tree-level inverse Fermi constant in MeV⁻², built as √2 times the RS-derived electroweak VEV squared. Cited by anyone tracing G_F to Recognition Science inputs (m_Z, Weinberg angle, α). The body is a one-line product definition; closed-form and positivity theorems sit immediately downstream.
Claim. Define the tree-level inverse Fermi constant by $G_{F,\mathrm{tree}}^{-1} := \sqrt{2}\, v_{\mathrm{tree}}^2$, where $v_{\mathrm{tree}}^2$ is the RS-derived vacuum expectation value squared (in MeV$^2$).
background
The module links VEV consistency (P5a) to the Fermi constant. Standard electroweak tree-level algebra gives $G_F = 1/(\sqrt{2}, v^2)$, so the inverse is $\sqrt{2}, v^2$. The upstream quantity vev_tree_sq is the tree-level VEV squared from RS inputs: $v_{\mathrm{tree}}^2 = m_Z^2 \sin^2\theta_W \cos^2\theta_W ,\alpha^{-1}/\pi$, with all factors RS-derived.
VEVConsistency already proves the closed form $\sin^2\theta_W\cos^2\theta_W = (8-\varphi)/36$, so $v^2$ (and therefore $G_F^{-1}$) inherits a zero-free-parameter origin. Constants sit in RS-native units with $\alpha^{-1}$ in the usual band; masses and the VEV are carried in MeV-scale units for comparison with particle data.
proof idea
Pure definition: unfold to $\sqrt{2}$ times the upstream tree-level VEV squared. No tactics, no lemmas. Downstream theorems obtain the closed form by rewriting through the VEV closed-form identity, and positivity by multiplying the positivity of $\sqrt{2}$ with positivity of the VEV squared.
why it matters
Anchors the Fermi-from-RS chain: once $v^2$ is fixed by RS inputs, $G_F^{-1}$ is fixed with no extra parameters. It is the quantity named in the certificate structure (closed form, positivity, zero free parameters) and is the left-hand side of the closed-form identity $G_F^{-1} = \sqrt{2}, z^2,(8-\varphi)/36,\alpha^{-1}/\pi$.
That identity is the concrete landing of the module claim that $G_F$ is determined by $(m_Z,\sin^2\theta_W,\alpha_{\mathrm{EM}})$ through $v^2$. In the broader framework it sits on the mass/electroweak side of the forcing chain (phi-fixed Weinberg combination, alpha band), not on T5–T8 geometry directly, but it inherits the structural rigidity of those inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.