abbrev
definition
OctantLevel
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SAT.GeoFamily on GitHub at line 24.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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 :=