rsJoint_fits_14_bits

formal source

  86  simp [RSJoint, Fintype.card_prod, rsTriple_card]
  87
  88/-- The joint state fits under 2¹⁴ = 16384 (clinical-bandwidth bound). -/
  89theorem rsJoint_fits_14_bits : Fintype.card RSJoint < 2^14 := by
  90  rw [rsJoint_card]; decide
  91
  92structure ProductRecognitionLatticeCert where
  93  five_cubed : (5 : ℕ)^3 = 125
  94  five_to_six : (5 : ℕ)^6 = 15625
  95  joint_size : (5 : ℕ)^3 * (5 : ℕ)^3 = 15625
  96  five_six_under_14_bits : (5 : ℕ)^6 < 2^14
  97  five_three_under_7_bits : (5 : ℕ)^3 < 2^7
  98  rsTriple_card : Fintype.card RSTriple = 125
  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