Masses Fermi From Rsinputs Free Parameters In Gf Chain

The 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, its value is measured experimentally, most precisely from the muon lifetime. The Recognition Science framework's machine-checked library, a collection of formal theorems verified by a computer, contains a declaration that its own derivation of G_F uses zero free parameters.

The declaration, free_parameters_in_gf_chain, is a definition that simply states the number of free parameters in the derivation chain is 0. A companion theorem, gf_zero_free_params, proves this by reflexivity, meaning the statement is true by definition. This is a structural claim about the framework's internal derivation, not an empirical one. The derivation starts with three inputs: the Z boson mass (m_Z), the weak mixing angle (sin²θ_W), and the fine-structure constant (α_EM). The framework claims these are not fitted to experimental data but are themselves derived from its own foundational principles.

The chain is: (m_Z, sin²θ_W, α_EM) → v² → G_F = 1/(√2 · v²), where v is the Higgs vacuum expectation value. The framework proves a closed form for the inverse Fermi constant: G_F⁻¹ = √2 · z_pred² · (8−φ)/36 · αInv/π, where φ is the golden ratio and z_pred is the predicted Z mass. This expression is a theorem in the library, tagged THEOREM. The positivity of G_F is also proved. The framework's claim is that this entire chain, from its axioms to the Fermi constant, involves no adjustable parameters.

What the declaration does not claim is that the framework has measured G_F or that its value matches experiment. The library contains no theorem asserting numerical agreement with the measured value. The comparison against the Particle Data Group's measured value is an external empirical check, not a proved result. The declaration also does not claim that the inputs (m_Z, sin²θ_W, α_EM) are derived without any identification choices. The seed for α, for instance, is an identification, not a derived coupling. The zero-parameter claim is about the internal derivation structure, not about the framework's relation to external data.

In plain terms, the declaration establishes a formal property: within the framework's own system, the Fermi constant is not a free input but a consequence of other derived quantities. This is a statement about the framework's internal consistency and structure. It is not a statement about the physical world independent of the framework's assumptions. The framework's library proves the structural claim; the empirical validation is a separate, unproved matter.

/-- The number of free parameters in the G_F derivation chain. -/
def free_parameters_in_gf_chain : ℕ := 0

/-- 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 framework has measured the Fermi constant or that its value matches experiment. The inputs (m_Z, sin²θ_W, α_EM) are derived without any identification choices. The zero-parameter claim extends to the framework's relation to external data, only to its internal derivation structure.

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: