IndisputableMonolith.Complexity.SAT.GeoFamily

   1import Mathlib
   2import IndisputableMonolith.Complexity.SAT.CNF
   3import IndisputableMonolith.Complexity.SAT.XOR
   4import IndisputableMonolith.Complexity.SAT.SmallBias
   5
   6namespace IndisputableMonolith
   7namespace Complexity
   8namespace SAT
   9
  10/-!
  11# Geometric XOR Family (Morton Octant Masks)
  12
  13This module defines the geometric XOR family 𝓗_geo(n) which extends the linear
  14mask family with Morton-curve-aligned octant parity constraints.
  15-/
  16
  17open List
  18
  19/-- Morton index: interleave 3 coordinates into a single index. -/
  20def mortonIndex (x y z : Nat) : Nat :=
  21  x + y * 1000 + z * 1000000
  22
  23/-- Octant level: how many octant subdivisions (0 = whole space, k = 8^k subregions). -/
  24abbrev OctantLevel := Nat
  25
  26/-- Octant index within a level (0 to 8^level - 1). -/
  27abbrev OctantIndex := Nat
  28
  29/-- Check if a Morton index falls within a given octant at a given level. -/
  30def inOctant (mortonIdx : Nat) (level : OctantLevel) (octant : OctantIndex) : Bool :=
  31  if level = 0 then true
  32  else (mortonIdx / (8 ^ (Nat.log2 mortonIdx / level + 1))) % (8 ^ level) = octant
  33
  34/-- Variables in a given octant. -/
  35def octantVars (n : Nat) (level : OctantLevel) (octant : OctantIndex) : List (Var n) :=
  36  (List.finRange n).filter fun v =>
  37    if level = 0 then true
  38    else v.val / (n / (8 ^ level).max 1) = octant % ((8 ^ level).min n)
  39
  40/-- XOR constraint for a single octant. -/
  41def octantConstraint (n : Nat) (level : OctantLevel) (octant : OctantIndex) (parity : Bool) : XORConstraint n :=
  42  { vars := octantVars n level octant, parity := parity }
  43
  44/-- XOR system for a single octant (both parities). -/
  45def octantSystems (n : Nat) (level : OctantLevel) (octant : OctantIndex) : List (XORSystem n) :=
  46  [[octantConstraint n level octant false], [octantConstraint n level octant true]]
  47
  48/-- All octants at a given level. -/
  49def octantsAtLevel (n : Nat) (level : OctantLevel) : List (XORSystem n) :=
  50  (List.range ((8 ^ level).min (n + 1))).flatMap fun octant =>
  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. -/
  85private lemma succ_le_two_pow (n : Nat) : n.succ ≤ 2 ^ n := by
  86  induction n with
  87  | zero => simp
  88  | succ n ih =>
  89    have h1 : 1 ≤ 2^n := Nat.one_le_two_pow
  90    calc n.succ.succ = n.succ + 1 := rfl
  91      _ ≤ 2 ^ n + 1 := by omega
  92      _ ≤ 2 ^ n + 2 ^ n := by omega
  93      _ = 2 ^ n.succ := by omega
  94
  95/-- Auxiliary: log2(n+1) ≤ n for all n. -/
  96private lemma log2_succ_le (n : Nat) : Nat.log2 n.succ ≤ n := by
  97  rw [Nat.log2_eq_log_two]
  98  have h1 : 1 < 2 := by norm_num
  99  have h3 : n.succ ≠ 0 := by omega
 100  have hlt : Nat.log 2 n.succ < n.succ := by
 101    rw [Nat.log_lt_iff_lt_pow h1 h3]
 102    have h4 : n.succ.succ ≤ 2^n.succ := succ_le_two_pow n.succ
 103    calc n.succ < n.succ.succ := by omega
 104      _ ≤ 2 ^ n.succ := h4
 105  omega
 106
 107/-- maxOctantLevel n ≤ n (since log2(n+1)/3 ≤ log2(n+1) ≤ n). -/
 108lemma maxOctantLevel_le (n : Nat) : maxOctantLevel n ≤ n := by
 109  unfold maxOctantLevel
 110  have h1 : Nat.log2 n.succ / 3 ≤ Nat.log2 n.succ := Nat.div_le_self _ _
 111  have h2 : Nat.log2 n.succ ≤ n := log2_succ_le n
 112  omega
 113
 114/-- Auxiliary: flatMap length bound. -/
 115private lemma flatMap_length_bound' (f : Nat → List (XORSystem n)) (m bound : Nat)
 116    (hbound : ∀ k < m, (f k).length ≤ bound) :
 117    ((List.range m).flatMap f).length ≤ m * bound := by
 118  rw [List.length_flatMap]
 119  have h : ∀ k ∈ List.range m, (f k).length ≤ bound := by
 120    intro k hk
 121    exact hbound k (List.mem_range.mp hk)
 122  have hsum : (List.map (fun k => (f k).length) (List.range m)).sum ≤
 123              (List.map (fun _ => bound) (List.range m)).sum := by
 124    apply List.sum_le_sum
 125    intro k hk
 126    exact h k hk
 127  calc ((List.map (fun k => (f k).length) (List.range m)).sum : Nat)
 128      ≤ (List.map (fun _ => bound) (List.range m)).sum := hsum
 129    _ = m * bound := by rw [List.map_const', List.sum_replicate, List.length_range]; ring
 130
 131/-- Morton octant family has polynomial size O(n²). -/
 132lemma mortonOctantFamily_size_bound (n : Nat) :
 133    (mortonOctantFamily n).length ≤ 2 * n.succ ^ 2 := by
 134  unfold mortonOctantFamily
 135  have hbound : ∀ level < maxOctantLevel n + 1, (octantsAtLevel n level).length ≤ 2 * (n + 1) :=
 136    fun level _ => octantsAtLevel_length_bound n level
 137  have h1 := flatMap_length_bound' (octantsAtLevel n) (maxOctantLevel n + 1) (2 * (n + 1)) hbound
 138  have h2 : maxOctantLevel n + 1 ≤ n + 1 := by
 139    have := maxOctantLevel_le n
 140    omega
 141  calc (mortonOctantFamily n).length
 142      = ((List.range (maxOctantLevel n + 1)).flatMap (octantsAtLevel n)).length := rfl
 143    _ ≤ (maxOctantLevel n + 1) * (2 * (n + 1)) := h1
 144    _ ≤ (n + 1) * (2 * (n + 1)) := Nat.mul_le_mul_right _ h2
 145    _ = 2 * (n + 1) ^ 2 := by ring
 146    _ = 2 * n.succ ^ 2 := rfl
 147
 148/-- Geometric family has polynomial size O(n²). -/
 149lemma geoFamily_poly_bound (n : Nat) :
 150    (geoFamily n).length ≤ 4 * n.succ ^ 2 := by
 151  unfold geoFamily
 152  rw [List.length_append]
 153  have h1 := linearFamily_length_eq n
 154  have h2 := mortonOctantFamily_size_bound n
 155  omega
 156
 157/-- Locality: variables in an octant are close in Morton space. -/
 158def mortonLocality (n : Nat) (level : OctantLevel) (octant : OctantIndex) : Prop :=
 159  ∀ v ∈ octantVars n level octant,
 160    if level = 0 then True
 161    else v.val / (n / (8 ^ level).max 1) = octant % ((8 ^ level).min n)
 162
 163theorem mortonLocality_holds (n : Nat) (level : OctantLevel) (octant : OctantIndex) :
 164    mortonLocality n level octant := by
 165  intro v hv
 166  unfold octantVars at hv
 167  simp only [List.mem_filter, List.mem_finRange, true_and] at hv
 168  exact hv
 169
 170/-- Geometric family candidate for isolation. -/
 171def geoSmallBias : SmallBiasFamily :=
 172  { 𝓗 := geoFamily }
 173
 174instance geoSmallBias_poly : HasPolySize geoSmallBias :=
 175  ⟨⟨4, 2, fun n => geoFamily_poly_bound n⟩⟩
 176
 177end SAT
 178end Complexity
 179end IndisputableMonolith
 180