maxOctantLevel

formal source

  51    octantSystems n level octant
  52
  53/-- Maximum octant level: log_8(n) levels of subdivision. -/
  54def maxOctantLevel (n : Nat) : Nat :=
  55  Nat.log2 n.succ / 3
  56
  57/-- Morton octant mask family: all octants at all levels. -/
  58def mortonOctantFamily (n : Nat) : List (XORSystem n) :=
  59  (List.range (maxOctantLevel n + 1)).flatMap fun level =>
  60    octantsAtLevel n level
  61
  62/-- Geometric XOR family: linear masks + Morton octant masks. -/
  63def geoFamily (n : Nat) : List (XORSystem n) :=
  64  linearFamily n ++ mortonOctantFamily n
  65
  66/-- Each octant contributes exactly 2 systems. -/
  67lemma octantSystems_length (n level octant : Nat) :
  68    (octantSystems n level octant).length = 2 := rfl
  69
  70/-- At each level, the number of systems is at most 2 * (n + 1).
  71    Proof: each of min(8^level, n+1) octants contributes 2 systems. -/
  72lemma octantsAtLevel_length_bound (n level : Nat) :
  73    (octantsAtLevel n level).length ≤ 2 * (n + 1) := by
  74  unfold octantsAtLevel
  75  rw [List.length_flatMap]
  76  have hlen : ∀ octant, (octantSystems n level octant).length = 2 := fun _ => rfl
  77  simp only [hlen]
  78  rw [List.map_const', List.sum_replicate, List.length_range]
  79  have hmin : (8 ^ level).min (n + 1) ≤ n + 1 := Nat.min_le_right _ _
  80  calc (8 ^ level).min (n + 1) * 2
  81      = 2 * (8 ^ level).min (n + 1) := by ring
  82    _ ≤ 2 * (n + 1) := by omega
  83
  84/-- Auxiliary: n + 1 ≤ 2^n for all n. -/