Actual occupied-block geometry with only the numerator scale enlarged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKSecondary_growth_data {Cscale x η M T R S : ℝ} (hscale : 1 ≤ Cscale) (hx : 4 ≤ x) (_hη : 0 ≤ η) (hη1 : η ≤ 1) (hM : 1 ≤ M) (hT : 1 ≤ T) (hxMT : x = 4 * M * T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hRS : R * S ≤ x) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) {a : ℤ} (ha : |↑a| ≤ Cscale * x) {F : ℕ} (hF : ↑F ≤ 2 * T) {K : WExtractedKey} (hK : K ∈ wExtractedKeyBox (x ^ η)) {j : Fin 5 → ℕ} {positive : Bool} {b : ℕ} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) : 2 ^ j 0 ≤ 8 * x ^ 6 ∧ ↑(wGramSecondaryNumeratorMax a K F j) ≤ 16 * Cscale * x ^ 9 ∧ 16 * 2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4 ≤ 16 * x ^ 4

Frequency and modulus retain their original bounds; the shift enters only in the numerator bound. No change to the floor, mask, key or x = 4MT is made.