lemma proved term proof

`res_nu2_simp`

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

formal statement (Lean)

 173lemma res_nu2_simp : res_nu2 = (-231 : ℚ) / 4 := by

Term-mode proof.

 174  unfold res_nu2
 175  -- res_nu3 = -217/4, spacing = 7/2 = 14/4
 176  simp [res_nu3_simp, nu_spacing_eq]
 177  norm_num
 178

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

nu1_frac_pred_bounds in IndisputableMonolith.Physics.NeutrinoSector decl_use
nu2_frac_pred_bounds in IndisputableMonolith.Physics.NeutrinoSector decl_use
res_nu1_simp in IndisputableMonolith.Physics.NeutrinoSector decl_use

Lean names referenced from this declaration's body.