`match_lepton_tau`

proved

show as: view math explainer →

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

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

  14
  15theorem match_lepton_mu : compute_rung (.fermion .mu) = 13 := by rfl
  16
  17theorem match_lepton_tau : compute_rung (.fermion .tau) = 19 := by rfl
  18
  19/-- Proof that the rung constructor reproduces the up-quark table. -/
  20theorem match_up_u : compute_rung (.fermion .u) = 4 := by rfl
  21
  22theorem match_up_c : compute_rung (.fermion .c) = 15 := by rfl
  23
  24theorem match_up_t : compute_rung (.fermion .t) = 21 := by rfl
  25
  26/-- Proof that the rung constructor reproduces the down-quark table. -/
  27theorem match_down_d : compute_rung (.fermion .d) = 4 := by rfl
  28
  29theorem match_down_s : compute_rung (.fermion .s) = 15 := by rfl
  30
  31theorem match_down_b : compute_rung (.fermion .b) = 21 := by rfl
  32
  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. -/

papers checked against this theorem

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