module module

`IndisputableMonolith.Masses.RungConstructor.Proofs`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Masses.RungConstructor.Motif module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (43)

theorem match_lepton_e L13
theorem match_lepton_mu L15
theorem match_lepton_tau L17
theorem match_up_u L20
theorem match_up_c L22
theorem match_up_t L24
theorem match_down_d L27
theorem match_down_s L29
theorem match_down_b L31
theorem match_boson_W L34
theorem match_boson_Z L36
theorem match_boson_H L38
theorem match_rsbridge_rung_charged_leptons L41
theorem match_rsbridge_rung_up_quarks L48
theorem match_rsbridge_rung_down_quarks L55
theorem match_rsbridge_rung_neutrinos L63
theorem match_rsbridge_rung L70
theorem sdgt_lepton_e L79
theorem sdgt_lepton_mu L80
theorem sdgt_lepton_tau L81
theorem sdgt_up_u L84
theorem sdgt_up_c L85
theorem sdgt_up_t L86
theorem sdgt_down_d L89
theorem sdgt_down_s L90
theorem sdgt_down_b L91
theorem sdgt_nu1 L94
theorem sdgt_nu2 L95
theorem sdgt_nu3 L96
theorem sdgt_boson_W L99
theorem sdgt_boson_Z L100
theorem sdgt_boson_H L101
theorem sdgt_agrees_leptons L104
theorem sdgt_differs_up_c L111
theorem sdgt_differs_up_t L113
theorem sdgt_differs_down_s L115
theorem sdgt_differs_down_b L117
theorem sdgt_up_step_12 L121
theorem sdgt_up_step_23 L123
theorem sdgt_down_step_12 L125
theorem sdgt_down_step_23 L127
theorem sdgt_lepton_step_12 L129
theorem sdgt_lepton_step_23 L131