mortonLocality_holds
plain-language theorem explainer
The theorem confirms that every variable selected into an octant at a given level satisfies the Morton locality predicate by construction of the filter. Researchers encoding geometric SAT instances or Morton-curve constraint families cite it to guarantee spatial clustering of variables. The short tactic proof introduces membership, unfolds the octantVars filter, simplifies the membership predicate via simp on List.mem_filter and finRange, and discharges by exact.
Claim. For all natural numbers $n$, octant levels $k$, and indices $o$, every variable $v$ belonging to the list of variables in octant $o$ at level $k$ satisfies: if $k=0$ then true, else $v / (n / (8^k).max 1) = o % ((8^k).min n)$.
background
The module defines the geometric XOR family extending linear masks with Morton-curve-aligned octant parity constraints. OctantLevel is the natural number counting subdivisions (0 for the whole space, $k$ for $8^k$ subregions). OctantIndex is the natural number indexing one of those subregions (0 to $8^k-1$). octantVars returns the filtered list of Var n whose Morton indices fall inside the chosen octant, using the quotient test $v.val / (n / (8^level).max 1) = octant % ((8^level).min n)$ when level > 0. mortonLocality is the proposition that every such selected variable obeys the same quotient test, i.e., the filter already enforces locality in Morton space.
proof idea
The tactic proof opens with intro v hv to obtain an arbitrary variable and its membership hypothesis. It unfolds octantVars at hv, exposing the filter expression. simp only [List.mem_filter, List.mem_finRange, true_and] reduces the membership statement to the filter predicate itself. exact hv then discharges the goal because the predicate is precisely the locality condition required by mortonLocality.
why it matters
The result is a foundational verification inside the geometric family construction, ensuring that octantVars produces spatially clustered variables for the Morton octant masks. It supports downstream definitions such as octantConstraint, octantSystems, and geoFamily by guaranteeing the locality property quoted in the module header. Within the Recognition framework it supplies a concrete geometric structure for SAT instances that can later interface with the self-similar fixed-point and eight-tick octave machinery, although the present declaration itself remains internal to the complexity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.