module module

`IndisputableMonolith.RSBridge.ResidueData`

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 (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.AnchorPolicy module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (22)

def gap_lepton_theory L37
def gap_up_theory L41
def gap_down_theory L45
theorem lepton_Z_is_1332 L49
theorem up_Z_is_276 L50
theorem down_Z_is_24 L51
def cert_e L62
def cert_mu L69
def cert_tau L76
def cert_u L88
def cert_c L95
def cert_t L104
def cert_d L111
def cert_s L118
def cert_b L125
structure StabilityCert L136
def canonicalAnchorSpec L144
theorem display_identity_uses_gap L151
def certificateWithinTolerance L158
def leptonCerts L166
def quarkCerts L169
def allCerts L172