`five_squared_lt_two_5`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.ProductRecognitionLattice on GitHub at line 53.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  50theorem five_three_lt_two_seven : (5 : ℕ)^3 < 2^7 := by decide
  51
  52/-- The information-bound theorem: 5^k < 2^(⌈k·log_2 5⌉ + 1) for small k. -/
  53theorem five_squared_lt_two_5 : (5 : ℕ)^2 < 2^5 := by decide
  54
  55/-! ## Joint products of independent C1 (cognitive) and C3 (oncology). -/
  56
  57/-- Joint state space size: 5³ × 5³ = 5⁶ = 15625. -/
  58theorem cognitive_oncology_joint : (5 : ℕ)^3 * (5 : ℕ)^3 = 5^6 := by
  59  ring
  60
  61theorem cognitive_oncology_size : (5 : ℕ)^3 * (5 : ℕ)^3 = 15625 := by decide
  62
  63/-- Joint state size as iterated product. -/
  64theorem joint_125_squared : (125 : ℕ) * 125 = 15625 := by decide
  65
  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

papers checked against this theorem

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