fermi_den_pos
The lemma establishes positivity of sqrt(2) times the square of the canonical electroweak VEV. Workers bounding the Recognition Science G_F prediction cite it to justify division in the interval comparison. The argument obtains square positivity from the VEV theorem then closes via linear arithmetic on the two positive constants.
claim$0 < √2 ⋅ v²$ where $v$ is the canonical RS electroweak vacuum expectation value (246 GeV).
background
The Fermi Constant Score Card module treats the natural-unit identity G_F = 1/(√2 v²) with the fixed canonical VEV v = 246 GeV, then proves the predicted interval (1.16 × 10^{-5}, 1.17 × 10^{-5}) GeV^{-2} contains the CODATA value. vev_canonical is the noncomputable definition equal to 246 whose positivity is already established by norm_num. sqrt2_pos records the elementary fact 0 < √2.
proof idea
One-line wrapper that first invokes sq_pos_of_ne_zero on vev_canonical_pos to obtain 0 < vev_canonical², then applies nlinarith to the pair (sqrt2_pos, hv).
why it matters in Recognition Science
The result supplies the denominator positivity required by row_fermi_pred_lower and row_fermi_pred_upper, which together certify the bracket around the RS G_F prediction. It therefore completes the arithmetic step of the P1-C01 row in the physical derivation plan. The module remains partial pending a first-principles derivation of the 246 GeV scale from the phi-ladder.
scope and limits
- Does not derive the numerical value 246 from the phi-ladder or Recognition forcing chain.
- Does not address conversion between natural units and SI/GeV conventions.
- Does not prove any electroweak Lagrangian or coupling unification.
formal statement (Lean)
61private theorem fermi_den_pos : 0 < Real.sqrt 2 * vev_canonical ^ 2 := by
proof body
Term-mode proof.
62 have hv : 0 < vev_canonical ^ 2 := sq_pos_of_ne_zero (ne_of_gt vev_canonical_pos)
63 nlinarith [sqrt2_pos, hv]
64