Pith. sign in
module module high

IndisputableMonolith.Masses.FermiFromRSInputs

show as:
view Lean formalization →

Derives the tree-level Fermi constant G_F (in MeV⁻²) from Recognition Science inputs alone, with no free electroweak parameters. Anyone checking the RS zero-parameter electroweak claim cites this module. The argument chains the RS-derived Z mass and weak angle into the VEV, then into G_F = 1/(√2 v²), and certifies that the free-parameter count is zero.

claimAt tree level, the inverse Fermi constant is fixed by RS inputs: $G_F^{-1} = \sqrt{2}\, v_{\mathrm{tree}}^2$, where $v_{\mathrm{tree}}^2$ is determined from the RS $Z$ mass, $\sin^2\theta_W$, and $\alpha^{-1}$ via $v^2 = m_Z^2\sin^2\theta_W\cos^2\theta_W\,\alpha^{-1}/\pi$. The module states a closed form for $G_F^{-1}$, positivity of $v_{\mathrm{tree}}^2$ and $G_F^{-1}$, and a certificate that the $G_F$ chain introduces zero free parameters.

background

Recognition Science fixes electroweak scales from the forcing chain rather than fitting $g$, $g'$, and $v$. Upstream, ElectroweakMasses places the $Z$ on rung 1 of the electroweak sector, giving $m_Z = 2\varphi^{51}/10^6$ MeV. VEVConsistency then removes $v$ as an independent input: the tree-level relation $v^2 = m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$ determines the Higgs vacuum expectation value from three RS-derived quantities.

The Fermi constant is the low-energy avatar of that VEV. In the Standard Model at tree level, $G_F = 1/(\sqrt{2} v^2)$. This module works in MeV$^{-2}$ and packages the inverse $G_F^{-1}$ so downstream scorecards can count parameters without re-deriving the chain.

Constants supplies the RS-native time quantum and related unit conventions used when converting ladder quantities into laboratory MeV units.

proof idea

Definition-and-certificate module, not a single deep proof. It defines the tree-level inverse Fermi constant from the RS VEV (via the standard $G_F = 1/(\sqrt{2} v^2)$ relation), records a closed-form expression, and proves positivity of $v_{\mathrm{tree}}^2$ and of $G_F^{-1}$ from upstream positivity of the electroweak inputs.

A short free-parameter ledger (free_parameters_in_gf_chain, gf_zero_free_params) shows every ingredient is already fixed by RS constants and prior mass modules. The bundle certificate FermiFromRSInputsCert and its holder fermiFromRSInputsCert_holds package those facts for import by the electroweak scorecard.

why it matters in Recognition Science

Closes the $G_F$ leg of the RS electroweak zero-parameter claim. Downstream, ElectroweakZeroParamScoreCard imports this module to argue that the four SM electroweak parameters $g$, $g'$, $v$, and $\lambda$ all descend from the forcing chain: $\alpha^{-1}$ from T5/T6/T7, $\sin^2\theta_W = (3-\varphi)/6$ from gauge embedding geometry, and $v$ (hence $G_F$) from the RS $Z$ mass and those couplings.

Without a certified tree-level $G_F$ from RS inputs, the scorecard could not claim that muon lifetime / Fermi coupling data are predictions rather than fits. This module is the mass-sector bridge between VEVConsistency and that physics-level audit.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (8)