pith. sign in
module module moderate

IndisputableMonolith.Complexity.SAT.GeoFamily

show as:
view Lean formalization →

The GeoFamily module constructs explicit families of SAT instances with three-dimensional geometric structure via Morton indexing of coordinates. Complexity researchers studying small-bias XOR systems or geometrically constrained formulas would cite these definitions when building explicit instances. The module supplies a collection of supporting definitions for octants and constraints but contains no theorems.

claimThe Morton index interleaves the binary digits of three coordinates $x,y,z$ to produce a linear index $m(x,y,z) : ℕ$. The geoFamily yields a collection of XOR systems (or CNF formulas) indexed by octant levels in a 3D grid, with octantVars selecting variables local to each octant and octantConstraint enforcing parity conditions within it.

background

The module works in the SAT complexity setting imported from CNF (variables indexed by Fin n), XOR (parity of a variable subset equals a given bit), and SmallBias (placeholder for explicit low-bias families of XOR systems). Morton indexing maps points in ℕ³ to ℕ by bit interleaving, which preserves geometric locality when variables are assigned to 3D positions. Hierarchical octant structures (OctantLevel, OctantIndex, inOctant) then partition the space into 2³ sub-cubes at each level, allowing octantSystems to assemble local constraint sets.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These geometric constructions supply the explicit 3D families needed for downstream complexity arguments in the Recognition Science framework, where D = 3 spatial dimensions and the eight-tick octave appear as structural landmarks. The module enables concrete small-bias XOR systems whose bias and locality properties can be analyzed against the Recognition Composition Law or phi-ladder mass formulas, even though no direct parent theorem is listed in the current dependency graph.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (23)