module module

`IndisputableMonolith.Masses.QuarkAnchorDerivation`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Masses.RSBridge.Anchor module_import

declarations in this module (15)

def charm_anchor_native L21
def bottom_anchor_native L22
def top_anchor_native L23
theorem charm_anchor_eq_massAtAnchor L25
theorem bottom_anchor_eq_massAtAnchor L28
theorem top_anchor_eq_massAtAnchor L31
theorem charm_rung_eq L34
theorem bottom_rung_eq L35
theorem top_rung_eq L36
theorem charm_Z_eq L38
theorem bottom_Z_eq L39
theorem top_Z_eq L40
theorem heavy_anchor_positive L42
structure QuarkAnchorDerivationCert L53
theorem quarkAnchorDerivationCert_holds L64