`sdgt_boson_H`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.RungConstructor.Proofs
domain: Masses
line: 101 · 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 101.

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

formal source

  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
 115theorem sdgt_differs_down_s : compute_rung_sdgt (.fermion .s) ≠ compute_rung (.fermion .s) := by
 116  decide
 117theorem sdgt_differs_down_b : compute_rung_sdgt (.fermion .b) ≠ compute_rung (.fermion .b) := by
 118  decide
 119
 120/-- SDGT generation step verification: the steps match the cyclic chain. -/
 121theorem sdgt_up_step_12 : compute_rung_sdgt (.fermion .c) - compute_rung_sdgt (.fermion .u) = 13 := by
 122  native_decide
 123theorem sdgt_up_step_23 : compute_rung_sdgt (.fermion .t) - compute_rung_sdgt (.fermion .c) = 11 := by
 124  native_decide
 125theorem sdgt_down_step_12 : compute_rung_sdgt (.fermion .s) - compute_rung_sdgt (.fermion .d) = 6 := by
 126  native_decide
 127theorem sdgt_down_step_23 : compute_rung_sdgt (.fermion .b) - compute_rung_sdgt (.fermion .s) = 8 := by
 128  native_decide
 129theorem sdgt_lepton_step_12 : compute_rung_sdgt (.fermion .mu) - compute_rung_sdgt (.fermion .e) = 11 := by
 130  native_decide
 131theorem sdgt_lepton_step_23 : compute_rung_sdgt (.fermion .tau) - compute_rung_sdgt (.fermion .mu) = 6 := by

papers checked against this theorem

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