spanAt

formal source

  26theorem canonicalSpan_eq : canonicalSpan = 2 ^ 3 - 1 := by decide
  27
  28/-- Reduced spans along the cube-dimension ladder. -/
  29def spanAt (d : ℕ) : ℕ := 2 ^ d - 1
  30
  31theorem span_at_3 : spanAt 3 = 7 := by decide
  32theorem span_at_2 : spanAt 2 = 3 := by decide
  33theorem span_at_1 : spanAt 1 = 1 := by decide
  34theorem span_at_0 : spanAt 0 = 0 := by decide
  35theorem span_at_4 : spanAt 4 = 15 := by decide
  36
  37/-- The span ladder is strictly increasing in d. -/
  38theorem span_strict_mono (d : ℕ) : spanAt d < spanAt (d + 1) := by
  39  unfold spanAt
  40  have h1 : 2 ^ d ≥ 1 := Nat.one_le_two_pow
  41  have h2 : 2 ^ (d + 1) = 2 * 2 ^ d := by rw [pow_succ]; ring
  42  omega
  43
  44/-- Between d = 3 (normal) and d = 4 (super-normal), the gap is
  45    15 − 7 = 8 = 2³, i.e., the extra working-memory headroom equals one
  46    full cube. -/
  47theorem super_normal_jump : spanAt 4 - spanAt 3 = 2 ^ 3 := by decide
  48
  49/-- The Miller 7 ± 2 corridor (5 to 9) brackets canonicalSpan. -/
  50theorem miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9 := by
  51  unfold canonicalSpan; decide
  52
  53structure WorkingMemoryFromCubeCert where
  54  canonical : canonicalSpan = 2 ^ 3 - 1
  55  reduced_to_5 : spanAt 2 = 3  -- collapse one dimension
  56  reduced_to_3 : spanAt 1 = 1  -- collapse two
  57  super_normal : spanAt 4 = 15  -- add one dimension
  58  miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9
  59  monotone : ∀ d, spanAt d < spanAt (d + 1)