flatMap_length_bound'
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply when the per-list bound varies with the index k.
- Does not extend to infinite m or non-Nat indices.
- Does not yield a stricter asymptotic than the trivial m·bound.
- Does not address the internal structure of the XOR constraints themselves.
Lean usage
have hbound : ∀ level < maxOctantLevel n + 1, (octantsAtLevel n level).length ≤ 2 * (n + 1) := fun level _ => octantsAtLevel_length_bound n level; have h1 := flatMap_length_bound' (octantsAtLevel n) (maxOctantLevel n + 1) (2 * (n + 1)) hboundformal statement (Lean)
115private lemma flatMap_length_bound' (f : Nat → List (XORSystem n)) (m bound : Nat)
116 (hbound : ∀ k < m, (f k).length ≤ bound) :
117 ((List.range m).flatMap f).length ≤ m * bound := by
proof body
Tactic-mode proof.
118 rw [List.length_flatMap]
119 have h : ∀ k ∈ List.range m, (f k).length ≤ bound := by
120 intro k hk
121 exact hbound k (List.mem_range.mp hk)
122 have hsum : (List.map (fun k => (f k).length) (List.range m)).sum ≤
123 (List.map (fun _ => bound) (List.range m)).sum := by
124 apply List.sum_le_sum
125 intro k hk
126 exact h k hk
127 calc ((List.map (fun k => (f k).length) (List.range m)).sum : Nat)
128 ≤ (List.map (fun _ => bound) (List.range m)).sum := hsum
129 _ = m * bound := by rw [List.map_const', List.sum_replicate, List.length_range]; ring
130
131/-- Morton octant family has polynomial size O(n²). -/