Actual A/B/C join on one retained prefix

All numerical mass and energy inputs of the normalization consumer are constructed from fixed-order coefficients and the actual arithmetic producer. The explicit local scale expressions still require payment.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_retained_prefix_three_terms (k m : ℕ) {ε κ δ ρ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hδ : 0 < δ) (hρ : 0 < ρ) : ∃ (Czero : ℝ) (Cnonzero : ℝ) (Csecondary : ℝ) (Cτ : ℝ) (Cjoint : ℝ) (Ca : ℝ) (Ccoeff : ℝ) (Couter : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ 0 < Csecondary ∧ 0 < Cτ ∧ 0 < Cjoint ∧ 0 < Ca ∧ 0 < Ccoeff ∧ 0 < Couter ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z T εSupport : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β γ ζ : ℕ → ℝ), a ≠ 0 → 0 ≤ R → 0 ≤ S → R ≤ X → S ≤ X → R * S ≤ X → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → (∀ n ∈ N, ↑n ≤ 2 * T) → (∀ n ∈ N, n ≤ F) → (∀ n ∈ N, ↑n ≤ X) → 1 < x → η < εSupport → x ^ εSupport ≤ T → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) → have E := Ccoeff * X ^ ρ; have W := (E * E) ^ 2; have Ez := ⋯ * ↑(wGramResonanceScaleBoxCard K F j) * wGramResonanceScaleEnvelope K F j ε; have Es := wGramSecondaryBaseCountBound K F j * ⋯; have Em := ⋯; ⋯