sqrt2_pos
plain-language theorem explainer
The declaration establishes that the square root of two is strictly positive in the reals. It is invoked inside the proof that the denominator of the Fermi constant expression remains positive. The argument is a one-line wrapper around the Mathlib lemma for square-root positivity, discharged by a numeric normalization check.
Claim. $0 < 2^{1/2}$
background
The Fermi Constant Score Card module targets the natural-unit electroweak identity G_F = 1 / (sqrt(2) * v^2) with the canonical vev_canonical = 246 GeV. It verifies that the Recognition Science prediction lies inside the interval (1.16e-5, 1.17e-5) GeV^{-2} that contains the CODATA value. The module imports Mathlib for real analysis and ElectroweakVEVStructure for the vev definition; the present helper supplies the required positivity fact for the denominator.
proof idea
The proof applies Real.sqrt_pos.mpr to the proposition 2 > 0, which norm_num discharges at once.
why it matters
fermi_den_pos applies this fact together with the positivity of vev_canonical^2 to conclude that the denominator is positive, completing the interval check for G_F in the phase-1 row P1-C01. The result therefore supports the partial theorem for the Fermi constant inside the constants domain. The remaining open question is the full SI/GeV bridge that would derive the 246 GeV scale from the phi-ladder without canonical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.