`triple_joint`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.ProductRecognitionLattice
domain: CrossDomain
line: 69 · 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 69.

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

formal source

  66/-! ## Larger joints. -/
  67
  68/-- Three triples: 125 × 125 × 125 = 5⁹ = 1953125 (~ 2 million). -/
  69theorem triple_joint : (125 : ℕ) * 125 * 125 = 1953125 := by decide
  70
  71/-- Sanity: 5⁹ = 1953125 < 2²¹ ≈ 2.1 million. -/
  72theorem five_nine_lt_two_21 : (5 : ℕ)^9 < 2^21 := by decide
  73
  74/-! ## Cross-domain product types — concrete instantiation. -/
  75
  76/-- A generic 5³ recognition state (D-cubed). -/
  77abbrev RSTriple : Type := Fin 5 × Fin 5 × Fin 5
  78
  79theorem rsTriple_card : Fintype.card RSTriple = 125 := by
  80  simp [RSTriple, Fintype.card_prod]
  81
  82/-- The joint state: two RS triples. -/
  83abbrev RSJoint : Type := RSTriple × RSTriple
  84
  85theorem rsJoint_card : Fintype.card RSJoint = 15625 := by
  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

papers checked against this theorem

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