The numerical two-box allocation core

This is the finite numerical induction in the proof of Lemma 1, p. 312, of H. Iwaniec, A new form of the error term in the linear sieve (1980). It does not assert the full lemma's admissibility geometry or construct sieve weights.

Every occurrence is assigned to exactly one box, in its original order. The input may carry arbitrary labels, with a real weight attached to each label. In fact the numerical argument does not require the weights to be nonnegative.

inductive MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.BoxPartition {α : Type u_1} : List α → List α → List α → Prop

An occurrence-preserving partition into two subsequences. Each constructor puts the new final occurrence in exactly one of the boxes, even when labels repeat.

• nil {α : Type u_1} : BoxPartition [] [] []
• left {α : Type u_1} {left right input : List α} (a : α) : BoxPartition left right input → BoxPartition (left ++ [a]) right (input ++ [a])
• right {α : Type u_1} {left right input : List α} (a : α) : BoxPartition left right input → BoxPartition left (right ++ [a]) (input ++ [a])

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.BoxPartition.sublists {α : Type u_1} {left right input : List α} (h : BoxPartition left right input) : left.Sublist input ∧ right.Sublist input

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.BoxPartition.perm {α : Type u_1} {left right input : List α} (h : BoxPartition left right input) : (left ++ right).Perm input

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.BoxPartition.prod_eq {α : Type u_1} {left right input : List α} (h : BoxPartition left right input) (weight : α → ℝ) : (List.map weight left).prod * (List.map weight right).prod = (List.map weight input).prod

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.append_fits_one_box {A B x M N : ℝ} (hM : 0 ≤ M) (hN : 0 ≤ N) (hbudget : A * B * x ^ 2 ≤ M * N) : A * x ≤ M ∨ B * x ≤ N

If appending a factor overflowed both boxes, the squared-factor budget would be exceeded. No sign assumption on the box products or factor is necessary.

def MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.PrefixSquareBound {α : Type u_1} (weight : α → ℝ) (D : ℝ) (input : List α) : Prop

The actual indexed-prefix squared-factor condition, not an allocation premise.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.PrefixSquareBound weight D input = ∀ (i : ℕ) (hi : i < input.length), (List.map weight (List.take i input)).prod * weight input[i] ^ 2 ≤ D

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.prefixSquareBound_append_singleton_iff {α : Type u_1} (weight : α → ℝ) (D : ℝ) (input : List α) (a : α) : PrefixSquareBound weight D (input ++ [a]) ↔ PrefixSquareBound weight D input ∧ (List.map weight input).prod * weight a ^ 2 ≤ D

Bridge between the indexed condition and the step used by the snoc induction.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.exists_boxPartition_of_prefixSquareBound {α : Type u_1} (weight : α → ℝ) {M N : ℝ} (hM : 1 ≤ M) (hN : 1 ≤ N) (input : List α) (hprefix : PrefixSquareBound weight (M * N) input) : ∃ (left : List α) (right : List α), BoxPartition left right input ∧ (List.map weight left).prod ≤ M ∧ (List.map weight right).prod ≤ N

Construct the two boxes by appending each occurrence to a box that fits. This is the numerical core only, with no sieve-support or parity assertion.

theorem MathlibNt.SieveTheory.LiLiuPrereqWFBoxAllocation.exists_real_box_partition {M N : ℝ} (hM : 1 ≤ M) (hN : 1 ≤ N) (input : List ℝ) (hprefix : ∀ (i : ℕ) (hi : i < input.length), (List.take i input).prod * input[i] ^ 2 ≤ M * N) : ∃ (left : List ℝ) (right : List ℝ), BoxPartition left right input ∧ left.Sublist input ∧ right.Sublist input ∧ (left ++ right).Perm input ∧ left.prod * right.prod = input.prod ∧ left.prod ≤ M ∧ right.prod ≤ N

Real-list form with the explicit indexed hypothesis and the usual sublist, permutation, and product conclusions. The partition witness records disjoint occurrences; disjointness of values is neither required nor appropriate.