noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondaryWeight (κ δ ρ C Csec Ccoeff x : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℝ

All arithmetic excess factors, but no structural powers or section length.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondaryWeight κ δ ρ C Csec Ccoeff x a K F j = C * (Ccoeff * x ^ ρ) ^ 4 * (1 + Real.log (2 * 2 ^ j 0)) * ↑a.natAbs.divisors.card * (16 * 2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4) ^ κ * √(Csec * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryNumeratorMax a K F j) ^ δ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_weight_nonneg {κ δ ρ C Csec Ccoeff x : ℝ} (hC : 0 ≤ C) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : 0 ≤ directPaySecondaryWeight κ δ ρ C Csec Ccoeff x a K F j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_energy_local {κ δ ρ C Csec Ccoeff x T : ℝ} (hκ : 0 ≤ κ) (hC : 0 ≤ C) (hCsec : 0 ≤ Csec) (_hT : 0 ≤ T) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (F : ℕ) (j cap : Fin 5 → ℕ) (hF : ↑F ≤ 2 * T) : directJoinedSecondary κ δ ρ C Csec Ccoeff x a R S K F j cap ≤ 256 * √8 * directPaySecondaryWeight κ δ ρ C Csec Ccoeff x a K F j * 2 ^ j 0 * (2 ^ j 2) ^ 2 * T ^ 2 * 2 ^ j 3 * √(2 ^ j 3) * (2 ^ j 4) ^ 3 * (↑K.D' + 2 * 2 ^ j 1 / (2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4))

Actual energy, not a hypothesis. Both q contributions remain literal.