flatMap_length_bound'
plain-language theorem explainer
This auxiliary lemma bounds the length of the concatenation of m lists, each produced by a function f from naturals, by m times a uniform upper bound on their individual lengths. Researchers establishing polynomial size for geometric families of XOR constraint systems in SAT encodings would cite it to control the total number of parity constraints. The proof rewrites the flatMap length, converts the forall hypothesis via range membership, applies a sum inequality, and reduces the replicated sum to m times the bound via length and replicate sum.
Claim. Let $f : {0,1,2,ldots} → $ lists of XOR constraint systems on $n$ variables, and let $m,b ∈ ℕ$. If $(f(k)).length ≤ b$ for every $k < m$, then the length of the concatenation of the lists $f(0),…,f(m-1)$ is at most $m·b$.
background
The module constructs the geometric XOR family 𝓗_geo(n) by extending linear masks with Morton-curve octant parity constraints on n variables. XORSystem(n) is defined as a list of XOR constraints, each enforcing parity on a subset of the n bits. The lemma supplies a generic length bound used when the family is assembled by flatMapping over octant levels. Upstream, the XORSystem abbreviation supplies the list type whose lengths are bounded; the RSNative map and AsteroidOre has declarations appear only as module imports and play no role in this auxiliary statement.
proof idea
The tactic proof begins by rewriting List.length_flatMap. It then builds an auxiliary forall over List.range m by applying mem_range.mp to the given hypothesis. Next it invokes List.sum_le_sum on the mapped lengths to obtain a sum inequality. The calculation step equates the right-hand sum to m·bound by rewriting List.map_const', List.sum_replicate, List.length_range and applying ring.
why it matters
The lemma is invoked inside mortonOctantFamily_size_bound to conclude that the Morton octant family has length at most 2(n+1)², thereby establishing the O(n²) polynomial size of the full geometric family. In the Recognition Science setting this size control is required before one can embed the geometric constraints into larger SAT instances whose complexity is measured against the phi-ladder and eight-tick octave. No open scaffolding remains; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.