Masses Fermi From Rsinputs Gf Zero Free Params

The Fermi constant's zero-parameter claim

The Fermi constant, G_F, is the coupling strength of the weak nuclear force, the interaction responsible for radioactive beta decay. In the standard model of particle physics, it is not a derived quantity but a measured input. Recognition Science (RS) attempts to change that status. Its machine-checked library of formal theorems contains a result, gf_zero_free_params, which states that the number of free parameters in its derivation chain for G_F is exactly zero.

The derivation chain starts from RS-derived inputs: the Z boson mass m_Z, the weak mixing angle sin²θ_W, and the fine-structure constant α_EM. From these, the theory computes the Higgs vacuum expectation value v², and then G_F = 1/(√2 · v²). The theorem gf_tree_inv_closed_form proves the closed-form expression G_F⁻¹ = √2 · z² · (8-φ)/36 · α⁻¹/π, where φ is the golden ratio and z is an RS-derived scale. The zero-parameter claim is a statement about the formal derivation: no input in this chain is a fitted constant.

What the theorem does not claim is that this expression numerically matches the measured Fermi constant. The library proves the algebraic identity and the positivity of the result, but it does not prove that the RS-derived value equals the experimentally determined value to within measurement uncertainty. That comparison is an empirical check, not a theorem. The formal result establishes a structural origin, not an experimental validation.

The distinction matters because the Fermi constant is one of the most precisely measured quantities in physics. The RS claim is that its value is not arbitrary but forced by the framework's internal consistency. Whether that forced value agrees with experiment is a separate question that the formal library does not address. The declaration gf_zero_free_params is a certificate of internal structure, not a certificate of agreement with nature.

/-- All RS inputs in the G_F chain are structural. -/
theorem gf_zero_free_params :
    free_parameters_in_gf_chain = 0 := rfl

/-- G_F expressed through the sin²·cos² closed form.
    G_F⁻¹ = √2 · z² · (8-φ)/36 · α⁻¹/π. -/
theorem gf_tree_inv_closed_form :
    gf_tree_inv = Real.sqrt 2 *
      (ElectroweakMasses.z_pred ^ 2 * ((8 - phi) / 36) * alphaInv / Real.pi) := by
  unfold gf_tree_inv
  rw [vev_tree_sq_closed_form]

/-- G_F⁻¹ is positive (since it is √2 times a positive quantity). -/
theorem gf_tree_inv_pos : 0 < gf_tree_inv := by
  unfold gf_tree_inv
  exact mul_pos (Real.sqrt_pos.mpr (by norm_num)) vev_tree_sq_pos

What this page does not claim

The theorem does not claim numerical agreement with the measured Fermi constant. The zero-parameter count does not include the identification of the seed 44π used elsewhere in the framework. The derivation is tree-level and does not account for radiative corrections.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/FermiFromRSInputs.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: