pith. machine review for the scientific record. sign in
theorem proved term proof

quarkAbsoluteBridgeScoreCardCert_holds

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

formal statement (Lean)

 160theorem quarkAbsoluteBridgeScoreCardCert_holds :
 161    Nonempty QuarkAbsoluteBridgeScoreCardCert :=

proof body

Term-mode proof.

 162  ⟨{ charm_up_ratio_agrees := row_charm_up_structural_anchor_agree
 163     top_charm_ratio_agrees := row_top_charm_structural_anchor_agree
 164     strange_down_anchor_ratio := row_anchor_strange_down_ratio_rpow
 165     bottom_strange_anchor_ratio := row_anchor_bottom_strange_ratio_rpow
 166     residual_named := row_absolute_quark_bridge_residual_is_named }⟩
 167
 168end
 169
 170end IndisputableMonolith.Masses.QuarkAbsoluteBridgeScoreCard

depends on (6)

Lean names referenced from this declaration's body.