Complete and partial residue blocks used to count finite prime-square conditions.

def LeanPool.DeadEnds.completeBlock (M k : ℕ) : Finset ℕ

The k-th complete block of positive integers of length M.

Equations

• LeanPool.DeadEnds.completeBlock M k = Finset.Icc (k * M + 1) ((k + 1) * M)

theorem LeanPool.DeadEnds.primeSquareProduct_pos (S : Finset Nat.Primes) : 0 < primeSquareProduct S

theorem LeanPool.DeadEnds.completeBlocks_subset_Icc (M X : ℕ) (_hM : 0 < M) (k : ℕ) (hk : k < X / M) : completeBlock M k ⊆ Finset.Icc 1 X

theorem LeanPool.DeadEnds.completeBlock_card (M k : ℕ) (hM : 0 < M) : (completeBlock M k).card = M

theorem LeanPool.DeadEnds.completeBlock_mapsTo (M k : ℕ) (hM : 0 < M) : Set.MapsTo (fun (x : ℕ) => x % M) ↑(completeBlock M k) ↑(Finset.range M)

theorem LeanPool.DeadEnds.abs_sub_lt_of_mem_completeBlock (M k x y : ℕ) (_hM : 0 < M) (hx : x ∈ completeBlock M k) (hy : y ∈ completeBlock M k) : |↑y - ↑x| < ↑M

For any x, y in the complete block [kM+1, (k+1)M], we have |y - x| < M.

This follows because:

• The block has width (k+1)M - (kM+1) = M - 1
• So the maximum absolute difference between any two elements is M - 1 < M In integers: max(y) - min(x) = (k+1)M - (kM+1) = M - 1 and min(y) - max(x) = (kM+1) - (k+1)M = 1 - M So |y - x| ≤ M - 1 < M. Mathlib coverage: This uses abs_sub_lt_iff and basic interval arithmetic.

theorem LeanPool.DeadEnds.completeBlock_injOn (M k : ℕ) (hM : 0 < M) : Set.InjOn (fun (x : ℕ) => x % M) ↑(completeBlock M k)

The function N ↦ N % M is injective on the complete block. Two numbers in [kM+1, (k+1)M] with the same residue mod M must be equal, since they are within distance M of each other. The proof uses the fact that if x, y are in [kM+1, (k+1)M], then |x - y| < M. If x % M = y % M and |x - y| < M, then x = y (since the only multiple of M in (-M, M) is 0).

theorem LeanPool.DeadEnds.completeBlock_surjOn (M k : ℕ) (hM : 0 < M) : Set.SurjOn (fun (x : ℕ) => x % M) ↑(completeBlock M k) ↑(Finset.range M)

theorem LeanPool.DeadEnds.completeBlock_residues_bijective (M k : ℕ) (hM : 0 < M) : Set.BijOn (fun (x : ℕ) => x % M) ↑(completeBlock M k) ↑(Finset.range M)

For N in the k-th complete block, N mod M takes each residue below M exactly once. This is because N ranges from kM+1 through (k+1)M, and:

• (kM+j) mod M = j for 1 ≤ j < M
• (k+1)M mod M = 0 More precisely: the map N ↦ N % M is a bijection from B_k to Finset.range M.

theorem LeanPool.DeadEnds.filter_mapsTo (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (k : ℕ) : have M := primeSquareProduct S; let P := fun (N : ℕ) => ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d; Set.MapsTo (fun (x : ℕ) => x % M) ↑(Finset.filter P (completeBlock M k)) ↑(Finset.filter P (Finset.range M))

theorem LeanPool.DeadEnds.filter_injOn (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (k : ℕ) : have M := primeSquareProduct S; let P := fun (N : ℕ) => ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d; Set.InjOn (fun (x : ℕ) => x % M) ↑(Finset.filter P (completeBlock M k))

Filtering a complete block preserves injectivity of the residue map.

theorem LeanPool.DeadEnds.filter_surjOn (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (k : ℕ) : have M := primeSquareProduct S; let P := fun (N : ℕ) => ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d; Set.SurjOn (fun (x : ℕ) => x % M) ↑(Finset.filter P (completeBlock M k)) ↑(Finset.filter P (Finset.range M))

Filtering a complete block preserves surjectivity of the residue map onto valid residues.

theorem LeanPool.DeadEnds.filter_card_eq_of_bijOn_filter (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (k : ℕ) : have M := primeSquareProduct S; let P := fun (N : ℕ) => ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d; Set.BijOn (fun (x : ℕ) => x % M) ↑(Finset.filter P (completeBlock M k)) ↑(Finset.filter P (Finset.range M))

theorem LeanPool.DeadEnds.completeBlock_valid_count (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (k : ℕ) : have M := primeSquareProduct S; have A := validResiduesMod b T S; {N ∈ completeBlock M k | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card = A.card

Each complete block B_k contributes exactly |A| valid integers.

Since the map N ↦ N % M is a bijection from B_k to Finset.range M, and by condition_mod_invariant validity depends only on N % M, the count of valid N in B_k equals the count of valid residues in Finset.range M, which is |A|. Uses: condition_mod_invariant, completeBlock_residues_bijective

theorem LeanPool.DeadEnds.completeBlock_disjoint (M : ℕ) (_hM : 0 < M) (i j : ℕ) (hij : i < j) : Disjoint (completeBlock M i) (completeBlock M j)

theorem LeanPool.DeadEnds.completeBlocks_pairwise_disjoint (M : ℕ) (hM : 0 < M) : Set.univ.PairwiseDisjoint fun (k : ℕ) => ↑(completeBlock M k)

The complete blocks indexed by Finset.range q are pairwise disjoint. Block B_i = [iM+1, (i+1)M] and B_j = [jM+1, (j+1)M] are disjoint for i ≠ j because their ranges don't overlap. Uses: For i < j, (i+1)M < jM+1 so the intervals are disjoint.

theorem LeanPool.DeadEnds.sum_valid_from_blocks_le_count (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; ∑ k ∈ Finset.range (X / M), {N ∈ completeBlock M k | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card ≤ count

The sum of valid elements from all complete blocks ≤ count.

Since blocks are disjoint and contained in [1,X], the union of filtered blocks is a subset of the filtered [1,X], so the sum of cardinalities is at most count. Uses: completeBlocks_pairwise_disjoint, completeBlocks_subset_Icc, Finset.card_biUnion

theorem LeanPool.DeadEnds.count_lower_bound (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have A := validResiduesMod b T S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; X / M * A.card ≤ count

def LeanPool.DeadEnds.partialBlock (M X : ℕ) : Finset ℕ

The partial block consists of the remaining integers from q * M + 1 through X, where q = X / M.

Equations

• LeanPool.DeadEnds.partialBlock M X = Finset.Icc (X / M * M + 1) X

theorem LeanPool.DeadEnds.partialBlock_subset_Icc (M X : ℕ) (_hM : 0 < M) : partialBlock M X ⊆ Finset.Icc 1 X

theorem LeanPool.DeadEnds.partialBlock_subset_Ico (M X : ℕ) (hM : 0 < M) : ↑(partialBlock M X) ⊆ ↑(Finset.Ico (X / M * M) (X / M * M + M))

theorem LeanPool.DeadEnds.partialBlock_injOn_mod (M X : ℕ) : Set.InjOn (fun (x : ℕ) => x % M) ↑(partialBlock M X)

The residue map N ↦ N % M is injective on the partial block from q * M + 1 through X. This is because for any N in the partial block, N = qM + k where 1 ≤ k ≤ r < M (where r = X % M), so N % M = k. Different elements have different k values. The key insight is that all elements lie within a single period of M: they are all in [qM+1, q*M+r] where r < M. Uses: Set.InjOn : ∀ {α : Type u_1} {β : Type u_2}, (α → β) → Set α → Prop which states f is injective on s iff ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y.

theorem LeanPool.DeadEnds.partialBlock_validMapsTo (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have A := validResiduesMod b T S; have validBlock := {N ∈ partialBlock M X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}; Set.MapsTo (fun (x : ℕ) => x % M) ↑validBlock ↑A

theorem LeanPool.DeadEnds.partialBlock_valid_count_le (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have A := validResiduesMod b T S; {N ∈ partialBlock M X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card ≤ A.card

theorem LeanPool.DeadEnds.completeBlock_disjoint_partialBlock (M X : ℕ) (_hM : 0 < M) (k : ℕ) (hk : k < X / M) : Disjoint (completeBlock M k) (partialBlock M X)

theorem LeanPool.DeadEnds.biUnion_completeBlocks_disjoint_partialBlock (M X : ℕ) (_hM : 0 < M) : Disjoint ((Finset.range (X / M)).biUnion (completeBlock M)) (partialBlock M X)

theorem LeanPool.DeadEnds.mem_completeBlock_of_div_lt (M X n : ℕ) (hM : 0 < M) (hn_pos : 1 ≤ n) (_hn_le : n ≤ X) (_hk : (n - 1) / M < X / M) : n ∈ completeBlock M ((n - 1) / M)

theorem LeanPool.DeadEnds.mem_partialBlock_of_div_eq (M X n : ℕ) (_hM : 0 < M) (hn_pos : 1 ≤ n) (hn_le : n ≤ X) (hk : (n - 1) / M = X / M) : n ∈ partialBlock M X

theorem LeanPool.DeadEnds.div_sub_one_le_div (M X n : ℕ) (hn_pos : 1 ≤ n) (hn_le : n ≤ X) : (n - 1) / M ≤ X / M

theorem LeanPool.DeadEnds.Icc_eq_biUnion_union_partialBlock (M X : ℕ) (hM : 0 < M) : Finset.Icc 1 X = (Finset.range (X / M)).biUnion (completeBlock M) ∪ partialBlock M X

The interval [1,X] equals the disjoint union of complete blocks indexed by Finset.range q and the partial block V from qM + 1 through X. Every n ∈ [1,X] falls into exactly one of:

• Complete block B_k where k = (n-1)/M for k < q
• Partial block V if (n-1)/M ≥ q Conversely, all elements in the blocks are in [1,X] by completeBlocks_subset_Icc and partialBlock_subset_Icc. Uses the division algorithm: n = (n-1)/M * M + (n-1)%M + 1.

theorem LeanPool.DeadEnds.filtered_biUnion_disjoint_filtered_partialBlock (M X : ℕ) (hM : 0 < M) (P : ℕ → Prop) [DecidablePred P] : Disjoint (Finset.filter P ((Finset.range (X / M)).biUnion (completeBlock M))) (Finset.filter P (partialBlock M X))

theorem LeanPool.DeadEnds.pairwiseDisjoint_filter_of_pairwiseDisjoint {ι : Type u_1} (s : Set ι) (f : ι → Finset ℕ) (P : ℕ → Prop) [DecidablePred P] (hpwd : s.PairwiseDisjoint f) : s.PairwiseDisjoint fun (k : ι) => Finset.filter P (f k)

Filtering preserves pairwise disjointness of Finsets: if the original Finsets are pairwise disjoint, then their filtered versions are too. Mathlib has Finset.pairwiseDisjoint_filter : ∀ {α β : Type*} {s : Finset α} {f : α → Finset β}, (↑s).PairwiseDisjoint f → ∀ (p : β → Prop), (↑s).PairwiseDisjoint (fun a => Finset.filter p (f a)) but this only works for Finsets s, not arbitrary sets. This follows from Set.PairwiseDisjoint.mono : ∀ {s : Set ι} {f g : ι → α}, s.PairwiseDisjoint f → g ≤ f → s.PairwiseDisjoint g combined with Finset.filter_subset : ∀ (p : α → Prop) [DecidablePred p] (s : Finset α), Finset.filter p s ⊆ s to show that filtering decreases each set. Since (f k).filter P ⊆ f k for all k, and disjointness is preserved under taking subsets, the filtered family inherits pairwise disjointness from the original family.

theorem LeanPool.DeadEnds.filtered_completeBlocks_pairwiseDisjoint (M : ℕ) (hM : 0 < M) (P : ℕ → Prop) [DecidablePred P] (s : Finset ℕ) : (↑s).PairwiseDisjoint fun (k : ℕ) => Finset.filter P (completeBlock M k)

theorem LeanPool.DeadEnds.count_eq_sum_blocks (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; have blockCounts := ∑ k ∈ Finset.range (X / M), {N ∈ completeBlock M k | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; have partialCount := {N ∈ partialBlock M X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; count = blockCounts + partialCount