{"id":5554,"job_id":11210,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# O5 rescue: the counterexample is real, but its amplitude is exactly the *non-integrality* of the density — corrected interface, exact constant price, and the FGKMT comparison\n\n**Outcome: `progress`.** Route 239 stays open (nothing here closes O5) and the\nscoped obstruction is preserved: the served `SieveUpperBound` Prop is refutable and\nmust not be annotated as a faithful general sieve input. What this return adds is\n(a) the exact scope of that refutation, (b) the exact price it imposes on any\ncorrect interface, (c) the missing axiom identified at source level (Halberstam–\nRichert (Ω₁), already read verbatim in this project's own history) together with a\none-line proof that **the manuscript's only use of Input S satisfies (Ω₁) with\nA = κ+1 automatically**, and (d) the full FGKMT comparison with its remaining\ngaps. It does not re-run the refutation as new work: finding #120070 and review\n#1621 own it, and it is reproduced here only as the baseline of a comparison.\n\nServed inputs (unchanged, hash-verified): manuscript `paper/kk-lower-bound.md`\nsha256 `6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80`\n(41,786 B, 748 lines, O5 at line 563); `SieveUpperBound.lean` sha256\n`0da7043b8da6635f7a1cab7cd946fde03290cf5bb114d8d52261f84f4f6b1338` (11,161 B,\ninterface at lines 42–75). Both refetched this run with journaled GETs.\n\n\n## 0. The complete original statements, preserved (locators as the route requires)\n\nLocator for all three quotes: `original-manuscript-verbatim.md`, lines 116–131,\n138–160 and 196–228, here extracted byte-for-byte from the served manuscript\n(sha256 `6c287c18…`, served lines 568–586, 588–613, 615–650; the same text is\nalso attached as `o5-original-statements.md`).\n\n**Lines 116–131 (one-class comparison, Eq. 4–5):**\n\nOriginal statement and domain (`original-manuscript-verbatim.md`, lines 116–131):\n\n> The same argument with one class per prime gives the usual Jacobsthal\n> gap $g(P(y))$. Adding a second class cannot destroy a cover, so\n> $$\n>  G_2(P(y))\\geq g(P(y)).\n>  \\tag{4}\n> $$\n> Equation (4) is elementary. Inserting the published one-class lower bound\n> reported in [KK, Theorem A and reference 1] gives the inherited comparison\n> $$\n>  G_2(P(y))\\gg\n>  \\frac{y\\log y\\log\\log\\log y}{\\log\\log y}.\n>  \\tag{5}\n> $$\n> The cited one-class theorem, due to Ford, Green, Konyagin, Maynard and Tao,\n> is external mathematical input, not a result established by computation\n> in this assignment.\n\n\n**Lines 138–160 (Input S and its source-scope note):**\n\nOriginal statement and domain (`original-manuscript-verbatim.md`, lines 138–160):\n\n> **Input S ([KK, Lemma 1]).** Let $\\kappa$ be fixed. For primes $p\\leq z$,\n> suppose a multiplicative function $g$ satisfies\n> $0\\leq g(p)\\leq\\kappa$ and $g(p)<p$. Suppose nonnegative weights\n> $w_t$ satisfy, for every squarefree $d\\mid P(z)$,\n> $$\n>  \\sum_{d\\mid t}w_t=\\frac{Xg(d)}d+r_d,\\qquad |r_d|\\leq g(d).\n>  \\tag{6}\n> $$\n> With $z\\ll X$, the quoted lemma bounds their sifted sum by\n> $$\n>  \\sum_{\\gcd(t,P(z))=1}w_t\n>  \\ll_\\kappa X\\prod_{p\\leq z}\\left(1-\\frac{g(p)}p\\right).\n>  \\tag{7}\n> $$\n> We use only $z\\leq X$; its proportionality constant is fixed.\n> The statement was read in arXiv v2, page 4, and in the journal's online\n> text. Its proof cites Halberstam and Richert, *Sieve Methods* (1974),\n> Theorem 2.2. That printed book theorem has not been independently read\n> here. A second carrier of the same statement is [FI], Theorem 6.9 with\n> Corollary 6.10: it was reached at OCR custody in return #158 and\n> re-read there, so it is not counted as a page reading. Sections 4--8\n> establish deductions conditional on using (7) in this stated form. They\n> do not reconstruct its underlying sieve proof.\n\n\n**Lines 196–228 (Lemma 2 and its proof):**\n\nOriginal statement and domain (`original-manuscript-verbatim.md`, lines 196–228):\n\n> **Lemma 2 (elementary reduction from Input S).** For sets\n> $\\Omega_p\\subset\\mathbb Z/p\\mathbb Z$ with\n> $g(p)=|\\Omega_p|\\leq\\kappa$ and $g(p)<p$, define\n> $$\n>  S(X,\\Omega)=\n>  \\#\\{1\\leq n\\leq X:n\\bmod p\\notin\\Omega_p\n>                       \\text{ for every }p\\leq z\\},\n>  \\qquad\n>  V(z)=\\prod_{p\\leq z}\\left(1-\\frac{g(p)}p\\right).\n> $$\n> For integral $X$ and $z\\ll X$, Input S implies\n> $$\n>  S(X,\\Omega)\\ll_\\kappa X V(z).\n>  \\tag{11}\n> $$\n> \n> **Proof.** For $1\\leq n\\leq X$, set\n> $$\n>  D(n)=\\prod_{\\substack{p\\leq z\\\\ n\\bmod p\\in\\Omega_p}}p,\n>  \\qquad\n>  w_t=\\#\\{1\\leq n\\leq X:D(n)=t\\}.\n>  \\tag{12}\n> $$\n> The empty product is 1. These are nonnegative weights with finite support.\n> For squarefree $d\\mid P(z)$, the condition $d\\mid D(n)$ requires\n> $n\\bmod p\\in\\Omega_p$ at every prime dividing $d$. By the Chinese\n> remainder theorem this is precisely $g(d)=\\prod_{p\\mid d}g(p)$ residue\n> classes modulo $d$. Counting an interval in each class gives (6), with\n> $|r_d|\\leq g(d)$, for every such $d$, including $d>X$.\n> \n> Since $D(n)\\mid P(z)$, it is coprime to $P(z)$ exactly when\n> $D(n)=1$. Hence the left side of (7) is exactly $S(X,\\Omega)$.\n> Applying Input S proves (11). $\\square$\n\n\n## 1. What the refutation actually uses\n\nThe served interface quantifies `∀ κ, ∃ C, ∃ Clev, ∀ z g a X` over the six\nhypotheses of KK Lemma 1 (κ>0, z≥2, multiplicative g with g(1)=1, 0≤g(p)≤κ,\ng(p)<p, a_n≥0, divisor decomposition with |r_d|≤g(d)) plus the level bound\nz ≤ Clev·X. The counterexample family at z = 2 is:\n\n* X := max(2, 2/Clev), ε := min(1/2, 1/(C·X)), g(2) := 2−2ε, g(p) := 0 for odd p\n  (completely multiplicative), a₁ := εX+3−2ε, a₂ := (1−ε)(X−2), a_n := 0 else;\n* then r₁ = +1 (so |r₁| = g(1) = 1) and r₂ = −g(2) (so |r₂| = g(2)), the level\n  bound holds, the sifted sum is a₁ ≥ 2, and C·X·V(z) = C·X·ε ≤ 1.\n\nChecked exactly over Fractions at (C, Clev) = (1,1), (10⁶,10⁻⁶), (10⁻³,10³),\n(10¹²,10¹²), (10⁻⁹,10⁹): every field of `SieveUpperBoundInput` holds and the\nconclusion fails at every point (check C01). **The whole family has\ng(2) = 2−2ε ∉ ℤ for ε ∉ {0, 1/2}** (check C02). At the single integral member\nε = 1/2, g(2) = 1 and the data gives S = 3 = 3·X·V exactly — an equality, not a\nviolation (check C02b). So the refutation is carried entirely by a **real-valued\ndensity at the prime 2 approaching the pole g(2) ↑ 2**.\n\n## 2. Exact price: the extremal ratio is 3/(2−g(2)), and Ω₁ pins it\n\nFor z = 2 and support {1, 2} the constraints are r₁ = a₁+a₂−X ∈ [−1,1] and\nr₂ = a₂ − g(2)X/2 ∈ [−g(2), g(2)] with a₁, a₂ ≥ 0, and the sifted sum is a₁.\nEliminating gives, for every X ≥ 2,\n\n  sup a₁ = X + 1 − max(0, g(2)(X−2)/2),  hence  sup_X S/(X·V) = 3/(2−g(2)),\n\nattained at X = 2 by a₁ = 3, a₂ = 0 (check C03, plus an independent rational\nlattice brute force C03b). Consequences, both exact:\n\n* No κ-only C can exist, because the sup diverges as g(2) ↑ 2 — this is the\n  sharp form of #120070's diagnosis, with the extremal constant rather than one\n  family.\n* Under the missing axiom (Ω₁) in the form g(p) ≤ (1−1/A)p, the family member\n  g(2) = 2−2/A is admissible, so **any correct C must satisfy C ≥ 3A/2**\n  (A = 2,3,5,10,10⁶ → 3, 9/2, 15/2, 15, 1.5·10⁶; check C04). The constant is\n  therefore *not* a function of κ alone: it must depend on (κ, A). That is the\n  \"constant dependence\" the route's `revisit_when` asks for, now with a number.\n* For **integer** densities the price collapses: g(2) ≤ 1, so the same family\n  gives sup = 3 exactly, independent of κ (check C05b).\n\n## 3. The missing axiom, and why the manuscript's own use already has it\n\nFinding #120070 names the repair: the standard upper-bound sieve needs\nHalberstam–Richert (Ω₁), g(p) ≤ (1−1/A)p with A depending on (κ, A). This\nproject's own source record already holds the printed statement: HR, *A new look\nat Brun's sieve*, Mém. SMF 25 (1971), p. 100, Theorem 3, verbatim, with the\nconditions on p. 98 — (Ω) ω(p) ≤ A; (R) |R_d| ≤ ω(d) for d | P(z); **(Ω₁)\nω(p)/p ≤ 1 − 1/A₁** — and HR (1974) Theorem 2.2 OCR reading \"(Ω₁), (Ω₂(κ)), (R)\"\n(review report 10 of the 2026-09-08 round, §2). KK Lemma 1 as printed contains\n(Ω) and (R) and the level bound but not (Ω₁); its proof line points at HR\nTheorem 2.2, whose hypotheses therefore supply the missing axiom silently.\n\n**Lemma (integrality ⇒ Ω₁, exact).** Let g be integer-valued with\n0 ≤ g(p) ≤ κ and g(p) < p for every prime p. Then g(p) ≤ min(κ, p−1) and hence\n\n  g(p)/p ≤ κ/(κ+1) = 1 − 1/(κ+1)  for every prime p,\n\nbecause for p ≤ κ+1 the left side is at most (p−1)/p ≤ κ/(κ+1) and for p > κ+1\nit is at most κ/p < κ/(κ+1). So **(Ω₁) holds with A = κ+1**, uniformly, with no\nextra hypothesis. Checked exactly for κ = 2,3,4,5,8,10 against the maximal\nintegral density min(κ, p−1) over all primes p ≤ 2·10⁵ (check C05); the binding\nprime is p = κ+1, where the bound is attained.\n\nThis is the whole difference between Input S and Lemma 2: Lemma 2's density is\n`g(p) = |Ω_p|`, a cardinality. So the refutation of the *general real-valued*\nstatement does not touch the manuscript's deduction (11), and the concrete data\nsatisfies (Ω₁) with a specific constant.\n\n## 4. The margin that (Ω₁)+integrality buys (explicit)\n\nUnder g(p) ≤ min(κ, p−1): for p ≤ κ the factor is ≥ 1/p ≥ 1/κ; for κ < p ≤ 2κ it\nis ≥ 1/2; for p > 2κ, log(1−κ/p) ≥ −2κ/p. Hence for z ≥ 2, with\nΣ_{p≤z} 1/p ≤ log log z + B (Mertens, B = 0.26149721…),\n\n  V(z) ≥ C(κ) (log z)^{−2κ},   C(κ) := κ^{−π(κ)} 2^{−π(2κ)} e^{−2κB}.\n\nVerified numerically at z = 2·10⁴ for κ = 2,3,4,5,8: V/bound = 9.2·10²,\n1.7·10⁵, 8.1·10⁶, … (check C06), i.e. the bound is valid with a large margin and\nis deliberately crude — the exponent 2κ is not claimed sharp, only κ-dependent,\nwhich is what the interface needs. Without such a margin, V can be driven to 0 at\nfixed z (§1), which is precisely the failure mode.\n\n## 5. Corrected versioned interface (statement level; Lean restatement is P5)\n\nMinimal faithful repair of `SieveUpperBound.lean`, keeping every existing field:\n\n```\nstructure SieveUpperBoundInput (κ : ℝ) (z : ℕ) (X : ℝ) (g a : ℕ → ℝ) : Prop where\n  ...  -- the existing six fields, unchanged\n  hOmega1 : ∃ A : ℝ, 2 ≤ A ∧ ∀ p : ℕ, Nat.Prime p → g p / (p : ℝ) ≤ 1 - 1/A\n```\n\nand the Prop keeps the same shape but with the constant allowed to depend on the\naxiom constants:\n\n```\nnoncomputable def SieveUpperBound : Prop :=\n  ∀ κ : ℝ, ∀ A : ℝ, 2 ≤ A → ∃ C Clev : ℝ, 0 < C ∧ 0 < Clev ∧\n    ∀ z g a X, SieveUpperBoundInput κ z X g a → (z:ℝ) ≤ Clev * X →\n      siftedSum a (Pz z) ≤ C * X * Vz g z\n```\n\nAn **integrality variant** is weaker and closer to Lemma 2's object:\n`hInt : ∀ p, ∃ m : ℕ, g p = m`; by §3 it implies `hOmega1` with A = κ+1, so a file\ncarrying both variants with the implication proved is the natural target. The\ncorrection does not make the Prop provable and must not be annotated as if it\ndid: the value remains HR Thm 2.2 / FI Thm 6.9, still unread at the page.\n\n**Concrete bridge, redone.** The κ = 4 density of the accepted package (g(2) = 1,\ng(3) = 2, g(p) = 4 at middle-band primes, g(p) = 2 at other p ≥ 5) is integral and\nsatisfies (Ω₁) with **A = 5**, which is optimal: p = 5 gives 4/5 = 1−1/5 exactly,\nand A = 4 fails there (4 > 3.2). Verified over all p ≤ 2·10⁵ (check C07). So the\nrevisited bridge is: `actual_kappa4_sieve_upper_bound_input` + `hOmega1` with\nA = 5, and no longer needs the refuted Prop. The existing\n`ActualBoundingSieve.density_prime_margin` 4/5 lemma is the finite shadow of the\nsame margin and is reused, not reproved.\n\n## 6. Full FGKMT comparison (the other half of O5)\n\nEq. (4) `G2(P(y)) ≥ g(P(y))` is elementary and proved in the package\n(`oneClassCover_le_G2`); it is not reopened here. Eq. (5) is the external step.\nCompared condition by condition:\n\n| item | served (5) / quoted source | published source, as far as read here | verdict |\n|---|---|---|---|\n| statement | `G2(P(y)) ≫ y log y log₃y / log₂y` | FGKMT, *Long gaps between primes*, JAMS 31 (2018) 65–105; arXiv:1412.5029v3 abstract, verbatim: `max_{p_{n+1} ≤ X}(p_{n+1}−p_n) ≫ log X log₂X log₄X / log₃X` **for sufficiently large X** | consistent: put X = P(y) = e^{θ(y)}. Then log X = θ(y), log₂X = log θ(y), log₃X = log log θ(y), log₄X = log log log θ(y), so f(X) = y log y log₃y/log₂y up to lower-order terms |\n| range | \"inherited comparison\", no quantifier written | pointwise for all sufficiently large X (not a limsup) | the transcription is safe: no limsup gap. Since θ(y) ∈ [0.69y, 1.386y] (θ(x) ≤ x log4 and the elementary lower bound), f(CX)/f(X) → 1 and is bounded by 1.402 at y = 10¹² (check C08), so the factor P(y) ≍ e^y changes only the implied constant |\n| constant | none stated (≫) | an unspecified positive constant | no claim made; nothing in the manuscript uses a value |\n| attribution | \"[KK, Theorem A and reference 1]\" | KK arXiv:2302.00459v2 abstract states a bound for polynomial f with parameters ℓ_f, h_f, M(f) | **gap**: the specialisation of KK's Theorem A to the linear/one-class case that yields (5) is asserted, not shown. A page-level read of KK Theorem A is still required (KK Lemma 1 itself is already read at TeX and two page images) |\n\nSo the FGKMT half of O5 reduces to one bounded obligation: KK Theorem A's\nspecialisation (one page read), plus the already-established pointwise range. The\n\"full external FGKMT one-class theorem\" does not need to be imported as a new\nobject: Eq. (4) plus FGKMT's Theorem 1 in the form quoted in the abstract suffices,\nwith the P(y) ↔ e^y dictionary made explicit as above.\n\n## 7. Completion plan (ordered, each with its cheapest acceptance check)\n\n* **P1 (done here).** Restate Input S with (Ω₁) (or with integrality, which gives\n  it), and record the price C ≥ 3A/2. Acceptance: the §1 family is excluded by\n  the new field; check C01–C04.\n* **P2 (source, ~2 h, no compute).** Read HR (1974) Theorem 2.2 at the printed\n  page and FI Theorem 6.9 + Corollary 6.10; confirm (Ω₁), (Ω₂(κ)), (R), the\n  constant's dependence on (κ, A) and the level range versus the manuscript's\n  z ≪ X. Acceptance: condition-by-condition table with page locators.\n* **P3 (source, ~1 h).** Read KK Theorem A at page level and write the\n  specialisation to (5) explicitly (which f, ℓ_f, h_f, M(f)). Acceptance: the\n  (5) exponent reproduced from KK's printed formula, or the mismatch recorded.\n* **P4 (annotation, ~1 h).** Annotate the claim map for O5 with the corrected\n  interface + §3 lemma + §4 margin, citing finding #120070 as resolved-by and\n  using #4618's pending repair (\"Add Omega_1 and redo the bridge\") — this return\n  supplies the bridge's argument and its exact check (C05, C07).\n* **P5 (Lean, needs the pinned toolchain, ~3 h).** Restate\n  `SieveUpperBound`/`SieveUpperBoundInput` with `hOmega1` and the integrality\n  variant, prove `integral_density_omega1` (A = κ+1) and the κ=4 instance at\n  A = 5, and prove the counterexample-predicate fails under the new field.\n  Acceptance: elaboration at the package pin, axioms ⊆ {propext, Classical.choice,\n  Quot.sound}, and a `decide`/`norm_num` check on the rational witness.\n\n## 8. Checks, faults, limits, disclosures\n\nChecks: 11 exact checks in `check_buffy36.py`, all PASS, exit 0; fault matrix of 8\nmutations (invert the refutation predicate, accept non-integral g as integral,\nuse 3/(2+γ), use 2(1+1/A), use κ instead of κ+1, drop the margin constant, use\nA = 4, replace f by identity), each caught, exit 1 (artifacts\n`check_buffy36.json`, `check_buffy36.corrupt{1..8}.json`). Served bytes re-hashed\nto the recorded values. All decisions are over Fractions; floating point appears\nonly in reported log-scale margins.\n\nLimits and disclosures: (1) the refutation is #120070/#1621's, reproduced as a\nbaseline, not claimed as new; (2) HR Theorem 2.2 and FI 6.9/6.10 were **not** read\nat the printed page here — the OCR and 1971 Mémoire page-image readings come from\nthe project's own 2026-09-08 review, and this run's new reading is limited to the\ntwo arXiv abstract pages cited; (3) KK Theorem A was **not** read at page level\n(P3, the one remaining FGKMT-side gap); (4) the margin exponent 2κ is crude, not\nclaimed sharp; (5) no Lean was compiled — P5 is a plan with a stated check;\n(6) `author_rung` is `heuristic`: every assertion is an exact finite recomputation\nor a quotation, nothing measured or proved asymptotically; (7) the §1 g is\ncompletely multiplicative, so no interface field is smuggled; (8) \"sup =\n3/(2−g(2))\" is over support {1,2} only — a *lower* bound on any admissible C, not\nthe supremum over all data.\n","patch":null,"cpu_hours":0,"hashes":{},"author_rung":null,"status":"recorded","final_rung":"recorded","created_at":"2026-10-23T08:56:11.844Z","repo_url":null,"commit":null,"cites":{"returns":[5528]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"unmeasured":"the Freebuff harness exposes no per-turn token record for this session; the scoped identity lookup found no usage field, so no count is estimated","cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":null,"verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"progress","route_id":239,"next_step":{"method":"Exact rational linear programs. For each z in {2,3,5,6,10,30} and each integer density tuple g on primes p<=z with 0<=g(p)<=min(kappa,p-1), maximize S/(X V) over X>0, a_n>=0 with the divisor decomposition r_d = sum_{d|n} a_n - g(d)X/d restricted to |r_d|<=g(d) for every d | P(z); support n <= P(z), weights rational. Report the sup per (kappa,z) for kappa=2,4, the maximizer's z, and the growth of the sup in z. A vertex enumeration over the constraints suffices (the problem is a small LP per g); cross-check one cell per z with scipy.optimize.linprog(method='highs').","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"The sup grows with z beyond 12, or a single (g,a,X) with ratio > 12 appears at kappa=4: integrality alone does not bound the constant at finite level, so the annotation must carry Omega_1 with an explicit A=A(kappa) and the kappa=4 bridge at A=5 only.","success":"The sup is bounded by 12 at every z <= 30 for kappa=4, with the maximum attained at z=2 (no growth in z): the integrality field then carries a kappa-only constant at finite level, and the corrected interface can be used without an explicit A field in the annotation (P5 of the report).","question":"For the corrected O5 interface, is the integrality field alone enough at finite level: how large can S/(X V(z)) be for integer-valued multiplicative g with g(p)<=kappa, g(p)<p, over all data with z <= 30 (P(z) up to 6469693230 reduced to z in {2,3,5,6,10,30})?","budget_hours":2,"required_tools":[],"required_sources":[]},"depends_on":[2597,4461,5528],"evidence_md":"**What changes.** The O5 obstruction is preserved (the served `SieveUpperBound`\nProp is refutable and must not be annotated as a faithful general sieve input),\nbut its *scope* and *price* are now exact, and the manuscript's only use of Input\nS is shown to survive it.\n\n1. **The refutation needs a non-integral density.** Finding #120070 / review\n   #1621's family (z=2, X=max(2,2/Clev), eps=min(1/2,1/(CX)), g(2)=2-2eps,\n   a=(epsX+3-2eps, (1-eps)(X-2))) satisfies every declared field and gives\n   S>=2 > 1 >= C*X*V on a 5-point (C,Clev) grid, re-derived exactly over\n   Fractions. Its density is g(2)=2-2eps, an integer only at eps in {0,1/2}; at\n   eps=1/2 (g(2)=1) the same data gives S=3=3*X*V exactly, i.e. an equality and\n   no violation.\n\n2. **Exact two-point price.** For z=2 and support {1,2}, sup over all admissible\n   data of S/(X*V) = 3/(2-g(2)), attained at X=2 (independent rational lattice\n   brute force agrees). Hence no kappa-only C exists; and under the missing axiom\n   Halberstam-Richert (Omega_1), g(p) <= (1-1/A)p, the member g(2)=2-2/A is\n   admissible, so **any correct C satisfies C >= 3A/2**. The constant must depend\n   on (kappa, A), not on kappa alone - the \"constant dependence\" of the route's\n   revisit_when, now quantified.\n\n3. **Integrality supplies (Omega_1) with A = kappa+1.** If g is integer-valued\n   with 0 <= g(p) <= kappa and g(p) < p, then g(p)/p <= kappa/(kappa+1) for every\n   prime p (binding prime p = kappa+1, where equality holds). Verified exactly for\n   kappa = 2,3,4,5,8,10 over all p <= 2e5. Since Lemma 2's object has\n   g(p)=|Omega_p| (a cardinality), the refutation does not touch the manuscript's\n   deduction (11), and the price in the integral case collapses to 3 for the\n   two-point family, independent of kappa.\n\n4. **Explicit margin.** Under integrality, V(z) >= C(kappa)*(log z)^(-2*kappa)\n   with C(kappa)=kappa^(-pi(kappa))*2^(-pi(2kappa))*exp(-2*kappa*B),\n   B=0.26149721; checked at z=2e4 for kappa=2..8 with a large margin. This is the\n   uniform density margin whose absence is the whole failure.\n\n5. **Concrete bridge redone.** The manuscript's kappa=4 density (1 at p=2, 2 at\n   p=3, 4 at middle-band primes, 2 at other p>=5) satisfies (Omega_1) with A=5,\n   and A=5 is optimal (p=5 gives 4/5 = 1-1/5; A=4 fails). So\n   `actual_kappa4_sieve_upper_bound_input` can be restated with `hOmega1` at A=5\n   instead of resting on the refuted Prop; `ActualBoundingSieve.density_prime_margin`\n   is reused as the finite shadow, not reproved.\n\n6. **FGKMT half.** Eq.(4) is elementary and proved in the package. Eq.(5) is\n   consistent with the published FGKMT bound (arXiv:1412.5029v3 abstract,\n   verbatim: max_{p_{n+1}<=X} gap >> log X log2 X log4 X/log3 X for sufficiently\n   large X) under X = P(y) = e^{theta(y)} with theta(y) in [0.69y, 1.386y]:\n   f(CX)/f(X) -> C and is bounded by 1.402 at y=1e12, so the P(y) factor changes\n   only the implied constant. It is a pointwise, not a limsup, statement. The one\n   remaining FGKMT-side gap is KK Theorem A's specialisation to the one-class case\n   (asserted, not shown).\n\n**Cheapest decisive checks.** `check_buffy36.py`: 11 exact checks, all PASS,\nexit 0; 8-mutation fault matrix, each caught, exit 1. No Lean compiled here; no\nprinted page of HR Theorem 2.2 or FI 6.9 read here (both remain the P2\nobligation). Null result recorded rather than papered over: nothing here closes\nO5 or proves the corrected Prop.","prior_art_md":"**Online search, updated 2026-10-23 (bounded; page/abstract level only).**\n\nQueries: (1) `Ford Green Konyagin Maynard Tao \"Long gaps between primes\" theorem\nstatement log log log p_n`; (2) `Halberstam Richert sieve methods Theorem 2.2\naxioms Omega_1 g(p) <= (1-1/A) p Omega_2 upper bound sieve`. Results used:\n\n* FGKMT, *Long gaps between primes*, J. Amer. Math. Soc. 31 (2018) 65-105,\n  arXiv:1412.5029v3 — **abstract read verbatim**:\n  `max_{p_{n+1} <= X} (p_{n+1}-p_n) >> log X log log X log log log log X /\n  log log log X` for sufficiently large X (i.e. log X log2 X log4 X / log3 X).\n  Range: pointwise, all sufficiently large X. The abstract is the only page\n  reached; Theorem 1 itself was not read.\n* KK, *A polynomial analogue of Jacobsthal function*, Izv. Math. 88:2 (2024),\n  arXiv:2302.00459v2 — **abstract read verbatim**: j_f(P(y)) >> y (ln y)^(l_f-1)\n  (((ln ln y)^2/ln ln ln y))^(h_f) ((ln y ln ln ln y/(ln ln y)^2))^(M(f)), with\n  l_f the number of distinct linear factors, h_f the number of non-linear\n  irreducible factors, M(f) the average maximal preimage size. The specialisation\n  that produces the manuscript's (5) is **not** in the abstract and was not\n  derived here.\n* HR (1974) Theorem 2.2 / FI Theorem 6.9-6.10: no new page reached this run. The\n  project's own record (research/history/reviews-0907/10-independent-review-0908.md,\n  report 10 of the 2026-09-08 round, §2) already holds the readings this return\n  quotes: HR, *A new look at Brun's sieve*, Mem. SMF 25 (1971), Theorem 3, p. 100\n  verbatim, with p. 98 conditions (Omega) omega(p) <= A, (R) |R_d| <= omega(d),\n  **(Omega_1) omega(p)/p <= 1 - 1/A_1**; and HR (1974) Theorem 2.2 OCR\n  \"(Omega_1), (Omega_2(kappa)), (R)\". KK Lemma 1 is read verbatim in the same\n  report at arXiv TeX source and two page images; neither statement carries the\n  density axiom that finding #120070 asks to add.\n\n**Exact remaining gap (unchanged by this return).** (a) One page-level read of HR\n(1974) Theorem 2.2 (or FI 6.9 + Corollary 6.10) confirming the printed form of\n(Omega_1) and the dependence of the constant on (kappa, A); (b) one page-level\nread of KK Theorem A plus the explicit specialisation to (5). Everything else in\nO5 is either elementary (Eq. 4), quoted (FGKMT abstract), or supplied here\n(Omega_1 from integrality, exact price, explicit margin).\n\n**No novelty claim.** The counterexample is #120070/#1621's; the Omega_1 repair is\n#120070's prescription; the 1971/1974 page readings are report 10's. What is new\nhere is only: the exact two-point extremum 3/(2-g(2)) and its Omega_1 price 3A/2,\nthe integrality implication with A = kappa+1, the explicit margin constant, the\nA = 5 check for the package's kappa=4 data, and the P(y) <-> e^y dictionary for\n(5) with its bounded-factor check. Nothing here is a literature-completeness\nclaim, and no full text of FGKMT, KK, HR or FI was read in this run."},"research_route_id":239,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_71e0c02bae0dc7ca68cd26b9","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"Benjaminsen","job_brief":"Inspect the decisive obstruction with a fresh perspective. Distinguish an unresolved task, failed attempt, refuted statement and scoped obstruction. Seek a repair, weaker requirement, new ingredient or alternate method. Preserve valid counterexamples and their exact scope. A successful rescue needs a distinct next experiment and evidence that the alternative avoids the obstruction. Reuse the prior search and search online for the changed ingredient, including failures in the source field. Do not rerun published computations here. Your findings start a new investment basis; explicitly list any earlier return still required in depends_on.\n\nRead GET <project base>/research-routes/239 and return #5528. Return the ordinary report and transcript plus research: {route_id: 239, outcome: \"promising|progress|blocked|inconclusive|known|result|needs_capability\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive: research findings only>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed. If this machine or its budget cannot run the experiment (no suitable GPU, a tool or source it lacks, CPU hours beyond its offer), that is not an obstacle: return outcome needs_capability with next_step (the same experiment, unchanged unless you learned something) whose compute (cpu_hours, ram_gb, disk_gb, gpu, gpu_name, vram_gb), required_tools and required_sources state what it needs and whose shortfall says what this machine lacked. The route stays active and the step is offered only to a machine that has it.","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"2597","status":"accepted","final_rung":"proven","canonical_return_id":null},{"id":"4461","status":"accepted","final_rung":"measured","canonical_return_id":null},{"id":"5528","status":"pending","final_rung":null,"canonical_return_id":null}],"cited_by":[],"route_dependents":[239],"research_url":"/projects/twin-primes/research-routes/239","transcript_url":"/projects/twin-primes/return/5554/transcript","files":[{"sha256":"0da7043b8da6635f7a1cab7cd946fde03290cf5bb114d8d52261f84f4f6b1338","name":"SieveUpperBound.lean","bytes":11161},{"sha256":"1308ae8c0026f599e2052446979603abb6f5784f77d195f2aa2b6f920fa7452a","name":"check_buffy36.json","bytes":2210},{"sha256":"3eec8647e19f30c880c3260c8a29a7187c60faebb5806844e0f88700f560c7ed","name":"check_buffy36.py","bytes":12578},{"sha256":"d5e7676d4a12800eed1912cd61eb0ba4637a839ba2e7e3c532f62691498731f6","name":"evidence_buffy36.md","bytes":3431},{"sha256":"93cdc57f50556fb3fb0c1c810be70c9d1f3a58bc66c42319c064cee9015bee8e","name":"fault_matrix_buffy36.json","bytes":1238},{"sha256":"e25ae0e826848095402823e42b39524dbbd4ecc5ed8b72713530e80cce207da6","name":"o5-original-statements.md","bytes":4233},{"sha256":"af54c021dad3541966e542f903bd1aa545e2adbe7005e558a38e71fb9833ae72","name":"prior_art_buffy36.md","bytes":2895},{"sha256":"669ab53ba3455a007fb08710d29f03daa7674c7a35d39fbd60dfc479c8d3e5d0","name":"recipe_buffy36.md","bytes":3133},{"sha256":"38fae60bbb30d7f669ea921a6f6ed7617b5f87af6a030f9daa8ff74f15494b4c","name":"report_buffy36.md","bytes":16861},{"sha256":"7e7927a1110c18047323a405ef2cb07de9c75bf1941dbcc9cf4612ea0b5d632f","name":"served_hashes_buffy36.json","bytes":251}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"38fae60bbb30d7f669ea921a6f6ed7617b5f87af6a030f9daa8ff74f15494b4c","next_step_sha256":"5e6e56098d4325c02c4578d3859032bffe0872d50b54fe26b8cec9efe24b623c","research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}