inOctant
The predicate determines whether a Morton index belongs to a specified octant after a given number of space subdivisions. Workers on geometric constraint families for SAT problems cite this check when building Morton-aligned parity systems. The definition implements the test directly: it accepts every index at the undivided level and otherwise extracts the block index by scaling the Morton number with a power of eight derived from its binary logarithm.
claimThe predicate that returns true precisely when Morton index $m$ lies in octant $o$ at subdivision level $l$, given by the case $l=0$ or $(m / 8^{ (floor(log_2 m) / l) +1 }) mod 8^l = o$.
background
The module defines the geometric XOR family that augments linear masks with Morton-curve octant parity constraints. OctantLevel counts the depth of recursive octant division, where level zero covers the full space and level $k$ produces $8^k$ subregions. OctantIndex selects one subregion in that partition, ranging from zero to $8^l-1$. The predicate draws on the base-two logarithm supplied by the information-compression library to locate the correct block within the Morton ordering.
proof idea
The definition is a direct case distinction on the level parameter. When the level is zero it returns true unconditionally. Otherwise it evaluates the integer quotient of the Morton index by eight raised to the quantity (log base two of the index divided by the level, plus one), then reduces that quotient modulo eight to the power of the level and compares the result to the target octant index.
why it matters in Recognition Science
This definition supplies the membership test required to generate the octant systems inside the geometric family of XOR constraints. It fills the geometric extension step in the module that augments linear masks with Morton-aligned constraints. No parent theorems are yet recorded as users of the predicate, so its precise role in larger encodings remains open for downstream development.
scope and limits
- Does not generate Morton indices from spatial coordinates.
- Does not enforce that the supplied octant index lies between zero and eight to the level minus one.
- Does not extend to non-natural-number levels or indices.
- Does not interact with the linear mask family directly.
formal statement (Lean)
30def inOctant (mortonIdx : Nat) (level : OctantLevel) (octant : OctantIndex) : Bool :=
proof body
Definition body.
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. -/