`productRecognitionLatticeCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.ProductRecognitionLattice
domain: CrossDomain
line: 102 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.ProductRecognitionLattice on GitHub at line 102.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  99  rsJoint_card : Fintype.card RSJoint = 15625
 100  joint_under_14_bits : Fintype.card RSJoint < 2^14
 101
 102def productRecognitionLatticeCert : ProductRecognitionLatticeCert where
 103  five_cubed := five_pow_3
 104  five_to_six := five_pow_6
 105  joint_size := cognitive_oncology_size
 106  five_six_under_14_bits := five_six_lt_two_fourteen
 107  five_three_under_7_bits := five_three_lt_two_seven
 108  rsTriple_card := rsTriple_card
 109  rsJoint_card := rsJoint_card
 110  joint_under_14_bits := rsJoint_fits_14_bits
 111
 112end IndisputableMonolith.CrossDomain.ProductRecognitionLattice

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.