row_fermi_pred_lower
plain-language theorem explainer
The declaration shows that the Recognition Science Fermi constant prediction exceeds 1.16 times 10 to the minus 5 in GeV inverse squared. Electroweak phenomenologists would reference this bound when validating the interval against CODATA data. The proof unfolds the reciprocal definition, applies the division inequality under positivity of the denominator, and closes via numerical bounds on sqrt(2) together with linear arithmetic.
Claim. $1.16 times 10^{-5} < 1 / (sqrt(2) * v^2)$ in GeV^{-2}, where $v = 246$ is the canonical electroweak vacuum expectation value.
background
In the Fermi Constant Score Card module the predicted Fermi constant is defined as 1 over the product of sqrt(2) and the square of the canonical vacuum expectation value set to 246 GeV. This implements the electroweak identity G_F = 1 / (sqrt(2) v^2) in natural units. The module targets the interval (1.16e-5, 1.17e-5) that contains the measured CODATA value 1.1663787 times 10^{-5} GeV^{-2}. Upstream, vev_canonical_pos asserts positivity of the VEV while fermi_den_pos ensures the denominator is positive, permitting the reciprocal inequality.
proof idea
Unfold the definition of the predicted Fermi constant. Rewrite the target inequality via lt_div_iff_0 using fermi_den_pos. Introduce the bound sqrt(2) < 1.4143 from sqrt2_lt_14143. Establish the upper estimate on the denominator by substituting the canonical value and applying nlinarith. Verify by norm_num that the product of 1.16e-5 with this upper estimate is less than 1. Conclude the inequality by nlinarith.
why it matters
The lower bound combines with the matching upper bound to form row_fermi_pred_bracket, which places the Recognition Science prediction inside the interval containing the CODATA Fermi constant. It fills phase 1 row P1-C01 in the physical derivation plan. The construction relies on the canonical VEV scale; the full derivation of that scale from the phi-ladder remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.