five_five_lt_two_thirteen

formal source

  41theorem five_six_lt_two_fourteen : (5 : ℕ)^6 < 2^14 := by decide
  42
  43/-- 5⁵ < 2¹³ (full RS pentapod fits in 13 bits). -/
  44theorem five_five_lt_two_thirteen : (5 : ℕ)^5 < 2^13 := by decide
  45
  46/-- 5⁴ < 2¹⁰ = 1024 (four-fold RS state fits in 10 bits). -/
  47theorem five_four_lt_two_ten : (5 : ℕ)^4 < 2^10 := by decide
  48
  49/-- 5³ < 2⁷ (single triple fits in 7 bits — Miller's working memory range). -/
  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. -/