geoFamily
plain-language theorem explainer
The definition constructs the geometric XOR family for n variables by concatenating the linear mask systems with the Morton octant systems. Researchers analyzing small-bias families or isolation invariants in SAT would cite this construction when instantiating geometric candidates. The definition proceeds by direct list concatenation of the two component families.
Claim. Let $H_{geo}(n)$ be the geometric XOR family over $n$ variables. Then $H_{geo}(n)$ is the concatenation of the linear mask family (all systems generated by masks below $(n+1)^2$) with the Morton octant family (all octant parity systems up to the maximum octant level).
background
The module defines the geometric XOR family $H_{geo}(n)$ as an extension of the linear mask family by Morton-curve-aligned octant parity constraints. An XORSystem $n$ is a list of XOR constraints on $n$ variables. The linearFamily enumerates pairs of systems for each mask below $(n+1)^2$, while mortonOctantFamily collects octants at every level from 0 to maxOctantLevel $n$.
proof idea
The definition is a one-line wrapper that concatenates the output of linearFamily $n$ with the output of mortonOctantFamily $n$.
why it matters
This definition supplies the concrete family used by geoSmallBias to instantiate a SmallBiasFamily candidate. It appears in the hypothesis of geometric_isolation_enables_propagation_thm and supports the polynomial size bound shown in geoFamily_poly_bound. The construction provides a geometric candidate family for isolation arguments in the SAT completeness analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.