def
definition
mortonLocality
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SAT.GeoFamily on GitHub at line 158.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
155 omega
156
157/-- Locality: variables in an octant are close in Morton space. -/
158def mortonLocality (n : Nat) (level : OctantLevel) (octant : OctantIndex) : Prop :=
159 ∀ v ∈ octantVars n level octant,
160 if level = 0 then True
161 else v.val / (n / (8 ^ level).max 1) = octant % ((8 ^ level).min n)
162
163theorem mortonLocality_holds (n : Nat) (level : OctantLevel) (octant : OctantIndex) :
164 mortonLocality n level octant := by
165 intro v hv
166 unfold octantVars at hv
167 simp only [List.mem_filter, List.mem_finRange, true_and] at hv
168 exact hv
169
170/-- Geometric family candidate for isolation. -/
171def geoSmallBias : SmallBiasFamily :=
172 { 𝓗 := geoFamily }
173
174instance geoSmallBias_poly : HasPolySize geoSmallBias :=
175 ⟨⟨4, 2, fun n => geoFamily_poly_bound n⟩⟩
176
177end SAT
178end Complexity
179end IndisputableMonolith