Masses Fermi From Rsinputs Gf Tree Inv

The Fermi constant from RS inputs

The Fermi constant G_F sets the strength of the weak nuclear force, the interaction behind beta decay. In the standard model of particle physics, it is not a free parameter but is related to the masses of the W and Z bosons and the weak mixing angle. The Recognition Science (RS) framework, in its module FermiFromRSInputs, proves a tree-level formula for the inverse Fermi constant, G_F⁻¹, in terms of three inputs: the Z boson mass m_Z, the weak mixing angle θ_W, and the fine-structure constant α. The derivation is a chain of equalities, each step checked by the machine-checked library of formal theorems, ending in a closed form that uses the RS-derived identity sin²θ_W · cos²θ_W = (8 - φ)/36, where φ is the golden ratio.

The central result is the theorem gf_tree_inv_closed_form, which states that G_F⁻¹ = √2 · z_pred² · ((8 - φ)/36) · α⁻¹/π. Here z_pred is the RS-predicted Z mass, αInv is the inverse fine-structure constant, and the expression is a direct consequence of the vacuum expectation value (VEV) consistency result. The framework also proves that G_F⁻¹ is positive and that the number of free parameters in the chain is exactly zero. This means that, within the framework, the Fermi constant is not fitted but is determined by the same structural inputs that fix the electroweak scale. The declaration gf_tree_inv is the definition of this quantity; the theorems prove its closed form and positivity.

The framework does not claim that this tree-level relation is the full quantum-corrected value. It is a tree-level formula, meaning it ignores radiative corrections from loop diagrams. The measured Fermi constant, from muon decay, is about 1.166 × 10⁻⁵ GeV⁻², but this derivation does not compare against that value with an error budget. The zero-free-parameter claim is about the chain of definitions, not about agreement with experiment. The framework also does not claim that the inputs themselves are derived from scratch; m_Z, sin²θ_W, and α are taken as measured inputs, even though they are called RS-derived in the docstring. The theorem proves an algebraic identity, not a physical prediction that has been tested against PDG data.

What the declaration establishes is a structural fact: given the framework's internal definitions and the proved VEV consistency, the Fermi constant has a closed-form expression with no free parameters. This is a consistency result within the framework, not a new measurement or a replacement for the standard model. The practical consequence is that the weak force's strength is tied to the same golden-ratio structure that appears elsewhere in RS, but that connection is a formal derivation, not an empirical confirmation.

/-- 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

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

What this page does not claim

This derivation is tree-level and does not include quantum loop corrections. The inputs m_Z, sin²θ_W, and α are taken as measured, not derived from first principles in this module. No comparison to the measured Fermi constant with an error budget is made here.

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: