Masses Fermi From Rsinputs Gf Tree Inv Closed Form

The Fermi constant from first principles

The Fermi constant, usually written G_F, measures the strength of the weak nuclear force, the interaction responsible for radioactive beta decay. In the standard model of particle physics, it is not predicted from deeper principles; it is measured experimentally and then used as an input to other calculations. Its measured value is about 1.166 × 10⁻⁵ GeV⁻².

This framework derives G_F from a chain of its own derived quantities. The key theorem, gf_tree_inv_closed_form, states that the inverse Fermi constant equals √2 times the square of the predicted Z boson mass (z_pred), times a factor (8 − φ)/36 where φ is the golden ratio, times the inverse fine-structure constant α⁻¹, divided by π. In symbols: G_F⁻¹ = √2 · z_pred² · ((8 − φ)/36) · α⁻¹ / π.

The framework's library of machine-checked theorems proves this formula as a closed form, meaning it is a single explicit expression with no hidden numerical fitting. The same library proves that the number of free parameters in this derivation chain is exactly zero. This is the structural claim: G_F is not an independent constant in this account, but a consequence of the framework's derived values for the Z mass, the weak mixing angle, and the fine-structure constant.

In Recognition Science, the framework models the weak force's strength as flowing from the same structural source as other constants. The derivation is tree-level, meaning it uses the simplest Feynman diagram approximation and does not include quantum corrections. The framework proves the algebraic identity and the positivity of the result, but it does not claim that this tree-level value already matches the measured G_F to experimental precision, because loop corrections are not part of this theorem.

What this changes for the reader: the Fermi constant, usually a free input, becomes a derived output in this framework. The theorem does not claim to have measured anything, nor does it claim that the tree-level formula is the final word on G_F. It establishes a structural relationship, and leaves the numerical comparison against experiment as a separate empirical check.

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

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

/-- 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 tree-level formula is not claimed to match the measured Fermi constant to experimental precision, since loop corrections are absent. The framework does not claim to have measured the Fermi constant; it derives a structural expression from its own inputs. The theorem does not claim that the Fermi constant is a fundamental constant in the conventional sense; it is a derived quantity 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: