38theorem span_strict_mono (d : ℕ) : spanAt d < spanAt (d + 1) := by
proof body
Tactic-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.