Masses Fermi From Rsinputs

The Fermi constant from RS inputs

The Fermi constant G_F is a number in particle physics that sets the strength of the weak nuclear force, the force responsible for radioactive beta decay. It is measured with great precision: the CODATA 2022 value is 1.1663788(6) × 10⁻⁵ GeV⁻². In the standard model, G_F is not a fundamental constant in its own right; it is related to the Higgs field's vacuum expectation value (VEV), the constant background value the Higgs field takes everywhere in space. The tree-level relation is G_F = 1/(√2 · v²), where v is that VEV.

This framework takes that standard relation and plugs in values for v² that come from within the Recognition Science framework. The framework is built on a ledger, a discrete record of recognition events, and its central theorem forces a specific cost function. From that, a chain of results derives quantities like the Z boson mass, the weak mixing angle, and the fine-structure constant. The framework shows that v², and therefore G_F, can be written entirely in terms of these framework-derived inputs: the predicted Z mass z_pred, the golden ratio φ, and the inverse fine-structure constant αInv.

The key result is a closed form: G_F⁻¹ = √2 · z_pred² · (8 - φ)/36 · αInv/π. This is a theorem in the machine-checked library, proved with no axioms beyond the standard logical ones. It is not a numerical fit; it is a symbolic identity that follows from the framework's earlier results. The framework also proves that this quantity is positive, which is physically required, and that the number of free parameters in the entire derivation chain is exactly zero.

In Recognition Science, this is a structural result. The framework models the weak force's strength as a consequence of the same underlying recognition cost that forces other constants. The framework does not measure G_F; it derives a formula for it. The comparison to the measured value is an empirical check, not part of the theorem. The point is that within this framework, the Fermi constant is not an independent input but a derived output, tied to the same source as the Z mass and the fine-structure constant.

structure FermiFromRSInputsCert where
  closed_form :
    gf_tree_inv = Real.sqrt 2 *
      (z_pred ^ 2 * ((8 - phi) / 36) * alphaInv / Real.pi)
  positivity : 0 < gf_tree_inv
  zero_params : free_parameters_in_gf_chain = 0

/-- Tree-level G_F from RS inputs (in MeV⁻²). -/
noncomputable def gf_tree_inv : ℝ :=
  Real.sqrt 2 * vev_tree_sq

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

The framework does not measure the Fermi constant; it derives a symbolic formula for it. The framework does not claim to have derived the numerical value of G_F from scratch without any input; it uses z_pred, φ, and αInv as its inputs. This result does not prove that the standard model's relation between G_F and the VEV is correct; it assumes that tree-level relation.

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: