A fixed occurrence-aware normalized signed geometric family

The index set is an image of a powerset, so one multiplicity profile occurs once, regardless of how many prime subsets realize it. Each member is one full-integer divided-power box product with the actual small Rosser weight. The family, the sign, and the small weight are fixed before every level split.

The favourable signs use lower endpoints; the opposite signs require distinct boxes and the strict upper-endpoint tests. This is the normalized convention of SignedRounding, not Iwaniec's factorial-copy labelled-slot sum.

def MathlibNt.SieveTheory.LiLiuPrereqWF.LooseSign (upper : Bool) (r : ℕ) : Prop

Upper/even and lower/odd are the loose lower-endpoint sides.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.LooseSign upper r = if upper = true then Even r else ¬Even r

def MathlibNt.SieveTheory.LiLiuPrereqWF.SignedTagAccepted (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (t : List ℕ) : Prop

Exact lower-endpoint source admissibility, with the redundant product cutoff retained explicitly. The other sign uses strict upper-endpoint tests.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SignedTagAccepted upper b c D t = (MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.Admissible upper b D t ∧ if MathlibNt.SieveTheory.LiLiuPrereqWF.LooseSign upper t.length then (List.map b t).prod < D else t.Nodup ∧ (List.map c t).prod < D ∧ MathlibNt.SieveTheory.LiLiuPrereqWFAdmissibility.CubicPrefixBound upper c D t)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) : Finset (List ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label = Finset.filter (MathlibNt.SieveTheory.LiLiuPrereqWF.SignedTagAccepted upper (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower D ε (ε ^ 9)) (fun (j : ℕ) => MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower D ε (ε ^ 9) (j + 1)) D) (Finset.image (MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile label) (P \ MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes P D ε).powerset)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.signedSmallWeight (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (r : ℕ) : ArithmeticFunction ℝ

The actual small Rosser choice in (25)--(26): loose signs use the upper small weight and tight signs use the lower small weight.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.signedSmallWeight upper P D ε r = if MathlibNt.SieveTheory.LiLiuPrereqWF.LooseSign upper r then MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight P D ε else MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight P D ε

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (t : List ℕ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t = (-1) ^ t.length • MathlibNt.SieveTheory.LiLiuPrereqWF.geometricBoxTerm P D ε (ε ^ 9) t (MathlibNt.SieveTheory.LiLiuPrereqWF.signedSmallWeight upper P D ε t.length)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate upper P D ε label = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε label, MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_apply (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (n : ℕ) : (signedFamilyAggregate upper P D ε label) n = ∑ t ∈ signedTags upper P D ε label, (signedFamilyTerm upper P D ε t) n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.wellFactorable_smul_of_abs_le_one {f : ArithmeticFunction ℝ} {Q r : ℝ} (hf : WellFactorable f Q) (hr : |r| ≤ 1) : WellFactorable (r • f) Q

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedSmallWeight_primeSupported (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (r : ℕ) : PrimeSupported (geometricSmallPrimes P D ε) (signedSmallWeight upper P D ε r)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_primeSupported (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (t : List ℕ) : PrimeSupported P (signedFamilyTerm upper P D ε t)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_eq_zero_of_not_subset (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) {n : ℕ} (hsub : ¬n.primeFactors ⊆ P) : (signedFamilyAggregate upper P D ε label) n = 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_wellFactorable (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (t : List ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hadm : LiLiuPrereqWFAdmissibility.Admissible upper (geometricLower D ε (ε ^ 9)) D t) : WellFactorable (signedFamilyTerm upper P D ε t) (D ^ (1 + ε + ε ^ 9))

One concrete signed term, on all integers, works for every real split of the same enlarged level. There is no supplied coefficient or factorization.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags_common_wellFactorable (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (t : List ℕ) : t ∈ signedTags upper P D ε label → WellFactorable (signedFamilyTerm upper P D ε t) (D ^ (1 + ε + ε ^ 9))

Finite family membership is decided numerically before all splits. Duplicate prime realizations do not add additional family members.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_squarefree (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (t : List ℕ) (hD : 1 ≤ D) (hε : 0 ≤ ε) {n : ℕ} (hn : Squarefree n) : (signedFamilyTerm upper P D ε t) n = if n.primeFactors ⊆ geometricSmallPrimes P D ε ∪ t.toFinset.biUnion (geometricPrimeBox P D ε (ε ^ 9)) ∧ ∀ j ∈ t.toFinset, (n.primeFactors ∩ geometricPrimeBox P D ε (ε ^ 9) j).card = List.count j t then (-1) ^ t.length * (signedSmallWeight upper P D ε t.length) ((n.primeFactors ∩ geometricSmallPrimes P D ε).prod id) else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometricLower_strictMono {D ε θ : ℝ} (hD : 1 < D) (hε : 0 < ε) (hθ : 0 < θ) : StrictMono (geometricLower D ε θ)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.geometric_boxLabel_monotoneOn (P S : Finset ℕ) {D ε θ : ℝ} (label : ℕ → ℕ) (hD : 1 ≤ D) (hθ : 0 ≤ θ) (hlabel : ∀ p ∈ S, p ∈ geometricPrimeBox P D ε θ (label p)) (p : ℕ) : p ∈ S → ∀ q ∈ S, p ≤ q → label p ≤ label q

Actual membership in half-open geometric boxes forces the label order. No monotonicity of a supplied labelling is an additional assumption.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedTagAccepted_boxProfile_iff (upper : Bool) (label : ℕ → ℕ) (b c : ℕ → ℝ) (D : ℝ) (S : Finset ℕ) (hmono : ∀ p ∈ S, ∀ q ∈ S, p ≤ q → label p ≤ label q) (hbmono : Monotone b) (hbinj : Function.Injective b) (hone : ∀ p ∈ S, 1 ≤ b (label p)) (hhead : ∀ p ∈ S, b (label p) ^ 2 < D) (hbc : ∀ p ∈ S, b (label p) ≤ c (label p)) : SignedTagAccepted upper b c D (boxProfile label S) ↔ if LooseSign upper S.card then RoundedSupport upper (fun (p : ℕ) => b (label p)) D S else TightRoundedSupport upper (fun (p : ℕ) => b (label p)) (fun (p : ℕ) => c (label p)) D S

Numerical identification of the source tag tests with the concrete normalized set convention, retaining the source head restriction.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (S : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet upper b c D S = if upper = true then MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperSet b c D S else MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerSet b c D S

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet_eq_profile_indicator (upper : Bool) (label : ℕ → ℕ) (b c : ℕ → ℝ) (D : ℝ) (S : Finset ℕ) (hmono : ∀ p ∈ S, ∀ q ∈ S, p ≤ q → label p ≤ label q) (hbmono : Monotone b) (hbinj : Function.Injective b) (hone : ∀ p ∈ S, 1 ≤ b (label p)) (hhead : ∀ p ∈ S, b (label p) ^ 2 < D) (hbc : ∀ p ∈ S, b (label p) ≤ c (label p)) : normalizedSignedSet upper (fun (p : ℕ) => b (label p)) (fun (p : ℕ) => c (label p)) D S = if SignedTagAccepted upper b c D (boxProfile label S) then (-1) ^ S.card else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_squarefree_profile (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 1 ≤ D) (hε : 0 ≤ ε) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) {n : ℕ} (hn : Squarefree n) (hsub : n.primeFactors ⊆ P) : (signedFamilyAggregate upper P D ε label) n = if SignedTagAccepted upper (geometricLower D ε (ε ^ 9)) (fun (j : ℕ) => geometricLower D ε (ε ^ 9) (j + 1)) D (boxProfile label (n.primeFactors \ geometricSmallPrimes P D ε)) then (-1) ^ (n.primeFactors \ geometricSmallPrimes P D ε).card * (signedSmallWeight upper P D ε (n.primeFactors \ geometricSmallPrimes P D ε).card) ((n.primeFactors ∩ geometricSmallPrimes P D ε).prod id) else 0

The aggregate has exactly one possible squarefree contribution: the canonical large-prime profile. This proves the absence of factorial copies.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_squarefree_normalized (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) {n : ℕ} (hn : Squarefree n) (hsub : n.primeFactors ⊆ P) : (signedFamilyAggregate upper P D ε label) n = normalizedSignedSet upper (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p)) (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p) ^ (1 + ε ^ 9)) D (n.primeFactors \ geometricSmallPrimes P D ε) * (signedSmallWeight upper P D ε (n.primeFactors \ geometricSmallPrimes P D ε).card) ((n.primeFactors ∩ geometricSmallPrimes P D ε).prod id)

Identification with the SAME normalized upper/lower set coefficients. The factors are the actual small Rosser weights selected in (25)--(26). Only the geometric labelling and the source head bound are numerical inputs.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate_squarefree (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) {n : ℕ} (hn : Squarefree n) : (signedFamilyAggregate upper P D ε label) n = if n.primeFactors ⊆ P then normalizedSignedSet upper (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p)) (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p) ^ (1 + ε ^ 9)) D (n.primeFactors \ geometricSmallPrimes P D ε) * (signedSmallWeight upper P D ε (n.primeFactors \ geometricSmallPrimes P D ε).card) ((n.primeFactors ∩ geometricSmallPrimes P D ε).prod id) else 0

The normalized identification at every squarefree integer, including integers outside the fixed sieve-prime support. It is not a squarefree mask definition: the left side remains the common full-integer family.