pith. sign in
module module moderate

IndisputableMonolith.Complexity.SAT.GeoFamily

show as:
view Lean formalization →

The GeoFamily module defines Morton indexing to interleave three coordinates and constructs octant-based geometric families of XOR constraints for SAT instances. It supplies definitions such as OctantLevel, octantVars, octantConstraint, and geoFamily to organize variables spatially. Complexity researchers studying explicit constructions for small-bias XOR systems would reference these objects. The module consists solely of definitions built on the imported CNF, XOR, and SmallBias modules.

claimThe Morton index interleaves three coordinates $x,y,z$ into one index. The geoFamily generates octant systems, each a collection of XOR constraints (parity of a variable subset equals a fixed parity) over variables indexed by elements of Fin $n$.

background

The module operates inside the SAT complexity layer. It imports the CNF module, where variable indices are elements of Fin $n$ for a problem of given size. The XOR module supplies the definition of a constraint as the parity of a subset of variables equaling a given parity value. The SmallBias module introduces a placeholder structure for an explicit small-bias family of such XOR systems. Morton ordering and octant partitioning supply the geometric mechanism to instantiate concrete families in three dimensions.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the geometric constructions that instantiate the small-bias placeholder. It supports explicit family generation in the Complexity.SAT hierarchy and contributes to the broader Recognition framework by providing 3D spatial structure for constraint systems, although no downstream uses are recorded.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (23)