octantSystems_length
plain-language theorem explainer
The lemma states that the list of XOR systems for any single octant at a given level contains exactly two elements, one for each parity. Researchers bounding the size of the geometric XOR family in SAT encodings of Morton octant constraints would cite this when deriving per-level system counts. The proof is immediate reflexivity on the explicit two-element construction in the definition of octantSystems.
Claim. For all natural numbers $n$, level, and octant, the list of XOR systems for octant $o$ at level $l$ has cardinality exactly 2.
background
The module defines the geometric XOR family extending linear mask families with Morton-curve-aligned octant parity constraints. The function octantSystems constructs, for given $n$, level, and octant, the two-element list consisting of the octantConstraint applied once with false parity and once with true parity. This lemma records the resulting length as invariably 2.
proof idea
One-line wrapper that applies reflexivity to the definition of octantSystems, which explicitly builds the list as the pair of false and true parity constraints.
why it matters
The result supplies the per-octant factor of 2 used to bound total systems at a level by 2 times the number of active octants. It anchors the geometric extension of the XOR family in the Recognition Science complexity module. No downstream citations are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.