Finite assembly of actual coprime prefixes. These assembly lemmas explicitly consume cell bounds; the analytic producer must instantiate them.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_prefix_coprime_commute (x S : ℝ) (N : Finset ℕ) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (cap : Fin 5 → ℕ) : wAnalyticPrefix (wCoprimeFiber x N S U c) cap = wCoprimeFiber x N S (wAnalyticPrefix U cap) c

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_block_prefix_assembly (x S : ℝ) (N : Finset ℕ) (U : Finset (WExtractedTuple × ℤ)) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (B C : ℝ) (hcard : ↑(Finset.image (wCoprimeLabel x N S) (wAnalyticDyadicBlock U j positive)).card ≤ C) (hB : 0 ≤ B) (hcell : ∀ c ∈ Finset.image (wCoprimeLabel x N S) (wAnalyticDyadicBlock U j positive), ∀ cap ∈ LiLiuPrereqFouvry.Rectangle.box (wAnalyticBoxLo j) (wAnalyticBoxHi j), wBlockAmplitude K j * ‖wAnalyticPrefixSum (wCoprimeFiber x N S (wAnalyticDyadicBlock U j positive) c) β c₁ γ ζ a cap‖ ≤ B) : wBlockAmplitude K j * wAnalyticBlockPrefixMax (wAnalyticDyadicBlock U j positive) j β c₁ γ ζ a ≤ C * B

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_key_prefix_assembly (U : Finset (WExtractedTuple × ℤ)) (K : WExtractedKey) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (B D : ℝ) (hB : 0 ≤ B) (hD : ↑(Finset.image wAnalyticDyadicKey U).card ≤ D) (hblock : ∀ j ∈ Finset.image wAnalyticDyadicKey U, ∀ (positive : Bool), wBlockAmplitude K j * wAnalyticBlockPrefixMax (wAnalyticDyadicBlock U j positive) j β c₁ γ ζ a ≤ B) : wAnalyticKeyPrefixMajorant U K β c₁ γ ζ a ≤ 2 * D * B