inOctant
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.