The local finite box of occupied resonance bases

The box keeps all five independent coordinates (r,n₁,h,n₂',s'). Its frequency interval has the actual fixed sign. Its second beta width is F/d, obtained from the original upper beta support, not from the first beta coordinate. No positivity is assumed for keys with empty occupied carriers.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval (i : ℕ) : Finset ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval i = Finset.Ico (2 ^ i) (2 ^ (i + 1))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval_card (i : ℕ) : (wGramResonanceScaleInterval i).card = 2 ^ i

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleFrequencies (i : ℕ) (positive : Bool) : Finset ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleFrequencies i positive = Finset.image (fun (n : ℕ) => if positive = true then ↑n else -↑n) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval i)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleFrequencies_card_le (i : ℕ) (positive : Bool) : (wGramResonanceScaleFrequencies i positive).card ≤ 2 ^ i

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBox (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (positive : Bool) : Finset WGramResonanceBase

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBox K F j positive = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval (j 3) ×ˢ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval (j 2)) ×ˢ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleFrequencies (j 0) positive ×ˢ Finset.Ioc 0 (F / K.1.1) ×ˢ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval (j 4)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBoxCard (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBoxCard K F j = 2 ^ j 3 * 2 ^ j 2 * 2 ^ j 0 * (F / K.1.1) * 2 ^ j 4

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBox_card_le (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (positive : Bool) : (wGramResonanceScaleBox K F j positive).card ≤ wGramResonanceScaleBoxCard K F j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels_second_beta_le_upper {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 : ℕ} {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) : 0 < K.1.1 ∧ L.2.2.1 ∈ Finset.Ioc 0 (F / K.1.1)

Membership recovers positive d and the original d*n₂' ∈ N before dividing by d. An empty label set requires no positive key.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBases_subset_scaleBox {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 (ℕ × ℕ)) : wGramResonanceBases (wGramZeroLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) ⊆ wGramResonanceScaleBox K F j positive

The inclusion is an identity injection into the Cartesian box; neither beta coordinate nor the signed frequency is identified with another.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBases_card_le_scaleBox {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 (ℕ × ℕ)) : (wGramResonanceBases (wGramZeroLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))).card ≤ wGramResonanceScaleBoxCard K F j