pith. machine review for the scientific record. sign in
lemma proved tactic proof

acceptable_quarks

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)

  79@[simp] lemma acceptable_quarks : acceptable quarksWitness 0 0 := by

proof body

Tactic-mode proof.

  80  refine And.intro ?hzs ?hchi
  81  · intro e he
  82    have hcases : e = u_entry ∨ e = d_entry ∨ e = s_entry ∨ e = c_entry ∨ e = b_entry ∨ e = t_entry := by
  83      simpa [quarksWitness] using he
  84    rcases hcases with h | h | h | h | h | h
  85    · subst h; simp [z_u_zero]
  86    · subst h; simp [z_d_zero]
  87    · subst h; simp [z_s_zero]
  88    · subst h; simp [z_c_zero]
  89    · subst h; simp [z_b_zero]
  90    · subst h; simp [z_t_zero]
  91  · simpa using chi2_quarks_zero
  92
  93/-! Boson witnesses (approximate PDG central values, GeV). -/

used by (1)

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

depends on (15)

Lean names referenced from this declaration's body.