linearFamily
The linearFamily definition builds a deterministic collection of single-constraint XOR systems by ranging over every mask index below (n+1) squared and emitting the two parity variants for each mask. Researchers constructing explicit small-bias families for SAT completeness or correlation bounds would cite this construction when assembling the linear component of a geometric family. It is realized by a direct flatMap over List.range combined with the systemOfMask constructor.
claimFor each natural number $n$, linearFamily$(n)$ is the list obtained by ranging over all masks $m < (n+1)^2$ and, for each such $m$, appending the two singleton XOR systems systemOfMask$(n,m,0)$ and systemOfMask$(n,m,1)$.
background
The SmallBias module supplies placeholder structures for explicit small-bias families of XOR systems. An XORSystem $n$ is an abbreviation for a list of XOR constraints on $n$ variables. The helper systemOfMask $n$ mask parity constructs a singleton system consisting of the parity constraint whose support is selected by the bits of mask and whose target parity is the supplied Boolean. The definition depends on the successor operation imported from both arithmetic and vantage modules.
proof idea
The definition is a direct functional construction that applies List.range to $(n.succ)^2$ and then flatMaps each mask index to the two-element list containing systemOfMask $n$ mask false and systemOfMask $n$ mask true.
why it matters in Recognition Science
This definition supplies the linear-mask component of the geometric family geoFamily, which concatenates it with the Morton octant family. It is referenced by the length-equality, length-bound, and polynomial-bound lemmas inside the same module, and it appears inside the (now falsified) geometric-isolation-enables-propagation hypothesis. Within the broader Recognition framework the construction provides an explicit deterministic family that could eventually interface with small-bias or forcing-chain arguments, though no such link is formalized here.
scope and limits
- Does not prove satisfiability or completeness for any generated system.
- Does not incorporate Morton-order or octant masks.
- Does not establish bias or correlation bounds for the family.
- Does not connect the construction to Recognition Science constants or the phi-ladder.
Lean usage
def geoFamily (n : Nat) : List (XORSystem n) := linearFamily n ++ mortonOctantFamily nformal statement (Lean)
40def linearFamily : (n : Nat) → List (XORSystem n) := fun n =>
proof body
Definition body.
41 (List.range ((n.succ) ^ 2)).flatMap fun mask =>
42 [systemOfMask n mask false, systemOfMask n mask true]
43
44/-- The linear-mask small-bias candidate. -/