The logarithmic ratio count on the actual secondary carrier

The code retains the common first beta coordinate, both second beta indices, both sieve coordinates, and both signed frequencies. Only the known fixed sign is removed. Thus ordered multiplicities are not lost.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioCode_mem_box {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {v : WGramSecondaryBase} (hv : v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))) : wGramSecondaryRatioCode v ∈ wGramSecondaryRatioBox K F j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioCode_injective {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : Set.InjOn wGramSecondaryRatioCode ↑(wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases_card_le_ratio {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : ↑(wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))).card ≤ ↑(2 ^ j 2) * ↑(F / K.1.1) ^ 2 * (4 * ↑(2 ^ (j 0 + 1)) * ↑(2 ^ j 4) * (1 + Real.log ↑(2 ^ (j 0 + 1))))

Every fixed-data base in the existing r-mean is counted. The final factor is O(H*S*log H), rather than the independent H²*S² box.