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

pmns_theta23_match

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)

 133theorem pmns_theta23_match :
 134    abs (sin2_theta23_pred - 0.546) < 0.01 := by

proof body

Term-mode proof.

 135  unfold sin2_theta23_pred atmospheric_weight atmospheric_radiative_correction
 136  -- 0.5 + 6*alpha ≈ 0.5 + 0.0438 = 0.5438. PDG 2022: 0.546(21)
 137  -- Use alpha bounds
 138  have h_alpha_lo := CKMGeometry.alpha_lower_bound
 139  have h_alpha_hi := CKMGeometry.alpha_upper_bound
 140  rw [abs_lt]
 141  constructor <;> linarith
 142
 143/-- Atmospheric radiative correction coefficient (6) is forced by cube topology. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.