geoFamily_poly_bound
plain-language theorem explainer
The geometric XOR family, formed by concatenating the linear mask family with the Morton octant family, has length at most 4(n+1)^2. Researchers establishing polynomial-size small-bias constructions or SAT reductions in Recognition Science would cite this bound to certify the overall family size. The proof is a one-line wrapper that unfolds the concatenation, substitutes the exact linear length and the quadratic octant bound, and closes the arithmetic with omega.
Claim. For every natural number $n$, if $H_{geo}(n)$ denotes the geometric XOR family then $|H_{geo}(n)| ≤ 4(n+1)^2$.
background
The geometric XOR family $H_{geo}(n)$ is the concatenation linearFamily n ++ mortonOctantFamily n. The linear family supplies axis-aligned parity masks whose length equals exactly 2(n+1)^2; the Morton octant family adds parity constraints on octants induced by the Morton curve and is bounded by 2(n+1)^2. The module develops this family to extend the linear masks with locality properties from the space-filling curve, supporting small-bias space constructions inside the SAT complexity analysis.
proof idea
The proof unfolds geoFamily to expose the append, rewrites the length of the concatenated list, substitutes the exact equality linearFamily_length_eq n and the quadratic upper bound mortonOctantFamily_size_bound n, then discharges the resulting inequality by omega.
why it matters
This lemma supplies the concrete polynomial bound required to instantiate HasPolySize geoSmallBias via the downstream declaration geoSmallBias_poly. It completes the size analysis for the geometric family, confirming that the Morton-augmented construction remains quadratic and therefore compatible with the Recognition Science treatment of small-bias spaces derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.