abbrev
definition
OctantIndex
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Complexity.SAT.GeoFamily on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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. -/