Problems / erdos-257 / variant-6b364d2b--h1--h1
Tao–Teräväinen §§5.6–5.14: κ₂–κ₅ for each Lemma 5.2 cube
variant-6b364d2b--h1--h1
open
Hole tt_sec5_setup of variant-6b364d2b--h1 (split by 20261023T140825Z-t1023-f2-partial.lean).
$\displaystyle \forall q \ge 1,\ T,\ \delta > 0,\ P_0\ \ \exists P \ge P_0,\ 2^K \le (\log P)^{2/3},\ H \le (\log P)^{2/3}\ \ \forall (p_0, v)\ \ \exists (N_s, S_1, S_2, M, \eta, w, R):\ \kappa_2, \kappa_3, \kappa_4, \kappa_5 \le \delta,\ \sum_{\varepsilon} \frac{1+\eta}{p_\varepsilon} \le \delta,\ \frac{q}{2^{K+1}} \le \delta,\ 2^K T \le \log\log R - \log\log w$
What is left of Tao–Teräväinen Theorem 5.1 (arXiv:2512.01739v2, p. 49) once the set-up is fixed: for every prime cube that Lemma 5.2 produces in (P/2, P], a random n (uniform on Ns) obeying (5.5)-(5.6) and (5.33), the prime split S₀/S₁/S₂ of §5.6 (S₁ avoids the discriminant of the near shifts), equidistribution (5.35) mod each p_ε and each p ∈ S₁ up to η, and the estimates κ₂ (§5.8), κ₃ (§§5.12-5.14, the paper's use of its Theorem 3.1(i)), κ₄ (§5.9), κ₅ (§5.10). The parameter clause 2^K T ≤ log log R - log log w is §5.11's (log₂R - log₂W)/2^K → ∞. Proved here, not in the hole: Lemma 5.2 (quantitative; Aristotle for t1023-f2, from t1022-s's and t1022-x's projects), Mertens' second theorem on S₁ (t1022-u), κ₁ (§5.7), (5.19), S₀ and the variance step (t1022-w's reduction), and the exact variance bound c₀ = q²/8 (t1023-f2).
Lean
theorem variant_6b364d2b__h1__h1 : ∀ (q : ℕ),
(0 : ℕ) < q →
∀ (T δ : ℝ),
(0 : ℝ) < δ →
∀ (P0 : ℕ),
∃ (Pw : ℕ) (K : ℕ) (H : ℕ),
P0 ≤ Pw ∧
(1 : ℕ) ≤ K ∧
(1 : ℕ) ≤ H ∧
(2 : ℝ) ^ K ≤ Real.log (↑Pw : ℝ) ^ (2 / 3 : ℝ) ∧
(↑H : ℝ) ≤ Real.log (↑Pw : ℝ) ^ (2 / 3 : ℝ) ∧
∀ (p0 : ℤ) (v : Fin K → ℤ) (P : (Fin K → Bool) → ℕ),
(∀ (ε : Fin K → Bool),
Nat.Prime (P ε) ∧
Pw < (2 : ℕ) * P ε ∧
P ε ≤ Pw ∧ (↑(P ε) : ℤ) = p0 + ∑ k : Fin K, if ε k = true then v k else (0 : ℤ)) →
(Function.Injective fun (ε : Fin K → Bool) =>
p0 + ∑ k : Fin K, if ε k = true then v k else (0 : ℤ)) →
(Function.Injective fun (x : (Fin K → Bool) × Fin H) =>
(p0 + ∑ k : Fin K, if x.1 k = true then v k else (0 : ℤ)) *
(↑((↑x.2 : ℕ) + (1 : ℕ) + K) : ℤ) -
∑ k : Fin K, ((↑(↑k : ℕ) : ℤ) + (1 : ℤ)) * if x.1 k = true then v k else (0 : ℤ)) →
∃ (B : ℕ) (Ns : Finset ℤ) (m : ℤ → (Fin K → Bool) → ℕ) (S1 : Finset ℕ) (S2 : Finset ℕ)
(sgn : (Fin K → Bool) → ℝ) (r : (Fin K → Bool) → ℕ → ℤ) (X : ℕ → ℤ → ℝ) (M : ℕ) (η : ℝ)
(w : ℕ) (R : ℕ),
((∀ (ε : Fin K → Bool), sgn ε = ∏ i : Fin K, if ε i = true then (-1 : ℝ) else (1 : ℝ)) ∧
(∀ (ε : Fin K → Bool) (h : ℕ),
r ε h =
p0 * (↑h : ℤ) +
∑ k : Fin K,
((↑h : ℤ) - ((↑(↑k : ℕ) : ℤ) + (1 : ℤ))) *
if ε k = true then v k else (0 : ℤ)) ∧
(∀ (p : ℕ) (n : ℤ),
X p n =
(↑q : ℝ) *
∑ k ∈ Finset.range H,
(∑ ε : Fin K → Bool,
sgn ε *
if p ∣ (n + r ε (k + K + (1 : ℕ))).toNat then (1 : ℝ)
else (0 : ℝ)) /
(2 : ℝ) ^ (k + K + (1 : ℕ))) ∧
Even M) ∧
(Ns.Nonempty ∧
(∀ n ∈ Ns,
∀ (ε : Fin K → Bool),
(n -
∑ k : Fin K,
((↑(↑k : ℕ) : ℤ) + (1 : ℤ)) * if ε k = true then v k else (0 : ℤ)) =
(↑(P ε) : ℤ) * (↑(m n ε) : ℤ)) ∧
∀ n ∈ Ns,
∀ (ε : Fin K → Bool),
∀ k < H,
(0 : ℤ) < n + r ε (k + K + (1 : ℕ)) ∧
n + r ε (k + K + (1 : ℕ)) ≤ (↑B : ℤ)) ∧
(S1 ⊆ Finset.filter Nat.Prime (Finset.range (B + (1 : ℕ))) ∧
S2 ⊆ Finset.filter Nat.Prime (Finset.range (B + (1 : ℕ))) ∧
Disjoint S1 S2 ∧
(∀ p ∈ Finset.filter Nat.Prime (Finset.range (B + (1 : ℕ))),
p ∉ S1 → p ∉ S2 → ∀ n ∈ Ns, ∀ n' ∈ Ns, (↑p : ℤ) ∣ n - n') ∧
∀ p ∈ S1,
∀ k1 < H,
∀ k2 < H,
∀ (ε1 ε2 : Fin K → Bool),
k1 ≠ k2 ∨ ε1 ≠ ε2 →
¬(↑p : ℤ) ∣ r ε1 (k1 + K + (1 : ℕ)) - r ε2 (k2 + K + (1 : ℕ))) ∧
((0 : ℝ) ≤ η ∧
η ≤ (1 / 4 : ℝ) ∧
(∀ (ε : Fin K → Bool) (a : ℕ),
(↑{n ∈ Ns | P ε ∣ m n ε + a}.card : ℝ) * (↑(P ε) : ℝ) ≤
((1 : ℝ) + η) * (↑Ns.card : ℝ)) ∧
∀ p ∈ S1,
∀ (a : ℤ),
|(↑{n ∈ Ns | (↑p : ℤ) ∣ n + a}.card : ℝ) * (↑p : ℝ) -
(↑Ns.card : ℝ)| ≤
η * (↑Ns.card : ℝ)) ∧
((↑q : ℝ) / (2 : ℝ) ^ (K + (1 : ℕ)) ≤ δ ∧
∑ ε : Fin K → Bool, ((1 : ℝ) + η) / (↑(P ε) : ℝ) ≤ δ) ∧
((↑Ns.card : ℝ)⁻¹ *
∑ n ∈ Ns,
∑' (k : ℕ),
(∑ ε : Fin K → Bool,
(↑((ArithmeticFunction.cardDistinctFactors : ℕ → ℕ)
(n + r ε (k + H + K + (1 : ℕ))).toNat) :
ℝ)) /
(2 : ℝ) ^ (k + H + K + (1 : ℕ)) ≤
δ ∧
√((↑Ns.card : ℝ)⁻¹ * ∑ n ∈ Ns, (∑ p ∈ S2, X p n) ^ (2 : ℕ)) ≤ δ ∧
∑ j ∈ Finset.range (M + (1 : ℕ)),
((2 : ℝ) * Real.pi) ^ j / (↑j.factorial : ℝ) *
|(↑Ns.card : ℝ)⁻¹ * ∑ n ∈ Ns, (∑ p ∈ S1, X p n) ^ j -
(↑(Fintype.piFinset fun (x : ↥S1) => Ns).card : ℝ)⁻¹ *
∑ ω ∈ Fintype.piFinset fun (x : ↥S1) => Ns,
(∑ p : ↥S1, X (↑p : ℕ) (ω p)) ^ j| ≤
δ ∧
(∏ p ∈ S1,
(↑Ns.card : ℝ)⁻¹ *
∑ n ∈ Ns,
Real.exp ((2 : ℝ) * Real.pi * Real.exp (1 : ℝ) * X p n) +
∏ p ∈ S1,
(↑Ns.card : ℝ)⁻¹ *
∑ n ∈ Ns,
Real.exp
(-((2 : ℝ) * Real.pi * Real.exp (1 : ℝ)) * X p n)) /
Real.exp (1 : ℝ) ^ M ≤
δ) ∧
(3 : ℕ) ≤ w ∧
w ≤ R ∧
(2 : ℝ) ^ K * T ≤
Real.log (Real.log (↑R : ℝ)) - Real.log (Real.log (↑w : ℝ)) ∧
∑ p ∈ Finset.filter Nat.Prime (Finset.Ioc w R) \ S1,
(1 : ℝ) / (↑p : ℝ) ≤
(1 : ℝ) := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Open. A direct proof closes it.
What is known
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
import Nodes.«variant-6b364d2b--h1--h1».Context
/-! Hole `tt_sec5_setup` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem variant_6b364d2b__h1__h1 : ∀ (q : ℕ),
(0 : ℕ) < q →
∀ (T δ : ℝ),
(0 : ℝ) < δ →
∀ (P0 : ℕ),
∃ (Pw : ℕ) (K : ℕ) (H : ℕ),
P0 ≤ Pw ∧
(1 : ℕ) ≤ K ∧
(1 : ℕ) ≤ H ∧
(2 : ℝ) ^ K ≤ Real.log (↑Pw : ℝ) ^ (2 / 3 : ℝ) ∧
(↑H : ℝ) ≤ Real.log (↑Pw : ℝ) ^ (2 / 3 : ℝ) ∧
∀ (p0 : ℤ) (v : Fin K → ℤ) (P : (Fin K → Bool) → ℕ),
(∀ (ε : Fin K → Bool),
Nat.Prime (P ε) ∧
Pw < (2 : ℕ) * P ε ∧
P ε ≤ Pw ∧ (↑(P ε) : ℤ) = p0 + ∑ k : Fin K, if ε k = true then v k else (0 : ℤ)) →
(Function.Injective fun (ε : Fin K → Bool) =>
p0 + ∑ k : Fin K, if ε k = true then v k else (0 : ℤ)) →
(Function.Injective fun (x : (Fin K → Bool) × Fin H) =>
(p0 + ∑ k : Fin K, if x.1 k = true then v k else (0 : ℤ)) *
(↑((↑x.2 : ℕ) + (1 : ℕ) + K) : ℤ) -
∑ k : Fin K, ((↑(↑k : ℕ) : ℤ) + (1 : ℤ)) * if x.1 k = true then v k else (0 : ℤ)) →
∃ (B : ℕ) (Ns : Finset ℤ) (m : ℤ → (Fin K → Bool) → ℕ) (S1 : Finset ℕ) (S2 : Finset ℕ)
(sgn : (Fin K → Bool) → ℝ) (r : (Fin K → Bool) → ℕ → ℤ) (X : ℕ → ℤ → ℝ) (M : ℕ) (η : ℝ)
(w : ℕ) (R : ℕ),
((∀ (ε : Fin K → Bool), sgn ε = ∏ i : Fin K, if ε i = true then (-1 : ℝ) else (1 : ℝ)) ∧
(∀ (ε : Fin K → Bool) (h : ℕ),
r ε h =
p0 * (↑h : ℤ) +
∑ k : Fin K,
((↑h : ℤ) - ((↑(↑k : ℕ) : ℤ) + (1 : ℤ))) *
if ε k = true then v k else (0 : ℤ)) ∧
(∀ (p : ℕ) (n : ℤ),
X p n =
(↑q : ℝ) *
∑ k ∈ Finset.range H,
(∑ ε : Fin K → Bool,
sgn ε *
if p ∣ (n + r ε (k + K + (1 : ℕ))).toNat then (1 : ℝ)
else (0 : ℝ)) /
(2 : ℝ) ^ (k + K + (1 : ℕ))) ∧
Even M) ∧
(Ns.Nonempty ∧
(∀ n ∈ Ns,
∀ (ε : Fin K → Bool),
(n -
∑ k : Fin K,
((↑(↑k : ℕ) : ℤ) + (1 : ℤ)) * if ε k = true then v k else (0 : ℤ)) =
(↑(P ε) : ℤ) * (↑(m n ε) : ℤ)) ∧
∀ n ∈ Ns,
∀ (ε : Fin K → Bool),
∀ k < H,
(0 : ℤ) < n + r ε (k + K + (1 : ℕ)) ∧
n + r ε (k + K + (1 : ℕ)) ≤ (↑B : ℤ)) ∧
(S1 ⊆ Finset.filter Nat.Prime (Finset.range (B + (1 : ℕ))) ∧
S2 ⊆ Finset.filter Nat.Prime (Finset.range (B + (1 : ℕ))) ∧
Disjoint S1 S2 ∧
(∀ p ∈ Finset.filter Nat.Prime (Finset.range (B + (1 : ℕ))),
p ∉ S1 → p ∉ S2 → ∀ n ∈ Ns, ∀ n' ∈ Ns, (↑p : ℤ) ∣ n - n') ∧
∀ p ∈ S1,
∀ k1 < H,
∀ k2 < H,
∀ (ε1 ε2 : Fin K → Bool),
k1 ≠ k2 ∨ ε1 ≠ ε2 →
¬(↑p : ℤ) ∣ r ε1 (k1 + K + (1 : ℕ)) - r ε2 (k2 + K + (1 : ℕ))) ∧
((0 : ℝ) ≤ η ∧
η ≤ (1 / 4 : ℝ) ∧
(∀ (ε : Fin K → Bool) (a : ℕ),
(↑{n ∈ Ns | P ε ∣ m n ε + a}.card : ℝ) * (↑(P ε) : ℝ) ≤
((1 : ℝ) + η) * (↑Ns.card : ℝ)) ∧
∀ p ∈ S1,
∀ (a : ℤ),
|(↑{n ∈ Ns | (↑p : ℤ) ∣ n + a}.card : ℝ) * (↑p : ℝ) -
(↑Ns.card : ℝ)| ≤
η * (↑Ns.card : ℝ)) ∧
((↑q : ℝ) / (2 : ℝ) ^ (K + (1 : ℕ)) ≤ δ ∧
∑ ε : Fin K → Bool, ((1 : ℝ) + η) / (↑(P ε) : ℝ) ≤ δ) ∧
((↑Ns.card : ℝ)⁻¹ *
∑ n ∈ Ns,
∑' (k : ℕ),
(∑ ε : Fin K → Bool,
(↑((ArithmeticFunction.cardDistinctFactors : ℕ → ℕ)
(n + r ε (k + H + K + (1 : ℕ))).toNat) :
ℝ)) /
(2 : ℝ) ^ (k + H + K + (1 : ℕ)) ≤
δ ∧
√((↑Ns.card : ℝ)⁻¹ * ∑ n ∈ Ns, (∑ p ∈ S2, X p n) ^ (2 : ℕ)) ≤ δ ∧
∑ j ∈ Finset.range (M + (1 : ℕ)),
((2 : ℝ) * Real.pi) ^ j / (↑j.factorial : ℝ) *
|(↑Ns.card : ℝ)⁻¹ * ∑ n ∈ Ns, (∑ p ∈ S1, X p n) ^ j -
(↑(Fintype.piFinset fun (x : ↥S1) => Ns).card : ℝ)⁻¹ *
∑ ω ∈ Fintype.piFinset fun (x : ↥S1) => Ns,
(∑ p : ↥S1, X (↑p : ℕ) (ω p)) ^ j| ≤
δ ∧
(∏ p ∈ S1,
(↑Ns.card : ℝ)⁻¹ *
∑ n ∈ Ns,
Real.exp ((2 : ℝ) * Real.pi * Real.exp (1 : ℝ) * X p n) +
∏ p ∈ S1,
(↑Ns.card : ℝ)⁻¹ *
∑ n ∈ Ns,
Real.exp
(-((2 : ℝ) * Real.pi * Real.exp (1 : ℝ)) * X p n)) /
Real.exp (1 : ℝ) ^ M ≤
δ) ∧
(3 : ℕ) ≤ w ∧
w ≤ R ∧
(2 : ℝ) ^ K * T ≤
Real.log (Real.log (↑R : ℝ)) - Real.log (Real.log (↑w : ℝ)) ∧
∑ p ∈ Finset.filter Nat.Prime (Finset.Ioc w R) \ S1,
(1 : ℝ) / (↑p : ℝ) ≤
(1 : ℝ) := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by t1023-f2, drafted with Claude Opus 5.5 (claude-opus-5-5); Aristotle (Harmonic) for Lemma 5.2, 2026-10-23; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall q \ge 1,\ T,\ \delta > 0,\ P_0\ \ \exists P \ge P_0,\ 2^K \le (\log P)^{2/3},\ H \le (\log P)^{2/3}\ \ \forall (p_0, v)\ \ \exists (N_s, S_1, S_2, M, \eta, w, R):\ \kappa_2, \kappa_3, \kappa_4, \kappa_5 \le \delta,\ \sum_{\varepsilon} \frac{1+\eta}{p_\varepsilon} \le \delta,\ \frac{q}{2^{K+1}} \le \delta,\ 2^K T \le \log\log R - \log\log w$
What is left of Tao–Teräväinen Theorem 5.1 (arXiv:2512.01739v2, p. 49) once the set-up is fixed: for every prime cube that Lemma 5.2 produces in (P/2, P], a random n (uniform on Ns) obeying (5.5)-(5.6) and (5.33), the prime split S₀/S₁/S₂ of §5.6 (S₁ avoids the discriminant of the near shifts), equidistribution (5.35) mod each p_ε and each p ∈ S₁ up to η, and the estimates κ₂ (§5.8), κ₃ (§§5.12-5.14, the paper's use of its Theorem 3.1(i)), κ₄ (§5.9), κ₅ (§5.10). The parameter clause 2^K T ≤ log log R - log log w is §5.11's (log₂R - log₂W)/2^K → ∞. Proved here, not in the hole: Lemma 5.2 (quantitative; Aristotle for t1023-f2, from t1022-s's and t1022-x's projects), Mertens' second theorem on S₁ (t1022-u), κ₁ (§5.7), (5.19), S₀ and the variance step (t1022-w's reduction), and the exact variance bound c₀ = q²/8 (t1023-f2).
Rendered from gloss/ff06d70085fc….md · Improve these words →
Rendered from targets/erdos-257/nodes/variant-6b364d2b--h1--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
e5f4b7b98ab5.import Mathlib theorem witness : ∃ (q : ℕ) (T : ℝ) (δ : ℝ) (P0 : ℕ), (0 : ℕ) < q ∧ (0 : ℝ) < δ := ⟨1, 0, 1, 0, Nat.one_pos, one_pos⟩
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).