pith. machine review for the scientific record. sign in
theorem proved term proof

simple_geometric_ratio

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 132theorem simple_geometric_ratio : geometricMixing ⟨3, 1, 8⟩ = 1/4 := by

proof body

Term-mode proof.

 133  unfold geometricMixing
 134  norm_num
 135
 136/-- The φ-correction to the geometric ratio.
 137
 138    sin²(θ_W) = 1/4 × (1 - ε)
 139    where ε = (φ - 1) / (12φ) ≈ 0.032
 140
 141    This gives: 0.25 × (1 - 0.032) = 0.242 × 0.968 = 0.234
 142
 143    Still a bit too large, but capturing the right structure. -/

depends on (2)

Lean names referenced from this declaration's body.