`sdgt_up_u`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.RungConstructor.Proofs
domain: Masses
line: 84 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.RungConstructor.Proofs on GitHub at line 84.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

compute_rung_sdgt IndisputableMonolith.Masses.RungConstructor.Motif

formal source

  81theorem sdgt_lepton_tau : compute_rung_sdgt (.fermion .tau) = 19 := by rfl
  82
  83/-- SDGT: Up-quark rungs {4, 17, 28} from steps {V+F-C=13, E_pass=11}. -/
  84theorem sdgt_up_u : compute_rung_sdgt (.fermion .u) = 4 := by rfl
  85theorem sdgt_up_c : compute_rung_sdgt (.fermion .c) = 17 := by rfl
  86theorem sdgt_up_t : compute_rung_sdgt (.fermion .t) = 28 := by rfl
  87
  88/-- SDGT: Down-quark rungs {4, 10, 18} from steps {F=6, V=8}. -/
  89theorem sdgt_down_d : compute_rung_sdgt (.fermion .d) = 4 := by rfl
  90theorem sdgt_down_s : compute_rung_sdgt (.fermion .s) = 10 := by rfl
  91theorem sdgt_down_b : compute_rung_sdgt (.fermion .b) = 18 := by rfl
  92
  93/-- SDGT: Neutrinos unchanged. -/
  94theorem sdgt_nu1 : compute_rung_sdgt (.fermion .nu1) = 0 := by rfl
  95theorem sdgt_nu2 : compute_rung_sdgt (.fermion .nu2) = 11 := by rfl
  96theorem sdgt_nu3 : compute_rung_sdgt (.fermion .nu3) = 19 := by rfl
  97
  98/-- SDGT: Bosons unchanged. -/
  99theorem sdgt_boson_W : compute_rung_sdgt .W = 1 := by rfl
 100theorem sdgt_boson_Z : compute_rung_sdgt .Z = 1 := by rfl
 101theorem sdgt_boson_H : compute_rung_sdgt .H = 1 := by rfl
 102
 103/-- SDGT agrees with legacy for leptons, neutrinos, and bosons. -/
 104theorem sdgt_agrees_leptons :
 105    compute_rung_sdgt (.fermion .e) = compute_rung (.fermion .e) ∧
 106    compute_rung_sdgt (.fermion .mu) = compute_rung (.fermion .mu) ∧
 107    compute_rung_sdgt (.fermion .tau) = compute_rung (.fermion .tau) :=
 108  ⟨rfl, rfl, rfl⟩
 109
 110/-- SDGT DIFFERS from legacy for quarks (the whole point!). -/
 111theorem sdgt_differs_up_c : compute_rung_sdgt (.fermion .c) ≠ compute_rung (.fermion .c) := by
 112  decide
 113theorem sdgt_differs_up_t : compute_rung_sdgt (.fermion .t) ≠ compute_rung (.fermion .t) := by
 114  decide

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.