IndisputableMonolith.Complexity.SAT.SmallBias
The module supplies placeholder definitions for an explicit small-bias family of XOR systems over n variables. Researchers extending linear SAT constraints toward derandomization or completeness results would cite it. It consists of type definitions and length bounds with no completed proofs.
claimA small-bias family of XOR systems over $n$ variables is a collection of linear parity constraints whose bias is bounded by a small parameter, equipped with polynomial-size masks and length controls.
background
The module imports the CNF setting in which variables are indexed by Fin n and the XOR setting in which each constraint asserts that the parity of a subset equals a target bit. It introduces auxiliary notions such as mask variables, constraint extraction from masks, and linear families that assemble these into systems. The overall context is the construction of explicit pseudorandom XOR families inside the SAT complexity layer of Recognition Science.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the linear small-bias layer that is imported by the Completeness module (which builds fully-determined backpropagation states from total assignments) and by the GeoFamily module (which extends the construction to Morton-curve-aligned octant parity constraints). It therefore occupies the explicit-construction step between basic XOR constraints and geometric or completeness results.
scope and limits
- Does not supply a concrete generator or explicit mask construction.
- Does not prove any bias bound or pseudorandomness property.
- Does not instantiate the family for a specific SAT instance.
- Does not contain termination or size proofs beyond length bounds.