Masses Fermi From Rsinputs Vev Tree Sq Pos

A positive vacuum squared

The Fermi constant, G_F, governs the strength of the weak nuclear force, the interaction responsible for radioactive beta decay. Its measured value is about 1.166 × 10⁻⁵ GeV⁻². In the standard model, this constant is not fundamental; it is derived from the Higgs field's vacuum expectation value, a quantity that sets the scale of electroweak symmetry breaking. The vacuum expectation value, v, is defined by the relation G_F = 1/(√2 · v²), so a positive G_F requires a positive v².

The declaration vev_tree_sq_pos is a formal theorem in the framework's machine-checked library of formal theorems. It proves that the tree-level vacuum squared, v², is strictly greater than zero. The proof relies on a chain of established results: the predicted Z boson mass is positive, the combination (8 − φ)/36 is positive, the inverse fine-structure constant is positive, and π is positive. Each factor in the expression for v² is positive, so their product is positive.

This positivity result is a consistency check, not a numerical prediction. It does not say what the value of v² is, only that it is not zero or negative. A zero or negative vacuum squared would signal a broken or unphysical electroweak sector. The theorem's significance is that it rules out such pathological cases within the framework's derivation, ensuring that the Fermi constant derived from this vacuum is a real, positive quantity.

In Recognition Science, this theorem is part of a larger claim that the Fermi constant is determined by structural inputs with zero free parameters. The framework models the Fermi constant as G_F = π · α / (√2 · m_Z² · sin²θ_W · cos²θ_W), where the sin²θ_W · cos²θ_W product is the closed form (8 − φ)/36. This is a definitional choice within the framework, not a measurement. The theorem vev_tree_sq_pos ensures that this derived quantity is well-defined and positive.

What the theorem does not claim is equally important. It does not prove that the framework's predicted value of G_F matches the measured value; that would require comparing the numerical output to experimental data, which is an empirical check, not a theorem. It also does not address higher-order quantum corrections, which would modify the tree-level relation. The theorem is a statement about the mathematical consistency of the framework's internal derivation, not a claim about the physical world beyond that derivation.

/-- The VEV squared is positive (since z_pred > 0, (8-φ)/36 > 0, αInv > 0, π > 0). -/
theorem vev_tree_sq_pos : 0 < vev_tree_sq := by
  unfold vev_tree_sq
  have hz : 0 < z_pred := by linarith [z_mass_bounds.1]
  have hs2 : 0 < sin2_theta_W_rs := sin2_theta_positive
  have hc2 : 0 < cos2_theta_W_rs := cos2_theta_positive
  have hα : 0 < alphaInv := by linarith [Numerics.alphaInv_gt]
  have hπ : 0 < Real.pi := Real.pi_pos
  have hz2 : 0 < z_pred ^ 2 := sq_pos_of_ne_zero (ne_of_gt hz)
  have hsc : 0 < sin2_theta_W_rs * cos2_theta_W_rs := mul_pos hs2 hc2
  have h1 : 0 < z_pred ^ 2 * sin2_theta_W_rs := mul_pos hz2 hs2
  have h2 : 0 < z_pred ^ 2 * sin2_theta_W_rs * cos2_theta_W_rs := mul_pos h1 hc2
  have h3 : 0 < z_pred ^ 2 * sin2_theta_W_rs * cos2_theta_W_rs * alphaInv := mul_pos h2 hα
  exact div_pos h3 hπ

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

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

What this page does not claim

The theorem does not prove that the framework's predicted Fermi constant matches the measured value. The theorem does not address quantum corrections beyond the tree level. The theorem does not establish the numerical value of the vacuum expectation itself.

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: