`match_boson_Z`

proved

show as: view math explainer →

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

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

  33/-- Proof that the rung constructor reproduces the boson table. -/
  34theorem match_boson_W : compute_rung .W = 1 := by rfl
  35
  36theorem match_boson_Z : compute_rung .Z = 1 := by rfl
  37
  38theorem match_boson_H : compute_rung .H = 1 := by rfl
  39
  40/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for charged leptons. -/
  41theorem match_rsbridge_rung_charged_leptons :
  42    compute_rung (.fermion .e) = RSBridge.rung .e ∧
  43    compute_rung (.fermion .mu) = RSBridge.rung .mu ∧
  44    compute_rung (.fermion .tau) = RSBridge.rung .tau :=
  45  ⟨rfl, rfl, rfl⟩
  46
  47/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for up-type quarks. -/
  48theorem match_rsbridge_rung_up_quarks :
  49    compute_rung (.fermion .u) = RSBridge.rung .u ∧
  50    compute_rung (.fermion .c) = RSBridge.rung .c ∧
  51    compute_rung (.fermion .t) = RSBridge.rung .t :=
  52  ⟨rfl, rfl, rfl⟩
  53
  54/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for down-type quarks. -/
  55theorem match_rsbridge_rung_down_quarks :
  56    compute_rung (.fermion .d) = RSBridge.rung .d ∧
  57    compute_rung (.fermion .s) = RSBridge.rung .s ∧
  58    compute_rung (.fermion .b) = RSBridge.rung .b :=
  59  ⟨rfl, rfl, rfl⟩
  60
  61/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for neutrinos.
  62    Neutrinos have baseline 0 (due to Z=0) and a different gen-2 step (+8 vs +6). -/
  63theorem match_rsbridge_rung_neutrinos :
  64    compute_rung (.fermion .nu1) = RSBridge.rung .nu1 ∧
  65    compute_rung (.fermion .nu2) = RSBridge.rung .nu2 ∧
  66    compute_rung (.fermion .nu3) = RSBridge.rung .nu3 :=

papers checked against this theorem

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