Constants Fermi Constant Score Card Row Fermi Pred Upper

The Fermi bracket

The Fermi constant, usually written G_F, sets the strength of the weak nuclear force, the interaction responsible for radioactive beta decay. In natural units, where the reduced Planck constant and the speed of light are set to one, the measured value from CODATA and the Particle Data Group is 1.1663787 x 10^-5 GeV^-2. The Recognition Science library contains a machine-checked theorem, row_fermi_pred_upper, that proves this predicted value is less than 1.17 x 10^-5 GeV^-2. A companion theorem proves it is greater than 1.16 x 10^-5 GeV^-2, so together they place the prediction inside a narrow interval that contains the measured value.

The prediction itself comes from a standard electroweak identity: G_F equals one divided by the square root of two times the square of the Higgs vacuum expectation value, v. The framework chooses the canonical value v = 246 GeV, a number familiar from conventional particle physics. Substituting that value into the identity yields the bracket. The two theorems, row_fermi_pred_lower and row_fermi_pred_upper, are proved with no unproven assumptions and no axioms beyond the standard logical ones, and they combine into a single certificate that also records the measured value sits inside the same bracket.

In Recognition Science, the framework models the electroweak vacuum expectation value as a derived quantity, not a free parameter. The theorem row_fermi_pred_upper is a step in that program, but it is explicitly marked as a partial result. The value 246 GeV is the canonical display value, and the fully derived bridge from the framework's fundamental constants to that GeV scale remains an open problem. The theorem proves an inequality about a number defined using 246 GeV; it does not prove that 246 GeV itself is forced by the framework.

What the bracket changes is the status of the Fermi constant prediction. The measured value landing inside the proved interval is a concrete, checkable agreement between the framework's chosen electroweak surface and experiment. The falsifier is equally concrete: if a future measurement of G_F fell outside the interval, or if a future derivation of the VEV failed to recover the 246 GeV scale, the prediction would be refuted. Until that VEV bridge is built, the row remains a partial theorem, a proved inequality resting on an identified but not yet derived input.

/-- CODATA/PDG Fermi constant in GeV^-2. -/
def row_fermi_codata : ℝ := 1.1663787e-5

theorem row_fermi_pred_upper :
    row_fermi_pred < (1.17e-5 : ℝ) := by
  unfold row_fermi_pred
  rw [div_lt_iff₀ fermi_den_pos]
  have hs : (1.4142 : ℝ) < Real.sqrt 2 := sqrt2_gt_14142
  have hden :
      (1.4142 : ℝ) * (246 : ℝ) ^ 2 < Real.sqrt 2 * vev_canonical ^ 2 := by
    have hv : vev_canonical = (246 : ℝ) := rfl
    rw [hv]
    nlinarith
  have hnum : 1 < (1.17e-5 : ℝ) * ((1.4142 : ℝ) * (246 : ℝ) ^ 2) := by
    norm_num
  nlinarith

theorem row_fermi_pred_eq :
    row_fermi_pred = 1 / (Real.sqrt 2 * vev_canonical ^ 2) := rfl

theorem row_fermi_codata_in_bracket :
    (1.16e-5 : ℝ) < row_fermi_codata ∧ row_fermi_codata < (1.17e-5 : ℝ) := by
  unfold row_fermi_codata
  constructor <;> norm_num

What this page does not claim

The theorem does not prove that 246 GeV is derived from more fundamental framework constants. The theorem does not claim the Fermi constant is predicted from first principles without any input. The theorem does not establish the Fermi constant's value beyond the stated bracket of 1.16 to 1.17 x 10^-5 GeV^-2.

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/Constants/FermiConstantScoreCard.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: