Resonance hypotheses from actual occupied witnesses

Both fixed supports, both canonical tuples, and the nonzero signed frequency are recovered from the original key fiber. The lower beta support excludes both degenerate differences. The common-k payment stays at its local dyadic width, not the full level.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramCoprimePrefix_subset (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels_fixedSupport {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {b : ℕ} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {L : WGramLabel} (hL : L ∈ wGramLabels V) : wKSectionFixedSupport N a x η R S K L.1.1 L.1.2 L.2.1.1 L.2.1.2.1 ∧ wKSectionFixedSupport N a x η R S K L.1.1 L.1.2 L.2.2.1 L.2.2.2.1 ∧ L.2.1.2.2 ≠ 0 ∧ L.2.2.2.2 ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramZeroLabels_resonance_data {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z T : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (hNT : ∀ n ∈ N, T ≤ ↑n) (hT : x ^ η < T) {K : WExtractedKey} {b : ℕ} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {L : WGramLabel} (hL : L ∈ wGramZeroLabels K a V) : L.2.1.2.2 * ↑L.2.2.1 * ↑L.2.2.2.1 ≠ 0 ∧ ↑K.1.2.1 * ↑L.1.2 - ↑L.2.2.1 ≠ 0 ∧ 0 < L.2.1.1 ∧ 0 < L.2.1.2.1 ∧ (K.1.2.1 * L.1.2).Coprime L.2.1.1 ∧ ↑K.1.2.1 * ↑L.1.2 - ↑L.2.1.1 ≠ 0 ∧ wGramNumerator K a L = 0

All arithmetic inputs of the genuine divisor count, obtained from an occupied zero label. Neither difference is a caller-supplied hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairCount_le_dyadic (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (L : WGramLabel) : wGramPairCount N a x η R S M Z K b j cap positive c L ≤ 2 ^ j 1