Reciprocal normalization, keeping the long interval term

Exact local algebra precedes any global enlargement. The last theorem is explicitly conditional only on numeric outer-mass and energy estimates; it is not a claimed proof of C.2, nor a new cancellation hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_span_le (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (L : WGramLabel) : ↑(wGramSpan R S M Z K j cap L) ≤ 2 * 2 ^ j 1

Inclusive interval length, including the natural subtraction convention.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_cost_split (ε C : ℝ) (a : ℤ) (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (L : WGramLabel) (hq : 0 < wGramModulus L) : wBlockAmplitude K j * wGramFouvryCost ε C a R S M Z K j cap L = C * ↑a.natAbs.divisors.card * √↑((wGramModulus L).gcd (wGramNumerator K a L).natAbs) * ↑(wGramModulus L) ^ ε * (wBlockAmplitude K j * ↑K.D' * √↑(wGramModulus L) + wBlockAmplitude K j * ↑(wGramSpan R S M Z K j cap L) / √↑(wGramModulus L))

Exact q^(1/2+epsilon) split. The span/q contribution does not disappear.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_long_factor_le (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (L : WGramLabel) (hD : 0 < K.D) (hq : 0 < wGramModulus L) : wBlockAmplitude K j * ↑(wGramSpan R S M Z K j cap L) / √↑(wGramModulus L) ≤ 2 / (↑K.D * 2 ^ j 3 * 2 ^ j 4 * √↑(wGramModulus L))

The inclusive span bound cancels k only after its true reciprocal factor.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_floor_frequency_paid {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) j positive) : wBlockAmplitude K j * 2 ^ j 0 ≤ 8 * Z / M

The local denominator cancels the true floor frequency, before enlargement.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_ceil_frequency_paid {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wUniformCutoff M Z) N Q a P R S ξ b K) j positive) : wBlockAmplitude K j * 2 ^ j 0 ≤ 8 * Z / M + wBlockAmplitude K j

The ceiling analogue honestly retains the reciprocal unit-frequency cost.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_rpow_payment {A H B p : ℝ} (hA : 0 < A) (hH : 0 ≤ H) (hB : 0 ≤ B) (hp : 0 ≤ p) (hHB : H ≤ A * B) : A⁻¹ * H ^ p ≤ A ^ (p - 1) * B ^ p

General monomial payment; the exponent p-1 is retained on the local denominator.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_sqrt_three {a b c : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : √(a + b + c) ≤ √a + √b + √c

Standard square-root split with both nonzero terms separately visible.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_actual_cauchy_three {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) (c : Finset (ℕ × ℕ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) {B Ezero Eshort Elong : ℝ} (hB : 0 ≤ B) (hz : 0 ≤ Ezero) (hs : 0 ≤ Eshort) (hl : 0 ≤ Elong) (hMass : wCorrelationOuterMass x N S U c K β c₁ γ ≤ B) (hEnergy : wSeparatedCorrelationEnergy x N S U c K β ζ a ≤ Ezero + Eshort + Elong) : wBlockAmplitude K j * ‖∑ t ∈ wCoprimeFiber x N S U c, ↑(wExtractedCoefficient β c₁ γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1‖ ≤ wBlockAmplitude K j * √B * (√Ezero + √Eshort + √Elong)

Conditional A/B consumer on the literal signed arithmetic carrier. Only numeric mass and three energy bounds are inputs. No C.2-sized target is assumed; all three contributions and the exact reciprocal stay visible.