module module

`IndisputableMonolith.Complexity.SAT.GeoFamily`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.SAT.CNF module_import
IndisputableMonolith.Complexity.SAT.SmallBias module_import
IndisputableMonolith.Complexity.SAT.XOR module_import

declarations in this module (23)

def mortonIndex L20
abbrev OctantLevel L24
abbrev OctantIndex L27
def inOctant L30
def octantVars L35
def octantConstraint L41
def octantSystems L45
def octantsAtLevel L49
def maxOctantLevel L54
def mortonOctantFamily L58
def geoFamily L63
lemma octantSystems_length L67
lemma octantsAtLevel_length_bound L72
lemma succ_le_two_pow L85
lemma log2_succ_le L96
lemma maxOctantLevel_le L108
lemma flatMap_length_bound' L115
lemma mortonOctantFamily_size_bound L132
lemma geoFamily_poly_bound L149
def mortonLocality L158
theorem mortonLocality_holds L163
def geoSmallBias L171
instance geoSmallBias_poly L174