module module

`IndisputableMonolith.CrossDomain.ProductRecognitionLattice`

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

declarations in this module (24)

theorem five_pow_2 L30
theorem five_pow_3 L31
theorem five_pow_4 L32
theorem five_pow_5 L33
theorem five_pow_6 L34
theorem five_pow_7 L35
theorem five_pow_8 L36
theorem five_six_lt_two_fourteen L41
theorem five_five_lt_two_thirteen L44
theorem five_four_lt_two_ten L47
theorem five_three_lt_two_seven L50
theorem five_squared_lt_two_5 L53
theorem cognitive_oncology_joint L58
theorem cognitive_oncology_size L61
theorem joint_125_squared L64
theorem triple_joint L69
theorem five_nine_lt_two_21 L72
abbrev RSTriple L77
theorem rsTriple_card L79
abbrev RSJoint L83
theorem rsJoint_card L85
theorem rsJoint_fits_14_bits L89
structure ProductRecognitionLatticeCert L92
def productRecognitionLatticeCert L102