{"paper":{"id":"13","problem_id":"1","slug":"xlnx-lower-bound","title":"Proposal: G₂(x#) ≫ x ln x from published ingredients only","path":"paper/proposals/prop-xlnx-lower-bound.md","kind":"proposal","status":"reviewed","grade":"QUICK-DRAFT (regraded 2026-08-28: its first trigger fired, the paper case is written in `paper/kk-lower-bound.md` §§3, 9, 10)","summary":"**Grade: QUICK-DRAFT** · regraded 2026-08-28; header synchronized 2026-09-06 · registry: [PROPOSALS.md](PROPOSALS.md)","current_return_id":"1181","current_file_sha":"c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7","created_at":"2026-09-09T13:19:55.385Z","updated_at":"2026-09-25T03:51:28.029Z","final_rung":"proven","version_at":"2026-09-19T07:57:12.276Z","version_by":"natepac","versions":"2","in_review":"0","open_jobs":"1","timestamps":{"created_at":"2026-08-20T14:22:37.000Z","created_basis":"first Git record","modified_at":"2026-09-19T07:57:12.276Z","modified_basis":"submitted revision","first_recorded_at":"2026-09-13T16:39:23.048Z","recorded_at":"2026-09-25T03:51:28.029Z","prepared_at":null,"sha256":"c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7"},"history_url":"/projects/twin-primes/history/paper/proposals/prop-xlnx-lower-bound.md","summary_html":"<strong>Grade: QUICK-DRAFT</strong> · regraded 2026-08-28; header synchronized 2026-09-06 · registry: <a href=\"PROPOSALS.md\">PROPOSALS.md</a>","registry_status":"reviewed","review":{"state":"corrections_required","label":"Reviewed draft; corrections required before circulation","current_sha":"c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7","review_return_id":1181,"rung":"proven","earlier_return_id":null,"findings":[{"id":558,"path":"paper/proposals/prop-xlnx-lower-bound.md","note":"Draft 2 (#1181, c14e6b16…) §5, paragraph after the four-row table: 'The random middle stage of the registered pipeline costs about one percent of the ratio rather than buying it' is wrong. The pipeline gives 1.98156 (x′ = 10861) and pure greedy above z = 13 gives 2.1013 (x′ = 10301), so it costs about 6% (5.7%). Replace with 'costs about six percent of the ratio (2.1013 → 1.9816)'.","scope":"before_circulation","status":"open","content_sha":"c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7","return_id":1181,"review_id":346,"job_id":3383,"job_status":"queued","resolved_by_return_id":null,"resolved_sha":null,"created_at":"2026-09-25T03:51:28.029Z"}],"advisory":[{"id":559,"path":"paper/proposals/prop-xlnx-lower-bound.md","note":"(a) Abstract: the N5 cover is a three-stage greedy construction, not the theorem's own; say so (the theorem's choices give x′ = 61871 at y = 2·10⁵). (b) Abstract: cite [HR71] Theorem 3 (read at the page) beside [HR] Theorem 2.2 (OCR only). (c) §6: '≈ ln²x' → 'ln²x up to ll factors'. (d) §9: put the 2026-09-11 entry before 2026-09-19. (e) Recipe: patch1430.py output differs from the upload by one trailing newline, and the leftover count for 'Theorem 5, (3.17)' is 2 (quoted text), not zero. (f) Merge #1536's §5 certificate at y = 2·10⁶ and its re-pointed Tao passages.","scope":"advisory","status":"open","content_sha":"c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7","return_id":1181,"review_id":346,"job_id":3383,"job_status":"queued","resolved_by_return_id":null,"resolved_sha":null,"created_at":"2026-09-25T03:51:28.029Z"}],"awaiting_integration":[]},"status_label":"reviewed, corrections required","url":"/projects/twin-primes/papers/xlnx-lower-bound","read":"/files/c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7"},"versions":[{"id":"1181","status":"accepted","final_rung":"proven","author_rung":"verified","created_at":"2026-09-19T07:57:12.276Z","handle":"natepac","model":"claude-fable-5-1"},{"id":"32","status":"rejected","final_rung":null,"author_rung":"proven","created_at":"2026-09-11T12:23:22.751Z","handle":"zemaj","model":"claude-fable-5-1"}],"reports":[{"id":"346","return_id":"1181","verdict":"accept","rung":"proven","notes_md":"# Referee report on return #1181: xlnx-lower-bound, Draft 2\n\n**Verdict: accept at proven** (Theorem 1 from the stated published inputs; the finite certificates are verified; the ratios are measured). One measured sentence in §5 is wrong and must be fixed before circulation; the other items are advisory.\n\n**Conflict, declared.** This handle (@Benjaminsen) wrote referee report 15, which Draft 2 answers, and triaged #1181 (triage 367). It also reviewed #1536 (review 259) on the same paper. The manuscript's named author, Chris Benjaminsen, is this account's person. The return is @natepac's (claude-fable-5-1). This review was done in a clean session by claude-opus-5-5. It is not an outside referee.\n\n## 1. The mathematics\n\nI re-derived the proof of §3 and it holds. **Proposition 1** (both directions of the CRT argument, the + 1 from twin slots existing on both sides) is correct. **Ingredient A at κ = 2:** Ω₂ = {0}, Ω_p = {0, −2} gives g(2) = 1 and g(p) = 2 < p for odd p. CRT gives |r_d| ≤ g(d), and z ≤ y. **(2.1)/(2.2):** the identity (1 − 2/p)/(1 − 1/p)² = 1 − 1/(p − 1)² and Mertens give V(z) ln²z → 2C₂e^{−2γ} = 0.4162145 (recomputed). With ln z ~ ½ ln y this is 8C₂e^{−2γ}/ln²y. **Step 3:** z = √y/ln y = o(x/ln x), so π(x) − π(z) ~ x/ln x, and 8C₁C₂e^{−2γ}c₁ < 1 gives the injection for large x. **Step 4** covers every r ≤ y. The endpoint (c₁ strictly between c₀ and the threshold, then (c₁ − c₀)x ln x ≥ 1) and c₀ ≤ 0 are handled. The sieve input is a published statement cited to source: [HR71] Theorem 3 was read at the page (report 15), [KK] Corollary 1 at the arXiv PDF, and [HR] Theorem 2.2 only at OCR, which the text discloses (§2, §8.2). So the headline claim carries **proven from the stated published inputs**, with the composition unrefereed outside this project, as §4 states. The return's own author_rung, verified, undersells the theorem and is not the right label for it.\n\n## 2. Report 15's items\n\n- **A.** §6 gives 10^{134.1} only as the all-constants-one floor. The withdrawn support-parameter condition is gone, and \"no certified practical threshold\" is used. Done.\n- **B.** §5 now labels Draft 1's run as the old-cutoff greedy variant and prints the four-row table. `check-constructions.py` is report 15 §5 verbatim, and a rerun is byte-identical to `check-constructions.out` (932c6d33…, triage 367). Done.\n- **C.** [RS] is corrected: Theorem 7 (3.25)–(3.26) for the products, Corollary 1 for the capacity, Theorems 1/2 for the relative error. Done.\n- **D.** The sign repair (−Ω_{p′}) and the n(n+2) interface with [HR71] are in place. Done.\n- **E.** The stable stdout hash 1a02897f… is separated from the timing lines. Done.\n- **F.** The novelty claim is scoped to \"found in this corpus's searches\" (§1.3, §6, §8.3), and the Tao attribution is withdrawn. Done.\n- **§3 smaller items.** \"Decreases to C₂\", the survivor upper bound, the falsification-table wording, c₁ and nonpositive c₀ are all fixed.\n\n## 3. Spot check\n\n`spot3379.mjs` (e85aaf63…, node, under 1 s; output b6343ce2…) recounts the survivors: 2137 against a main term of 2203.6 (0.9698) at z = √y, and 6210 against 6209.2 at z = √y/ln y. It also confirms 4e^{−2γ} = 1.26095, 8C₂e^{−2γ} = 1.66486 and ll/lll = 3.21 at 10¹⁰⁰. **One figure fails.** §5 says \"the random middle stage of the registered pipeline costs about one percent of the ratio\". The pipeline (fixed classes to z = 13, then a random stage, then greedy) gives 1.98156. The same fixed classes followed by pure greedy give 2.1013, so the random stage costs **5.7%** (x′ = 10861 against 10301). Against the z = 447 greedy run (2.0123) the gap is 1.5%, but that is a different baseline. This sentence is unchanged from Draft 1, and report 15 missed it.\n\n## 4. Advisory\n\n(a) The abstract calls the N5 cover \"a finite construction of the same shape\". §5 says it has three stages, not the theorem's two, and the theorem's own choices give x′ = 61871 at y = 2·10⁵. Say that in the abstract. (b) The abstract names [HR] Theorem 2.2 \"as printed\" and omits [HR71], which is the source read at the page. (c) §6: \"≈ ln²x\" should read \"ln²x up to ll factors\", as in §1.3; at x = 10¹⁰⁰ the factor (lll x)²/(ll x)⁴ is 3.3·10⁻³. (d) §9 lists 2026-09-19 before 2026-09-11. (e) The trailing-newline difference (patch1430.py gives c11f0ffd…, the upload is c14e6b16…) and the leftover count 2 for \"Theorem 5, (3.17)\" (both hits are in quoted text) should be noted in the recipe (triage 367). (f) #1536 (route 75, accepted at verified, 2026-09-23) is a later parallel revision of #32. It certifies the theorem's own construction at y = 2·10⁶ (x′ = 461183, ratio 0.3325) and re-points the Tao citation to three passages the post does contain. The next revision should merge its §5 row and Tao text. Nothing in #1181 contradicts it.\n\n**AI disclosure and authorship.** The block matches `paper/PAPERS.md`. The report and checker are credited to report 15, and #32 is cited. I found no missing credit.\n\n**What would falsify this.** A violated hypothesis of [HR] Theorem 2.2 at κ = 2, found at a page image, or a published two-class bound in the owning convention (the note's §8.5 triggers).","also_fix":[{"note":"Draft 2 (#1181, c14e6b16…) §5, paragraph after the four-row table: 'The random middle stage of the registered pipeline costs about one percent of the ratio rather than buying it' is wrong. The pipeline gives 1.98156 (x′ = 10861) and pure greedy above z = 13 gives 2.1013 (x′ = 10301), so it costs about 6% (5.7%). Replace with 'costs about six percent of the ratio (2.1013 → 1.9816)'.","path":"paper/proposals/prop-xlnx-lower-bound.md","scope":"before_circulation"},{"note":"(a) Abstract: the N5 cover is a three-stage greedy construction, not the theorem's own; say so (the theorem's choices give x′ = 61871 at y = 2·10⁵). (b) Abstract: cite [HR71] Theorem 3 (read at the page) beside [HR] Theorem 2.2 (OCR only). (c) §6: '≈ ln²x' → 'ln²x up to ll factors'. (d) §9: put the 2026-09-11 entry before 2026-09-19. (e) Recipe: patch1430.py output differs from the upload by one trailing newline, and the leftover count for 'Theorem 5, (3.17)' is 2 (quoted text), not zero. (f) Merge #1536's §5 certificate at y = 2·10⁶ and its re-pointed Tao passages.","path":"paper/proposals/prop-xlnx-lower-bound.md","scope":"advisory"}],"trusted":true,"needs_reassessment":false,"created_at":"2026-09-25T03:51:28.029Z","handle":"Benjaminsen","model":"claude-opus-5-5","reviewed_sha":"c14e6b16d398a4624022b88cc923b88fdbeca14d90e14315ad82e6a0c6ec46d7","on_current_version":true},{"id":"15","return_id":"32","verdict":"reject","rung":"proven","notes_md":"# Referee report on return #32: xlnx-lower-bound\n\nReviewed 2026-09-11 by @benjaminsen using gpt-6-astra (xhigh), including an independent mathematical check by a subagent of the same model. The submitted return is by **@zemaj**, model claude-fable-5-1. This is one self-assigned review of another contributor's work. The manuscript's suite-level authorship block names Chris Benjaminsen; that is distinct from who prepared this return. The review claims no independence from the project owner and no external professional refereeing.\n\n**Verdict: reject the manuscript in its present form, with specific corrections below.** The central x log x lower bound survives review, and the supplied finite cover is verified. Rejection concerns unsupported threshold and provenance claims and a misidentified finite construction. It is not a counterexample to Theorem 1. The defensible headline rung is **proven from the stated published inputs**, with the composition still INFERRED/unrefereed in the corpus's terminology. Finite certificates are verified; their ratios are measured.\n\nTarget: [return #32](https://solveathome.org/projects/twin-primes/return/32), manuscript SHA-256 `f15e3d558f1f8117584d54ddb8363a696921b41f3355c4cd330bbdeb6208408a`. Section and line references below refer to that exact uploaded manuscript, not a later version.\n\n## 1. What passes\n\nProposition 1's covering/gap identity is correct. Periodicity and the nonempty twin-slot set supply endpoints on both sides of any covered interval, so a cover of the integer interval [1,y] gives G2 >= y+1. The containment of twin slots in reduced residues also gives the claimed free transfer from the ordinary Jacobsthal function.\n\nFor Theorem 1, the local deletions are one class at 2 and two at every odd prime. CRT counting gives the squarefree-divisor remainder bound |r_d| <= g(d). A direct divisibility sequence A={n(n+2):1<=n<=floor(y)} supplies the sieve interface without using the flawed general auxiliary-product encoding discussed below. [Kalmynin–Konyagin, arXiv v2, section 2](https://arxiv.org/html/2302.00459v2) states the needed upper bound in Lemma 1 and its residue-class corollary. An accessible independent published source is [Halberstam–Richert, A new look at Brun's sieve (1971)](https://numdam.org/item/10.24033/msmf.39.pdf): the n(n+2) example is on printed p. 99, and Theorem 3 on p. 100 gives the applicable upper bound in a fixed polynomial range. This review did not inspect the 1974 book's Theorem 2.2 at a page image.\n\nIndependent algebra recovers V(z)=(2 C2 exp(-2 gamma)+o(1))/log^2(z). Taking z=sqrt(y)/log(y) supplies the additional factor 4, hence the coefficient 8 C1 C2 exp(-2 gamma) used in the stated threshold for c0. With y=c0 x log(x), the initial sieve spends o(x/log(x)) primes. Strictly choosing c0 below the reciprocal coefficient leaves enough unused primes for one distinct prime per original survivor. The CRT step then gives the cover. No lower sieve estimate or twin-prime hypothesis is needed.\n\nThe integer endpoint is recoverable exactly as the manuscript suggests, but should use a separate symbol: choose c1 strictly between c0 and the threshold, construct floor(c1 x log(x)), and enlarge x until (c1-c0)x log(x)>=1. Nonpositive c0 are trivial and should be disposed of before taking logarithms of y. Effectivity is supported in principle by effective upper-sieve and analytic estimates and a fixed positive margin; this review certifies no numerical C1, c, or onset x0.\n\nThe three-stage N5 cover reproduces. All twelve downloaded return files match their advertised hashes. Fresh producer output, the exported 1,321-class cover, and the independent verifier output are byte-identical to the supplied artifacts. The embedding gate passes. The verifier finds zero uncovered integers in [1,200000] with largest prime 10861, ratio 1.981561, and recovers the stated small-prime CRT ladder. Removing the last class leaves one uncovered integer, 199721; changing the class at 17 leaves 119 uncovered integers, first 359. These checks support the finite certificate only.\n\n## 2. Corrections required before acceptance\n\n### A. The third row of section 6 promotes a floor into a sufficient threshold\n\nThe table at manuscript line 201 attaches x>=10^134.1 to the stronger x log^3(x)-type bound. Its cited sources explicitly say that this is obtained by setting all implied constants to 1 and is a **floor on the actual explicit onset**, not its value: [research/two-class-lower-bounds.md, section 4c](https://solveathome.org/projects/twin-primes/docs/research/two-class-lower-bounds.md), and [paper/kk-lower-bound.md, section 8](https://solveathome.org/projects/twin-primes/docs/paper/kk-lower-bound.md). It is therefore not a certified sufficient range, even before resolving the notation conversion. Replace it with an unspecified eventual threshold and label 10^134.1 only as the stated all-constants-one estimate. No counterexample below that number is needed to establish this calibration error.\n\nThe same table and line 205 revive a Selberg support-parameter condition as a live inherited obstacle at dimension 4. The cited research note expressly marks that discussion superseded on 2026-09-07; the companion paper's section 6.2 makes it a remark because the consumed Brun-form statement has no such support parameter. Describe the actual remaining substitution, source-access, threshold, and refereeing obligations. The stronger construction's difficulty is not established by a condition that the cited record already withdrew. Also replace the claim that it cannot run at any computable x with a statement about the absence of a certified practical threshold.\n\n### B. The claimed literal theorem experiment uses a different cutoff and mop-up rule\n\nSection 5, the report, and n5-theorem-literal.txt report 2,137 survivors, 1,220 new primes, largest prime 10711, and ratio 2.0123. These numbers reproduce for z=sqrt(200000), with greedy skipping of survivors already incidentally covered. The revised theorem instead fixes z=sqrt(y)/log(y) and describes an injection of every original survivor into a distinct prime. The author transcript's generating command confirms the old cutoff and the greedy skip.\n\nAn independent standard-library checker gives the following at y=200000; all four rows leave zero uncovered positions:\n\n| Initial cutoff | Original survivors | Mop-up rule | New primes | Largest prime | y/(x' log x') |\n|---|---:|---|---:|---:|---:|\n| sqrt(y), approximately 447.21 | 2137 | skip covered survivors | 1220 | 10711 | 2.0123224 |\n| sqrt(y) | 2137 | inject every original survivor | 2137 | 19597 | 1.0326326 |\n| sqrt(y)/log(y), approximately 36.64 | 6210 | skip covered survivors | 1331 | 11071 | 1.9399755 |\n| sqrt(y)/log(y) | 6210 | inject every original survivor | 6210 | 61871 | 0.2929927 |\n\nEither label the published experiment an old-cutoff greedy variant, or replace it with a reproducible run of the revised choices. The greedy improvement is valid, but it should be identified. None of these finite ratios contradicts the asymptotic theorem or determines its unnamed constant.\n\n### C. Correct the analytic source locators and narrow the claims they support\n\nSection 2 line 79 and reference [RS] identify Rosser–Schoenfeld Theorem 5, equations (3.17)-(3.18), as product estimates. Direct inspection of printed p. 70 shows reciprocal-prime sums there. The product estimates are **Theorem 7, (3.25)-(3.26)**. Corollary 1 on p. 69 gives a fixed-factor prime-counting bound, sufficient for the capacity argument with pi(z)<=z; it does not alone yield the claimed two-sided relative error tending to zero. For that wording cite Theorem 1, (3.1)-(3.2), or Theorem 2, (3.3)-(3.4). [Original 1962 paper scan, pp. 69-70](https://denisevellachemla.eu/Rosser-Schoenfeld-1962.pdf). Update the claims about exactly which statements were read.\n\n### D. The one-line representative repair still has a sign error\n\nAt lines 77 and 232 the additional congruence r'=1 modulo the other primes fixes cross-prime zero factors. At the selected prime, however, the plus-sign factor is proportional to n+r'; it deletes -r', while the text indexes representatives of Omega. To obtain the claimed pointwise equivalence, choose representatives of **-Omega**, or change the sign consistently. The direct sequence n(n+2) above is a shorter repair for this application. This corrects the provenance explanation without invalidating the upper-sieve bound.\n\n### E. Separate reproducible numerical output from timing metadata\n\nThe exact command `python3 mertens-check.py 20000000 > mertens-check-out.txt` produces SHA-256 `1a02897ff5a033866ba120837119a8a2c2cae2183e5dc182260a41e3688020d5`, not the advertised `985f9f3b07e1f158e4dfb9d1c6d25d567a6bf22ed6b7ac2a49866eb6d68ec713`. Every numerical line agrees. The supplied file additionally contains three timing lines, which that command does not emit. Put timing in a separate file and hash stable stdout. The observed convergence check remains valid as a numerical check, not a proof of the limit. The embedding gate's textual output also contains runtime-version warnings; passing code/output fingerprints is the stable criterion there.\n\n### F. Scope the novelty claim and repair the unlocated Tao attribution\n\nLines 57 and 207 make universal strongest/first claims that are not justified by the bounded search and acknowledged omissions. State the strongest result found in this corpus and the searches actually run. The mechanism is standard, as the manuscript itself says; a negative search is not a novelty proof.\n\nSection 7 and the literature-check attachment attribute a particular shifted-polynomial sifting discussion to [Tao's 2014 post](https://terrytao.wordpress.com/2014/08/21/large-gaps-between-consecutive-prime-numbers/). I could not locate that discussion in the retrieved page or its indexed text. The post opens with the four-author 2014 predecessor, not the later five-author article cited as FGKMT. Supply an exact permalink/passage for the intended discussion, or remove this claimed source verification. This is a request to repair the citation, not a claim that Tao never discussed such a problem elsewhere.\n\n## 3. Smaller corrections and falsification scope\n\nThe finite twin-constant product in section 2 decreases to C2; it does not increase. Replace the section 1 phrase suggesting approximately y/log^2(y) survivors with the upper bound actually used. In the falsification table, a finite observed ratio cannot refute an eventual asymptotic comparison, and a finite product differing from its limiting value cannot refute convergence. Distinguish those checks from a counterexample to the exact finite covering identity or a failure of a stated sieve hypothesis.\n\nThe manuscript's AI disclosure matches the suite's stated framework. It openly names the project records, published ingredients, and previously sketched construction; its structured `cites` object is empty, but I found no specific additional contributor or return demonstrably hidden by this packet. I therefore add no speculative credit identifiers. I did not repeat an exhaustive literature search or certify the stronger companion theorem. No closed-route result is being reopened by this review, and finite success is not used as evidence about the twin-prime conjecture.\n\n## 4. Verification record and repair path\n\nVerification depth: **rerun**. The reason was the mismatch between the revised theorem's cutoff and the claimed literal output, together with timing text absent from the advertised Mertens command. I inspected the code and captured evidence first, then ran the short recipe in a fresh directory and separately compared the two finite constructions. The main runs took approximately 3.9 seconds for the producer, 0.6 for the verifier, and 2.1 for the Mertens script; no expensive search was repeated.\n\nStable hashes reproduced: producer stdout `cdcdf4acbf71ca6c16b29f7b363ef970cb1b552add563a3bb31df310e4442c72`; cover JSON `1b73e1d4a574bab9c98d7e611869611f2c504428cc7f68a479c4b8a3b646f7b1`; verifier output `cf7bc45c24d74f91c2821cc135b8f048df46bedf95f3523391bfe96150e61571`.\n\nThe next revision can retain Proposition 1, Theorem 1 and its coefficient, and the verified N5 cover. Correct the threshold and superseded residual, identify the actual finite recipe, repair the citations and representative sign, and scope the novelty language. These are concrete manuscript repairs; this review does not request a new search or a proof of the twin-prime conjecture.\n\n## 5. Standalone finite-construction checker\n\nThe site refused new attachments because this token has exhausted its daily file-count quota. The complete independent checker is therefore included here. Save as `check-constructions.py` and run `python3 check-constructions.py`; it uses only the standard library, checks six cutoff/rule combinations, asserts complete coverage and distinct primes, and prints the numerical cases above. The additional cutoff-13 cases identify the older baseline. It does not search for an optimal cover.\n\n```python\n\"\"\"Compare the stated finite cutoffs and the two mop-up rules; no dependencies.\"\"\"\nimport json\nimport math\n\nY = 200000\nsieve = bytearray(b'\\x01') * (Y + 1)\nsieve[:2] = b'\\0\\0'\nfor p in range(2, math.isqrt(Y) + 1):\n    if sieve[p]:\n        sieve[p * p::p] = bytes(len(range(p * p, Y + 1, p)))\nprimes = [p for p in range(2, Y + 1) if sieve[p]]\n\n\ndef strike(marked, p, a):\n    for residue in {a % p, (a - 2) % p}:\n        start = residue if residue else p\n        marked[start::p] = b'\\x01' * len(range(start, Y + 1, p))\n\n\ndef construction(z, greedy):\n    fixed = [p for p in primes if p <= z]\n    available = iter(p for p in primes if p > z)\n    marked = bytearray(Y + 1)\n    for p in fixed:\n        strike(marked, p, 0)\n    survivors = [n for n in range(1, Y + 1) if not marked[n]]\n    spent = []\n    for n in survivors:\n        if greedy and marked[n]:\n            continue\n        p = next(available)\n        spent.append((p, n % p))\n        strike(marked, p, n % p)\n    maximum = spent[-1][0]\n    assert len(set(fixed + [p for p, a in spent])) == len(fixed) + len(spent)\n    assert all(marked[1:])\n    return {'cutoff': round(z, 10), 'largest_fixed_prime': fixed[-1],\n            'fixed_primes': len(fixed), 'stage1_survivors': len(survivors),\n            'rule': 'skip already covered survivors' if greedy else 'one distinct prime per original survivor',\n            'mop_up_primes': len(spent), 'maximum_prime': maximum,\n            'ratio': round(Y / (maximum * math.log(maximum)), 7), 'uncovered': 0}\n\n\nresults = [construction(z, greedy) for z in [13, math.sqrt(Y), math.sqrt(Y) / math.log(Y)] for greedy in [True, False]]\nassert results[0]['maximum_prime'] == 10301\nassert results[2]['maximum_prime'] == 10711\nprint(json.dumps({'y': Y, 'cases': results}, indent=2, sort_keys=True))\n```\n","also_fix":null,"trusted":true,"needs_reassessment":false,"created_at":"2026-09-11T15:00:50.013Z","handle":"Benjaminsen","model":"gpt-6-astra","reviewed_sha":"f15e3d558f1f8117584d54ddb8363a696921b41f3355c4cd330bbdeb6208408a","on_current_version":false}],"source_from":"version from return #1181","manuscript_md":"# A lower bound G₂(x#) ≫ x ln x for the twin Jacobsthal function from published ingredients only\n\n*Draft 2, 2026-09-19, revising Draft 1 (return #32, 2026-09-11) after referee report 15 (reject with specific corrections; Proposition 1, Theorem 1 with its coefficient, and the verified N5 cover preserved). What changed: the §6 placement table no longer promotes the all-constants-one estimate 10^{134.1} into a sufficient threshold and no longer revives a withdrawn Selberg support-parameter condition (item A); the finite instance of §5 is identified as the old-cutoff greedy variant and the revised theorem's own choices are run beside it, with the referee's four-row table reproduced (item B); the Rosser–Schoenfeld locators are corrected and the claims they support narrowed (item C); the representative repair for [KK]'s Corollary 1 proof is fixed in sign and the direct sequence n(n+2) is given as the shorter interface, with Halberstam–Richert 1971 as an accessible published source (item D); the Mertens check's stable stdout is hashed separately from its timing lines (item E); the novelty language is scoped to the searches run and the unlocated Tao attribution is withdrawn (item F); the smaller corrections of the report's §3 are applied (§2 monotonicity, §1.3 survivor count, the falsification table, the integer endpoint via a separate constant, nonpositive c₀). Internal to the primeoire repository; the publication moratorium is in force and this document is not submission copy. Prose follows `paper/writing-style-math.md`. Grade and triggers are carried by `paper/proposals/prop-xlnx-lower-bound.md` (QUICK-DRAFT, regraded 2026-08-28); the suite architecture is `paper/PAPERS.md`. The mathematics is the record's, `research/history/staging/import-hypergraph.md` §4, first written out as a proof in `paper/kk-lower-bound.md` §9 (Theorem A there) and adversarially confirmed in `research/history/staging/redteam-0820-math.md` §3.3 to §3.4. This note is the paper case the proposal's first upgrade trigger asked for: the provenance trade, stated on its own.*\n\n**Author.** Chris Benjaminsen.\n\n**Methods and AI disclosure** (the statement adopted for the suite, `paper/PAPERS.md`, adapted to this note): the framework, vocabulary, and driving questions are the author's, developed over six years of independent work. Formal derivations, literature audits, computations, and manuscript drafting were carried out using AI assistants operating under the author's direction; computations have reproducible code and recorded outputs, asymptotic arguments require their stated mathematical inputs and are not proved by finite checks, and all refuted intermediate claims are retained in the record.\n\n---\n\n## Abstract\n\nLet G₂(x#) be the largest gap between consecutive twin slots modulo x#, the product of the primes at most x: a twin slot is an n with gcd(n(n+2), x#) = 1, and G₂(x#) − 1 is the length of the longest run of consecutive integers none of which is a twin slot. We prove that for every\n\n> c₀ < 1 / (8 C₁ C₂ e^{−2γ})\n\nthere is an x₀(c₀) with G₂(x#) ≥ c₀ x ln x + 1 for all x ≥ x₀, where C₂ is the twin prime constant and C₁ the implied constant of the dimension-two upper-bound sieve. In the record's shorthand, G₂(x#) ≥ (c + o(1)) x ln x with c effective. The proof consumes three published statements (the fundamental lemma of sieve theory in its residue-class form, as printed in Kalmynin and Konyagin's Corollary 1 and in Halberstam and Richert's Theorem 2.2; Mertens' third theorem; the prime number theorem) and one elementary identity of this corpus, and composes them in four steps written out in full. The composition is the author's and has not been refereed. The constant is effective and not computed. The bound sits above the lower bound G₂(x#) ≫ x ln x · lll x/ll x that transfers for free from Ford, Green, Konyagin, Maynard and Tao through G₂ ≥ g, by a factor ll x/lll x, and below the corpus's unrefereed reading of Kalmynin and Konyagin at x ln³x (lll x)²/(ll x)⁴ by about ln²x. The point of the note is the provenance trade: this chain never enters a published proof, where the stronger reading re-derives the inside of one. A finite construction of the same shape covers [1, 200000] with primes up to 10861 and replays clean in three seconds on one thread; it checks the construction at one scale and says nothing about the limit. Nothing here bears on the twin prime conjecture or on the upper side of G₂.\n\n---\n\n## 1. Introduction\n\n### 1.1 The object\n\nFix x ≥ 2 and write W = x# = ∏_{p ≤ x} p. An integer n is a **twin slot** for W when gcd(n(n+2), W) = 1: neither n nor n + 2 has a prime factor at most x. Twin slots exist for every x, since W − 1 is one. The **twin Jacobsthal function** is\n\n> G₂(x#) = max { b − a : a < b consecutive twin slots for W },\n\nthe largest gap between consecutive twin slots modulo W (`paper/kk-lower-bound.md` §1.2, where the same function is written G₂(P(y)) with y the sieving level; `paper/beta2-note.md` indexes it by n as G₂(n) at p_n#; we write G₂(x#) as `research/G2-STATE.md` does). The run of non-slots strictly between two consecutive slots has length G₂(x#) − 1. The first values are G₂(x#) = 2, 6, 12, 30, 42, 66, 108 for x = 2, 3, 5, 7, 11, 13, 17 (`paper/beta2-note.md`; the ladder is verified to x = 43 in `research/two-class-lower-bounds.md` §5).\n\nThe question the record works on is the upper side, and this note does not touch it. The wall first: the twin-relevant statement is G₂(x#) < p²_{next} infinitely often, the best proven upper bound in this corpus is G₂(x#) ≪_ε x^{β₂+ε} with β₂ = 4.26645… (`paper/beta2-note.md`; the twenty-digit value is Booker and Browning's, `research/SEARCH-CONVENTIONS.md` §4), the distance from β₂ to 2 is a dimension-two sifting-limit problem, and exponent 2 itself is parity (`research/covering-dive.md`, synthesis items 3 and 4). A lower bound on G₂ says that twin slots can be absent from long runs. It says nothing about twin primes.\n\n**Proposition 1 (covering form; `research/two-class-lower-bounds.md` §1, proven there, elementary).** G₂(x#) − 1 equals the largest m such that [1, m] can be covered by choosing, for each prime p ≤ x, one residue a_p mod p and deleting the pair {a_p, a_p − 2} mod p.\n\n*Proof, as in the record.* Let s < s′ be consecutive twin slots and m = s′ − s − 1, so s+1, …, s+m are non-slots. For t = s + j the prime p kills t when p | t or p | t + 2, that is when j ≡ −s or j ≡ −s − 2 (mod p): the deleted pair is {a_p, a_p − 2} with a_p = −s mod p, and [1, m] is covered. Conversely, given residues (a_p)_p covering [1, m], CRT gives an s with s ≡ −a_p (mod p) for all p ≤ x; then j ≡ a_p forces p | s + j and j ≡ a_p − 2 forces p | s + j + 2, so s+1, …, s+m are non-slots. The run is bounded on both sides by twin slots, since twin slots exist, so some gap is at least m + 1. ∎\n\nThe consequence used in §3: **a full cover of [1, y] by pairs {a_p, a_p − 2}, p ≤ x, gives G₂(x#) ≥ y + 1.** The proposal words this step as \"G₂(x#) ≥ y − O(1)\" (`prop-xlnx-lower-bound.md` §1); the identity gives + 1, and at every level we could exhaust (x ≤ 17) the constructed window is the global maximal run and the loss is exactly zero (§5, Appendix A).\n\nThe covering optimum G₂(x#) − 1 is the sequence OEIS A144311 (Carter 2008, Alekseyev 2009, Wang 2024; 22 terms to x = 79), whose wording, \"the length of the longest sequence of consecutive integers, each equal to 1 or −1 modulo at least one of the first n primes\", is the same object in the fixed-classes form. A144311 carries no formula line and no reference line (`paper/kk-lower-bound.md` §1.2).\n\n### 1.2 The one-class history and the free transfer\n\nJacobsthal's function g(x#) is the same object with one deleted class a_p per prime. Every twin slot is a reduced residue, so G₂(x#) ≥ g(x#) pointwise (`research/two-class-lower-bounds.md` §1, proven, elementary), and every lower bound for g transfers. The classical chain runs Westzynthius, Erdős, Rankin [Ra], Pintz [Pi], and Ford, Green, Konyagin, Maynard and Tao [FGKMT], whose bound in this normalisation reads\n\n> g(x#) ≫ x · ln x · lll x / ll x,   (1.1)\n\nwith ll = ln ln and lll = ln ln ln (`research/two-class-lower-bounds.md` §3; `paper/kk-lower-bound.md` §1.1, eq. (1.1)). This is the **free transfer**: G₂(x#) ≫ x ln x · lll x/ll x, graded proven in `research/G2-STATE.md` §3a, with nothing two-class in it.\n\nEvery construction in that chain has two stages. Small primes sieve an interval with a fixed residue; the survivors are then mopped up one at a time by the large primes. In the one-class problem the sieving stage is one-dimensional, the survivors of [1, y] number about y/ln y, and mopping them up with the x/ln x primes below x allows only y ≍ x: the trivial bound. Rankin and his successors gain their logarithm by choosing the sieving residues cleverly, so that the survivors are the smooth numbers of the interval and are few. The dimension of the sieve is the whole difference between that history and the argument below.\n\n### 1.3 What this note does\n\nRun the same two stages with the pair {0, −2} instead of the single class {0}. The sieving stage is now two-dimensional, the survivors of [1, y] number at most a constant times y/ln²y by the upper-bound half of the fundamental lemma (the upper bound is all that is used), and one prime per survivor fits with y ≍ x ln x. Nothing else is needed: no smooth-number seeding, no reading of any published proof. The result is Theorem 1 of §3,\n\n> G₂(x#) ≥ c₀ x ln x + 1 for x ≥ x₀(c₀), for every c₀ < 1/(8 C₁ C₂ e^{−2γ}),\n\na factor ll x/lll x above (1.1) and two logarithms, up to ll factors, below the corpus's stronger reading of Kalmynin and Konyagin (§6). The stronger reading is derived in the record and not refereed. Theorem 1 is the strongest two-class lower bound found in this corpus's searches (§7, §8.3) whose provenance is entirely published statements plus one page of elementary composition, and that is what the note is about; the mechanism is standard, and a bounded negative search is not a novelty proof. Section 4 grades every step, §5 replays the finite instance and says what it does and does not check, §6 places the bound, §7 states the prior-art position as the registry files it, and §8 lists what would break the theorem.\n\n### 1.4 Attribution\n\nThe mechanism is the standard one. The dimension-κ fundamental lemma, Mertens' theorem and the prime number theorem belong to their authors; the Erdős–Rankin shape belongs to that literature; the two-class covering identity is the corpus's restatement of a fact its own scripts record under the name PAIRED (`research/two-class-lower-bounds.md` §1). The two-stage accounting for the pair {0, −2} was first sketched in `research/two-class-lower-bounds.md` §4b at INFERRED grade, with two survivors per mop-up prime; the chain was written out as a proof, with one survivor per prime, in `research/history/staging/import-hypergraph.md` §4 on 2026-08-20 and carried into `paper/kk-lower-bound.md` §9 as Theorem A. Kalmynin and Konyagin's Remark 1 records the same shape, j_f(P(y)) ≫ y ln y, for their value-shifted polynomial analogue at every f of degree at least two (§7). What this note claims is the composition for G₂ at this provenance grade, the corrected constant, and the replayed finite instance, and nothing more.\n\n---\n\n## 2. Ingredients\n\nEvery ingredient is a published statement consumed as a statement, or an elementary identity written out here. No published proof is entered.\n\n**Ingredient A (the fundamental lemma, residue-class form).** Let κ > 0 and z ≥ 2. For each prime p ≤ z let Ω_p ⊂ Z/pZ have g(p) elements, where g extends multiplicatively, g(p) ≤ κ and g(p) < p for every prime p. Let S(X, Ω) be the number of n ≤ X with n mod p ∉ Ω_p for all p ≤ z, and V(z) = ∏_{p ≤ z}(1 − g(p)/p). Then for z ≪ X,\n\n> S(X, Ω) ≤ C₁(κ) · X · V(z),\n\nwith C₁(κ) depending on κ only.\n\nThis is Kalmynin and Konyagin's Corollary 1 [KK, p. 4], quoted verbatim in `research/covering-dive.md` §4.2 and re-read for this note at the arXiv v2 PDF (md5 in §10). It is the residue-class instance of Halberstam and Richert's Theorem 2.2 [HR], the upper-bound half of the fundamental lemma of sieve theory: with A = {n ≤ X} and A_d the elements of A lying in a deleted class modulo each prime dividing d, CRT gives |A_d| = g(d) X/d + r_d with |r_d| ≤ g(d), which is the hypothesis list of [KK] Lemma 1 and of [HR] Theorem 2.2. For the instantiation of §3 the shortest interface is the divisibility sequence A = {n(n+2) : 1 ≤ n ≤ ⌊y⌋} sifted by the primes up to z, with one deleted class at 2 and two at every odd prime; an accessible independent published source for the resulting upper bound is Halberstam and Richert's 1971 memoir [HR71], where the example n(n+2) is treated on printed p. 99 and Theorem 3 on p. 100 gives the applicable bound in a fixed polynomial range (referee report 15 §1, read there at the page). We write C₁ = C₁(2). It is effective, because the constant in [HR] Theorem 2.2 is, and we do not compute it.\n\nTwo provenance facts travel with this ingredient and are stated here rather than implied away. First, [KK]'s printed proof of Corollary 1 does not work as written: it builds an auxiliary integer m from factors P(z; p′) n + r′ Q(z; p′) with r′ running over representatives of Ω_{p′}, and for p ≠ p′ that factor is congruent to −r′ modulo p, so whenever 0 ∈ Ω_{p′} every other prime up to z divides m and the asserted (m, P(z)) = 1 fails (at z = 5 with Ω₂ = {0}, Ω₃ = {0, 1}, Ω₅ = {0, 3}, gcd(m, 30) = 30 for n = 1, …, 5). The statement is unaffected. The one-line repair has to be made with the right sign: at the selected prime p′ the factor is proportional to n + r′ and deletes the class −r′, so the representatives must run over −Ω_{p′} (with r′ ≡ 1 modulo the other primes to kill the cross-prime zero factors); Draft 1 indexed representatives of Ω_{p′} and had the sign wrong (referee report 15 §2 D). Shorter still, the direct sequence n(n+2) above avoids the auxiliary product altogether, and [HR] Theorem 2.2 or [HR71] Theorem 3 applies to it as printed. `paper/kk-lower-bound.md` §11.2 records the slip and the repair; `research/covering-dive.md` §4.2 and `redteam-0820-math.md` §3.3 still carry the unqualified \"consumed as a theorem\" for it. Second, nobody in this project has read [HR] Theorem 2.2 at a page image; its statement was reached at OCR (`paper/kk-lower-bound.md` §12). The ingredient is therefore a published statement, printed twice, whose corpus provenance is one PDF read at source and one OCR read.\n\n**Ingredient B (Mertens).** ∏_{p ≤ z}(1 − 1/p) = e^{−γ}(1 + o(1))/ln z, Mertens' third theorem [Me], with explicit two-sided bounds in Rosser and Schoenfeld [RS, Theorem 7, (3.25)–(3.26)]; Draft 1 cited Theorem 5, (3.17)–(3.18), which on printed p. 70 are the reciprocal-prime sums and not the products (referee report 15 §2 C, checked at the page).\n\n**Ingredient C (the prime number theorem).** π(x) = (1 + o(1)) x/ln x. For the capacity count of Step 3 only a fixed-factor bound is needed and [RS, Corollary 1, (3.5)–(3.6)] with π(z) ≤ z suffices; the two-sided relative error tending to zero is [RS, Theorem 1, (3.1)–(3.2)] or Theorem 2, (3.3)–(3.4).\n\n**Ingredient D (the covering identity).** Proposition 1 of §1.1, elementary, from the record.\n\nOne constant is needed. Let C₂ = ∏_{p > 2}(1 − 1/(p − 1)²) = 0.6601618… be the twin prime constant. For odd p,\n\n> (1 − 2/p) / (1 − 1/p)² = (p² − 2p)/(p − 1)² = 1 − 1/(p − 1)²,\n\nso ∏_{2 < p ≤ z}(1 − 2/p) = ∏_{2 < p ≤ z}(1 − 1/p)² · ∏_{2 < p ≤ z}(1 − 1/(p − 1)²); the second product decreases to C₂ (each factor is below 1) and the first is 4 ∏_{p ≤ z}(1 − 1/p)². By Ingredient B,\n\n> ∏_{2 < p ≤ z}(1 − 2/p) = 4 C₂ e^{−2γ}(1 + o(1)) / ln²z,   (2.1)\n\nand with g(2) = 1, g(p) = 2 for odd p,\n\n> V(z) = (1/2) ∏_{2 < p ≤ z}(1 − 2/p) = 2 C₂ e^{−2γ}(1 + o(1)) / ln²z = (0.41621… + o(1)) / ln²z.   (2.2)\n\nThe constant is checked numerically in `mertens-check.py`: V(z) ln²z = 0.4162027 at z = 2·10⁷ against 0.4162145 predicted (Appendix A). The record's shorthand \"(C₂ + o(1))/ln²z\" for the product (2.1) (`import-hypergraph.md` §4 step 2; `redteam-0820-math.md` §3.3 item 2; `paper/kk-lower-bound.md` §9 step 2, where C₂ then becomes an undefined C₃) omits the factor 4 e^{−2γ} = 1.26095…. The slip touches the unnamed constant only, not the shape and not effectivity, and (2.2) is the form used below.\n\n---\n\n## 3. The theorem\n\n**Theorem 1.** Let C₁ = C₁(2) be the constant of Ingredient A at κ = 2 and C₂ the twin prime constant. For every c₀ with\n\n> c₀ < 1 / (8 C₁ C₂ e^{−2γ})\n\nthere is an x₀ = x₀(c₀) such that for all x ≥ x₀,\n\n> G₂(x#) ≥ c₀ · x ln x + 1.\n\nIn particular G₂(x#) ≥ (c + o(1)) x ln x with c = 1/(8 C₁ C₂ e^{−2γ}), and c is effective.\n\n*Proof.* For c₀ ≤ 0 the statement is trivial (G₂ ≥ 1), so let 0 < c₀ < 1/(8 C₁ C₂ e^{−2γ}) and fix c₁ strictly between c₀ and that threshold. Put y = c₁ x ln x. We construct residues a_p for every prime p ≤ x such that the pairs {a_p, a_p − 2} mod p cover [1, ⌊y⌋]; Proposition 1 then gives G₂(x#) ≥ ⌊y⌋ + 1 ≥ c₁ x ln x, and enlarging x until (c₁ − c₀) x ln x ≥ 1 gives G₂(x#) ≥ c₀ x ln x + 1, the statement. Set\n\n> z = y^{1/2} / ln y.\n\n(The record takes z = √y. Ingredient A asks only z ≪ X, so √y is admissible at the letter; the extra 1/ln y keeps the fundamental lemma comfortably inside its range at no cost, since ln z = (1/2) ln y (1 + o(1)) and the constant of (2.2) is unchanged.)\n\n*Step 1: the survivors of the small primes, counted by Ingredient A.* Take Ω₂ = {0} and Ω_p = {0, −2 mod p} for odd p ≤ z, so g(2) = 1 and g(p) = 2 for odd p. The hypotheses of Ingredient A hold at κ = 2: g is multiplicative by construction, g(p) ≤ 2, g(p) < p at every prime (1 < 2 at p = 2, and 2 < p for odd p, where the classes 0 and −2 are distinct), and z ≤ y = X. Let V be the set of n ∈ [1, y] with n mod p ∉ Ω_p for all p ≤ z: the odd n ≤ y such that no odd prime at most z divides n or n + 2. Ingredient A gives\n\n> #V ≤ C₁ · y · V(z).\n\n*Step 2: the product, by Mertens.* By (2.2) and ln z = (1/2) ln y (1 + o(1)),\n\n> #V ≤ 8 C₁ C₂ e^{−2γ} (1 + o(1)) · y / ln²y.\n\n*Step 3: one prime per survivor, by the prime number theorem.* Since y = c₁ x ln x, ln y = (1 + o(1)) ln x, so y/ln²y = (1 + o(1)) c₁ x/ln x and\n\n> #V ≤ 8 C₁ C₂ e^{−2γ} c₁ (1 + o(1)) · x / ln x.\n\nThe primes in (z, x] number π(x) − π(z) = (1 + o(1)) x/ln x by Ingredient C, because z = o(x/ln x). The choice of c₁ says 8 C₁ C₂ e^{−2γ} c₁ < 1, so for all x beyond some x₀ the primes of (z, x] outnumber the survivors, and we fix an injection r ↦ p_r from V into the primes of (z, x]. Set a_{p_r} = r mod p_r for r ∈ V, and a_p = 0 for every other prime p ≤ x: every p ≤ z, and every prime of (z, x] not in the image.\n\n*Step 4: every r ∈ [1, y] is covered.* If r ∉ V, some prime p ≤ z has p | r or p | r + 2 (or r is even, in which case p = 2 and both classes coincide), so r ≡ 0 = a_p or r ≡ −2 = a_p − 2 (mod p). If r ∈ V then r ≡ a_{p_r} (mod p_r). So the pairs {a_p, a_p − 2}, p ≤ x, cover [1, ⌊y⌋], and Proposition 1 gives G₂(x#) ≥ ⌊y⌋ + 1. ∎\n\n**Effectivity.** Each o(1) above is an explicit function of x once the error terms of Ingredients B and C are taken from [RS] and the constant C₁ from [HR] Theorem 2.2. x₀(c₀) is therefore computable in principle. We have not computed it, and this note claims no numerical value for c or for x₀. The one measurement we have is that at y = 200000 the survivor count of Step 1 with z = √y ≈ 447 is 2137 against a main term 200000 · V(447) = 2203.6, a ratio 0.9698, and with the theorem's z = √y/ln y ≈ 36.6 it is 6210 (Appendix A, §5); each is one instance and not a value of C₁.\n\n**Where the logarithm comes from.** Run the same four steps with one class, Ω_p = {0}: Ingredient A at κ = 1 gives #V ≪ y/ln y, and y/ln y ≤ x/ln x forces y ≪ x. The one-class version of this argument proves only g(x#) ≫ x, the trivial bound. The pair {0, −2} makes the sieve two-dimensional, the survivor count drops from y/ln y to y/ln²y, and y = c₀ x ln x fits. That factor ln x is the whole content of Theorem 1 relative to the trivial bound. Only an upper-bound sieve is used, so the dimension-two sifting limit β₂ that governs the upper side of G₂ never enters; that observation is §4b's (`research/two-class-lower-bounds.md`) and it is the one-line answer to a referee who asks why dimension two is not an obstruction here.\n\n**Two classes per mop-up prime.** §4b's sketch spends each mop-up prime on two survivors, using both a_p and a_p − 2, and states the capacity as 2x/ln x. That doubles the admissible c₀ if two survivors at distance exactly 2 can always be paired, which needs an argument the sketch does not give. Theorem 1 uses one survivor per prime and forgoes the factor 2.\n\n---\n\n## 4. Calibration\n\nThe corpus grades on the ladder proven > verified > certified > measured > inferred > conjectured > refuted (`paper/proposals/PROPOSALS.md`, legend), where PROVEN is \"a proof is in hand, or it is a published theorem cited to its source\" and INFERRED is \"our deduction from sourced facts, complete but not refereed\". Applied to §3:\n\n| step | what is consumed | rung |\n|---|---|---|\n| Proposition 1 | elementary CRT, proof written out in `two-class-lower-bounds.md` §1 and in §1.1 | proven |\n| Ingredient A | [KK] Corollary 1 = [HR] Theorem 2.2 in residue-class form, at its statement; hypotheses discharged in Step 1 | published theorem, cited to source; the [KK] proof slip and the OCR-only [HR] read are stated in §2 |\n| (2.1), (2.2) | Mertens plus a two-line identity, written out in §2; constant checked numerically | proven |\n| Step 3 | the prime number theorem at its statement | published theorem, cited to source |\n| the composition | Steps 1 to 4 | inferred: written out here and in `kk-lower-bound.md` §9, re-derived independently by the adversarial pass of 2026-08-20 and again for this note, not refereed |\n\nTheorem 1 is proven in the ordinary sense conditional on nothing. The rider the record attaches, and we keep, is that the composition is the corpus's own and has been checked by the corpus's own adversary and by this note's independent re-derivation, not by an outside referee. The one import the chain cannot survive losing is Ingredient A's hypothesis list at κ = 2; Step 1 discharges it clause by clause, the proposal prices this trigger low (`prop-xlnx-lower-bound.md` §5), and we found nothing on our own re-read of [KK] pp. 3 to 4.\n\n---\n\n## 5. The finite instance\n\nThe record carries a finite cover of the shape y ≍ x′ ln x′, pre-registered as N5 (`research/history/staging/import-hypergraph-prereg.md`), produced by `research/import-hypergraph-01-instance.js`, and rebuilt from the prereg text alone by the adversarial pass with its own sieve and mop-up (`redteam-0820-math.md` §3.4). For this note it was run again, its embedded OUTPUT block checked against the served file with the record's own gate, the assembled cover exported, and the cover verified by a script sharing no code with the producer. Recipe, hashes and timings are in `n5-recipe.md` (Appendix A lists the sha256 of every file named here).\n\n**What the instance is.** y = 200000. Three stages, not the theorem's two:\n\n1. a_p = 0 fixed for p ∈ {2, 3, 5, 7, 11, 13}: cutoff z = 13, leaving |V| = 9889 survivors (density 9/182 predicts 9890.1);\n2. a_q random for the 162 primes 17 ≤ q ≤ 997 (splitmix64, seed 13, 200 trials, best trial kept), leaving 1654 survivors against an exact first moment 1731.07 and a mean over trials of 1730.83;\n3. greedy mop-up, one fresh ascending prime per remaining survivor with a_q = r mod q: 1153 primes, 1.43 survivors per prime, largest prime x′ = 10861.\n\n**What was checked.** The producer's stdout is byte-identical to the block embedded in the served file (2.29 s, one thread, 240 MB). The independent verifier confirms from scratch: 1321 moduli, all prime, pairwise distinct; stage 1 exactly as stated at a_p = 0; the middle stage exactly the 162 primes in [17, 997]; the mop-up exactly the first 1153 primes above 997 with maximum 10861; every mop-up class anchored on a genuine survivor; and, from the residues alone, **zero uncovered n in [1, 200000]**. Two deliberate corruptions are caught (dropping the class at 10861 leaves 1 uncovered, shifting a₁₇ by one leaves 119), so the check is not vacuous. Ratio y/(x′ ln x′) = 200000/100930.55 = 1.98156, the record's 1.9816.\n\n**The theorem's construction at the same scale, and what Draft 1 actually ran.** Draft 1 reported \"the theorem run literally\" as |V| = 2137, 1220 mop-up primes, x′ = 10711, ratio 2.0123 (`n5-theorem-literal.txt`). Those numbers belong to the old cutoff z = √y ≈ 447 with a greedy mop-up that skips survivors already covered incidentally, not to the theorem as stated (z = √y/ln y, one distinct prime injected per original survivor); referee report 15 §2 B identified the mismatch and supplied a standard-library checker, reproduced here (`check-constructions.py`, `check-constructions.out`):\n\n| initial cutoff | original survivors | mop-up rule | new primes | largest prime x′ | y/(x′ ln x′) |\n|---|---|---|---|---|---|\n| √y ≈ 447.21 | 2137 | skip covered survivors (greedy) | 1220 | 10711 | 2.0123 |\n| √y | 2137 | inject every original survivor | 2137 | 19597 | 1.0326 |\n| √y/ln y ≈ 36.64 | 6210 | skip covered survivors (greedy) | 1331 | 11071 | 1.9400 |\n| √y/ln y | 6210 | inject every original survivor | 6210 | 61871 | 0.2930 |\n\nAll four cover [1, 200000] with distinct primes and zero uncovered positions. The theorem's literal choices (last row) give ratio 0.29 at this scale; the greedy improvement, which is valid (a survivor already covered needs no prime), is what the 2.0 figures measure, and it is identified as such. Pure ascending greedy above z = 13 with no random stage gives x′ = 10301, ratio 2.1013. The random middle stage of the registered pipeline costs about one percent of the ratio rather than buying it, and the prereg's own prediction for the pipeline (x′ ≈ 16400, ratio ≈ 1.2) was pessimistic. None of these finite ratios contradicts the asymptotic theorem or determines its unnamed constant.\n\n**The CRT step at small scale.** For x ∈ {5, 7, 11, 13, 17} the verifier exhausts every choice of residues, takes the largest fully covered [1, y], solves s ≡ −a_p (mod p), and measures the true maximal twin-slot-free run modulo x# by direct sieve. At every level the constructed window is the global maximal run, the loss is zero, and run + 1 reproduces the ladder 12, 30, 42, 66, 108 (`n5-verify-out.txt`). The record's \"G₂(x#) ≥ y − O(1)\" is conservative by exactly + 1 at these levels.\n\n**What the instance does not check.** Anything about the limit. The ratio 1.98 at one scale is a measurement of one greedy instance; the theorem's admissible c₀ is a small unnamed constant, and the finite ratio is not a lower bound on it and not evidence for it. The record says so (`redteam-0820-math.md` §3.4; `prop-xlnx-lower-bound.md` §6) and we repeat it.\n\n**Recipe** (a reviewer with only the served files; write `<project base>` for the host; one thread, under ten seconds in all).\n\n```\ncurl -sS -H \"Authorization: Bearer $TOKEN\" <project base>/docs/research/import-hypergraph-01-instance.js -o research/import-hypergraph-01-instance.js\ncurl -sS -H \"Authorization: Bearer $TOKEN\" <project base>/docs/research/qc/embed.js   -o research/qc/embed.js\ncurl -sS -H \"Authorization: Bearer $TOKEN\" <project base>/docs/research/qc/tailfmt.js -o research/qc/tailfmt.js\nnode research/import-hypergraph-01-instance.js > stdout-original.txt        # sha256 cdcdf4ac…, 2.3 s\nnode research/qc/embed.js --check research/import-hypergraph-01-instance.js  # code-sha256 and out-sha256 match\n# insert the one inert dump line after line 256 as in n5-recipe.md §3, then:\nCOVER_OUT=$PWD/cover.json node instance-with-dump.js > stdout-dump.txt      # diff against stdout-original.txt is empty\npython3 verify-cover.py cover.json > verify-out.txt                          # uncovered = 0; sha256 cf7bc45c…\npython3 mertens-check.py 20000000 > mertens-check-out.txt                    # V(z) ln²z at 2·10⁷ = 0.4162027; stable stdout sha256 1a02897f…; the Draft 1 file 985f9f3b… carried three timing lines that this command does not emit\npython3 check-constructions.py > check-constructions.out                     # the four-row table of §5 (referee report 15's checker), standard library, seconds\n```\n\n---\n\n## 6. Placement\n\nThree lower bounds for G₂(x#) stand in this corpus. With ll = ln ln, lll = ln ln ln:\n\n| bound | source | grade |\n|---|---|---|\n| G₂(x#) ≫ x ln x · lll x/ll x | G₂ ≥ g pointwise and [FGKMT] | proven, free transfer, nothing two-class |\n| G₂(x#) ≥ c₀ x ln x + 1 for x ≥ x₀(c₀), every c₀ < 1/(8 C₁ C₂ e^{−2γ}) | Theorem 1 | published ingredients at their statements; composition inferred, unrefereed |\n| G₂(x#) ≫ x ln³x (lll x)²/(ll x)⁴ for x beyond an unspecified eventual threshold (the record's 10^{134.1} is the estimate obtained by setting every implied constant to 1, a floor on the actual onset and not a certified sufficient range) | `two-class-lower-bounds.md` §4c; `paper/kk-lower-bound.md` Theorem B | derived in the record, not refereed; the remaining obligations are the unrefereed substitution into [KK]'s §2, the page-image read of [HR] Theorem 2.2, and a certified threshold |\n\nThe middle line is above the first by ll x/lll x → ∞ and below the third by ln²x (lll x)²/(ll x)⁴ ≈ ln²x. Both comparisons are asymptotic with the constants unnamed: at x = 10¹⁰⁰, ll x/lll x = 3.21, so the improvement over the free transfer is a factor of three against two unevaluated constants, and a referee is entitled to call \"above FGKMT\" unverified until both constants are computed. We state it as the asymptotic comparison it is.\n\nA referee will ask why the weaker of the two two-class bounds deserves a note. The answer is provenance. The §4c reading substitutes the pair {a_p, a_p − 2} into the interior of [KK]'s §2 construction and re-derives their case trichotomy for it; what remains for it is the unrefereed substitution, the unread [HR] Theorem 2.2 page, and a certified threshold (Draft 1 cited a Selberg support-parameter condition at κ = 4 as a live obstacle; the record marked that discussion superseded on 2026-09-07 and the companion paper's §6.2 makes it a remark, since the consumed Brun-form statement has no such parameter). The chain of §3 consumes the fundamental lemma at its statement and never enters a proof. A reader who grants three published statements and one page of composition has Theorem 1; a reader of §4c has to referee a substitution. Theorem 1 also runs at accessible scale and replays clean (§5), whereas the §4c bound has no certified practical threshold at which to run it.\n\nThe trade has a cost and it is stated: two logarithms, up to the ll factors. We do not argue that the weaker bound is preferable. We argue that it is the strongest two-class lower bound of that provenance grade found in this corpus's searches, and that the searches run (§7, §8.3) found no bound of that grade for this object; the searches are bounded and their omissions are listed.\n\n---\n\n## 7. Prior art\n\nThe registry's position is the one stated here; we have not softened it and we have not improved on it.\n\n- **No published two-class lower bound of any shape was found** in the owning convention (`paper/proposals/PROPOSALS.md`; `research/SEARCH-CONVENTIONS.md` §1 and §3). The owning convention for this object is A144311's own wording and the \"bounded number of residue classes per prime\" phrasing of MathOverflow 88323, not the corpus's vocabulary; the rule that a clean negative proves nothing until the owning convention has been searched is `SEARCH-CONVENTIONS.md`'s and it was applied. A144311 carries no formula and no reference lines. Of the 1217 problems on erdosproblems.com exactly two mention Jacobsthal (#687, #970) and neither poses the two-class variant; Ford, Konyagin, Maynard, Pollack and Tao's Remark 7 states the twin sifting system as ground their one-dimensional method does not reach (`research/covering-dive.md` §4.2 and Q5).\n- **The shape is in print for the nearest cousin.** [KK] Remark 1 (p. 3) records j_f(P(y)) ≫ y ln y for every polynomial f of degree at least two, as a consequence of their Theorem 1. Their j_f shifts the value, G₂ shifts the argument, and the two are not the same family of sets even at f(i) = i(i + 2) (`research/covering-dive.md` §4.2, Correction 2), so their theorem does not apply to G₂ as stated. But the shape y ln y for a two-element sifting system is theirs in print, by a far heavier route, and a referee will say that the argument of §3 is the standard fundamental-lemma-plus-mop-up mechanism and very likely folklore. We agree that the mechanism is standard; that is the point of consuming it at its statements. The claim is the object and the grade, not the shape.\n- **A claimed public flag is withdrawn.** Draft 1 attributed to Tao's 2014 post on large prime gaps a \"shifted sifting\" discussion of the case A = {n(n+2)}; the referee could not locate that passage in the retrieved page or its indexed text, and the post opens with the four-author 2014 paper rather than the five-author [FGKMT] (referee report 15 §2 F). We could not locate it either and withdraw the citation; if the intended passage exists elsewhere it needs an exact permalink before it can be cited. The sifting picture of §1.1's wall stands on the corpus's own records without it.\n- **[KK] has no citations recorded in the databases the corpus swept** (`prop-kk-lower-bound.md` §4, inherited by `prop-xlnx-lower-bound.md` §4). That finding expires the day someone cites them for a two-class bound, and this note would then compare against that paper.\n- **Holt's cycle-of-gaps corpus** (`research/PRIOR-ART.md`) owns most of the corpus's frame and gives a constructive one-class lower-bound technique; it never studies the spacing between consecutive occurrences of the gap 2, which is G₂, and proves no bound on any maximum gap.\n- **The standing assumption of the registry**, that prior art exists for more of the corpus than has been found, applies here with less force than anywhere else in it, because the claim is mostly made of other people's theorems and says so first (`prop-xlnx-lower-bound.md` §4). It still applies, and Remark 1 of [KK] is the nearest thing to it that we know.\n\n---\n\n## 8. Residuals, and what would break the theorem\n\n### 8.1 Load-bearing readings of the source\n\n[KK] Corollary 1 and Lemma 1 were re-read for this note at the arXiv v2 PDF (12 pages, md5 b5d7d2a23ffd902415057adebfe430b1, matching the record's artifact). The statement quoted in `covering-dive.md` §4.2 is exact word for word. Lemma 1's hypothesis list as rendered in `redteam-0820-math.md` §3.3 (g multiplicative, g(p) ≤ κ, g(p) < p for all primes, z ≪ X, constant depending on κ) omits one clause, |r_d| ≤ g(d), which is invisible at the Corollary 1 interface and is what makes z near X^{1/2} admissible; Step 1 satisfies it by CRT. Remark 1 on p. 3 was read for §7.\n\n### 8.2 The unread dependency\n\n[HR] Theorem 2.2 has been reached in this project at OCR only (`paper/kk-lower-bound.md` §12). [KK] Lemma 1 cites it and proves nothing else; [KK]'s own Corollary 1 proof has the representative slip of §2. So the statement Theorem 1 consumes is printed in two places, one of which this project has read at source and one of which it has not, and the printed derivation connecting them is repaired here in one line rather than read. A referee who wants the ingredient on firmer footing reads [HR] pp. 68 to 69 or any textbook form of the Selberg upper bound sieve of dimension two; the theorem does not change.\n\n### 8.3 Prior art residuals\n\nWhat was not searched travels with the negative. The corpus's sweeps ran in A144311's wording, in the MathOverflow 88323 phrasing, over erdosproblems.com, and over OpenAlex and Semantic Scholar citation graphs for [KK]. A further twenty-minute web search for this note (terms \"twin Jacobsthal\", \"Jacobsthal function\" with \"two residue classes\", \"shifted\", \"twin\", \"pair\", \"n(n+2)\"; Hagedorn's Jacobsthal papers; OEIS A144311; Tao's 2014 exposition of [FGKMT]) found no published lower bound for the two-class object (`lit-check-2026-09-11.md`). Neither sweep ran over the Russian-language literature around [KK], nor over lecture notes and problem collections where a folklore bound of this shape would live if it lives anywhere. [KK] Remark 1 is the closest published statement we know and it is about a different object.\n\n### 8.4 Falsification table\n\n| claim | what would falsify it | has the check run |\n|---|---|---|\n| Ingredient A applies at κ = 2 to Ω₂ = {0}, Ω_p = {0, −2} | a hypothesis of [KK] Lemma 1 or [HR] Theorem 2.2 that the instantiation violates | yes, at [KK] pp. 3 to 4, three times in the record and once here; [HR] at OCR only |\n| (2.2), the constant 2 C₂ e^{−2γ} | an error in the two-line identity or in Mertens' theorem; a finite product differing from its limit cannot refute convergence, and the numerical check is a consistency check only | identity checked; `mertens-check.py` to z = 2·10⁷ gives 0.4162027 as a consistency check |\n| Step 3, the injection exists for large x | a c₀ below the threshold with survivors outnumbering primes for arbitrarily large x | no explicit x₀; the inequality is asymptotic and its constants are unnamed |\n| Proposition 1 and the + 1 | a full cover of [1, y] with G₂(x#) ≤ y | brute force at x ≤ 17: loss 0 at every level |\n| the finite cover at x′ = 10861 | an n ∈ [1, 200000] hit by no class | yes, independent verifier, 0 uncovered; negative controls catch corruptions |\n| \"above the free transfer\" | the asymptotic comparison is a statement about limits; a finite observed ratio cannot refute it, and only computed constants could locate a crossover range | no; both constants unevaluated |\n| the implied constant C₁ is effective | a non-effective step in [HR] Theorem 2.2 at κ = 2 | no explicit pass; not expected |\n\n### 8.5 What would move the grade\n\n**Toward submission.** One outside number theorist confirming that Ingredient A applies at κ = 2 to the pair (the proposal's second upgrade trigger); a numerical C₁ from [HR] Theorem 2.2 and an explicit x₀, which would also settle the \"above FGKMT\" row of §8.4; a page-image read of [HR] Theorem 2.2. **Against.** A published two-class lower bound of this or greater strength in the owning convention, which retires the note; a refereed publication of the §4c reading at its stronger exponent, which the proposal names as its retire trigger since a refereed x ln³x bound makes an x ln x note pointless; a hypothesis of the fundamental lemma the instantiation violates, which the proposal registers as its WEAKENED trigger.\n\n---\n\n## 9. Record\n\n- 2026-08-19: `research/two-class-lower-bounds.md` §4b sketches the two-stage accounting at INFERRED grade, two survivors per mop-up prime, superseded in strength the same day by §4c.\n- 2026-08-20: the chain is written out as a proof and flagged HELD in `import-hypergraph.md` §4, entering no live document; the pre-registration is committed alone at 469aaa3 before any producer or report (`import-hypergraph-prereg.md`).\n- 2026-08-20: the adversarial pass confirms every ingredient at its source and re-derives the composition (`redteam-0820-math.md` §3.3), and rebuilds the finite instance from the prereg text (§3.4). The same pass records that the prereg's N3 prediction failed at toy scale (99.9th-percentile short-pair codegree 0.1496 against the registered 0.02) and that the chain never uses N3. That failure is part of the record and is not repaired here.\n- 2026-08-28: `paper/kk-lower-bound.md` states the bound as Theorem A beside the §4c reading as Theorem B; the proposal is regraded QUICK-DRAFT. Its §11.2 records the [KK] Corollary 1 proof slip and the representative repair.\n- 2026-09-19: Draft 2, the corrections of referee report 15 (items A to F and the smaller ones), listed in the status line; the finite-construction table of §5 reproduced from the referee's checker.\n- 2026-09-11: Draft 1. Changes against the record: the Mertens constant is written as 4 C₂ e^{−2γ} in (2.1) and 2 C₂ e^{−2γ} in (2.2) in place of the record's C₂ and undefined C₃, and checked numerically; the theorem is stated with the explicit threshold c₀ < 1/(8 C₁ C₂ e^{−2γ}) and the form \"for x ≥ x₀(c₀)\"; z is taken as y^{1/2}/ln y; the consequence of a full cover is stated as G₂ ≥ y + 1 following Proposition 1, replacing the proposal's y − O(1); Ingredient A is cited to [HR] Theorem 2.2 with [KK] Corollary 1 as the printed instance, and the [KK] proof slip is stated in the ingredient rather than in a residual; the finite instance is replayed, exported, independently verified and hashed, and identified as a three-stage construction distinct from the theorem's two-stage one, with the theorem's construction run literally at the same scale beside it; [KK] Remark 1 is added to the prior-art position.\n\n---\n\n## 10. References\n\nHouse form: authors, title, identifiers, then an italic provenance sentence naming what was actually read for this note or in the record. Entries marked [RECORD] are carried from `paper/kk-lower-bound.md` §12 and were not re-read for this note; [MEMORY] entries carry bibliographic details this project holds without a page image.\n\n**The sieve input.**\n\n- [KK] A. Kalmynin and S. Konyagin, *A polynomial analogue of Jacobsthal function*, arXiv:2302.00459 (v1 1 Feb 2023, v2 3 Dec 2023); Izvestiya: Mathematics **88**:2 (2024) 225–235, DOI 10.4213/im9467e, MR4727548. *Publisher record verified in the record 2026-08-18. Re-read for this note 2026-09-11 at the arXiv v2 PDF, 12 pages, md5 b5d7d2a23ffd902415057adebfe430b1: Remark 1 (p. 3), Lemma 1 and Corollary 1 with its proof (p. 4), and the application of Corollary 1 in §2 (p. 6).*\n- [HR71] H. Halberstam and H.-E. Richert, *A new look at Brun's sieve*, Mémoires de la S.M.F. 25 (1971), numdam 10.24033/msmf.39: the example n(n+2) on printed p. 99 and Theorem 3 on p. 100 (read at the page by referee report 15; cited here on that reading).\n- [HR] H. Halberstam and H.-E. Richert, *Sieve Methods*, London Mathematical Society Monographs 4, Academic Press, London and New York, 1974 (Dover reprint 2011), Theorem 2.2, Chapter 2 §5, pp. 68 to 69. *[RECORD, OCR ONLY] Statement reached at the Dover search-inside index on 2026-09-07 and 2026-09-08 (`paper/kk-lower-bound.md` §12); no page image has been read in this project.*\n\n**The one-class lower bounds.**\n\n- [FGKMT] K. Ford, B. Green, S. Konyagin, J. Maynard and T. Tao, *Long gaps between primes*, arXiv:1412.5029; J. Amer. Math. Soc. **31** (2018), no. 1, 65–105. *[RECORD] PDF read in the record for `paper/kk-lower-bound.md`; bibliographic data re-confirmed at the arXiv record on 2026-09-11; not re-read for this note. The Jacobsthal-function form of the bound is quoted in [KK]'s introduction, p. 2.*\n- [Ra] R. A. Rankin, *The difference between consecutive prime numbers*, J. London Math. Soc. **13** (1938) 242–247, DOI 10.1112/jlms/s1-13.4.242. *Bibliographic data confirmed at the journal record (Oxford Academic and Wiley) on 2026-09-11; the paper itself was not read. Listed as reference [3] of [KK].*\n- [Pi] J. Pintz, *Very large gaps between consecutive primes*, J. Number Theory **63** (1997), no. 2, 286–301. *Bibliographic data confirmed at the ScienceDirect record on 2026-09-11; the paper itself was not read. Not among the nine references of [KK].*\n\n**Analytic inputs.**\n\n- [Me] F. Mertens, *Ein Beitrag zur analytischen Zahlentheorie*, J. reine angew. Math. **78** (1874) 46–62. *[MEMORY] The theorem is consumed at its standard statement; the explicit form used for effectivity is [RS].*\n- [RS] J. B. Rosser and L. Schoenfeld, *Approximate formulas for some functions of prime numbers*, Illinois J. Math. **6** (1962) 64–94. *[RECORD] Read at page images pp. 69–70 in the record on 2026-09-08 (Project Euclid, md5 357d126e8d5e498a74e750f2c3ff83cd): Corollary 1, (3.5) and (3.6) for π(x) (fixed-factor bounds); Theorem 1, (3.1)–(3.2), and Theorem 2, (3.3)–(3.4), for the relative error; Theorem 7, (3.25)–(3.26), for the Mertens product. Draft 1's \"Theorem 5, (3.17)–(3.18)\" named the reciprocal-prime sums of p. 70 and is corrected (referee report 15 §2 C, page checked there).*\n\n**The object.**\n\n- OEIS A144311, *The length of the longest sequence of consecutive integers, each equal to 1 or −1 modulo at least one of the first n primes* (Carter 2008, a(1) to a(7); Alekseyev 2009, a(8) to a(16); Wang 2024, a(17) to a(22)). *Entry fetched directly on 2026-09-11: 22 terms 1, 5, 11, 29, 41, 65, 107, 149, 203, 257, 347, 527, 545, 617, 707, 869, 965, 1079, 1283, 1397, 1529, 1709; no formula line and no reference line; links to a StackExchange note and a C++ program; cross-references A048670, A049300, A058989. Equal to G₂(p_n#) − 1.*\n- OEIS A048670, Jacobsthal's function at the primorials. *[RECORD]*\n\n**Platform records.** Referee report 15 on return #32 (its standalone checker is `check-constructions.py` here).\n\n**This corpus.** `research/two-class-lower-bounds.md` §1, §3, §4b, §4c, §5; `research/history/staging/import-hypergraph.md` §4; `research/history/staging/import-hypergraph-prereg.md`; `research/history/staging/redteam-0820-math.md` §3.3 to §3.4; `research/covering-dive.md` §4.2; `research/G2-STATE.md` §3a; `research/SEARCH-CONVENTIONS.md` §1, §3, §4; `research/PRIOR-ART.md`; `paper/kk-lower-bound.md` §1, §3, §9, §11, §12; `paper/beta2-note.md`; `paper/proposals/prop-xlnx-lower-bound.md`; `paper/proposals/prop-kk-lower-bound.md`; `paper/proposals/PROPOSALS.md`.\n\n---\n\n## Appendix A. Provenance of every number\n\n| number | where it appears | source |\n|---|---|---|\n| 2, 6, 12, 30, 42, 66, 108 | §1.1 | G₂ ladder, `paper/beta2-note.md`; rebuilt from scratch for x = 5 to 17 in `n5-verify-out.txt` |\n| 4.26645… | §1.1 | `paper/beta2-note.md`; twenty-digit value Booker and Browning per `research/SEARCH-CONVENTIONS.md` §4 |\n| 22 terms to x = 79 | §1.1 | OEIS A144311 via `paper/kk-lower-bound.md` §1.2 |\n| C₂ = 0.6601618 | §2 | partial product to 2·10⁷ in `mertens-check-out.txt`, agreeing with the literature value |\n| e^{−2γ} = 0.31524, 4 e^{−2γ} = 1.26095 | §2 | `mertens-check-out.txt` |\n| 2 C₂ e^{−2γ} = 0.4162145; observed V(z) ln²z = 0.4162027 at z = 2·10⁷ | §2, §8.4 | `mertens-check.py`, `mertens-check-out.txt` |\n| 8 C₂ e^{−2γ} = 1.66486 | §3 | `mertens-check-out.txt` |\n| 2137 survivors at z = √y, main term 2203.6, ratio 0.9698; 6210 survivors at z = √y/ln y | §3, §5 | `n5-theorem-literal.txt`, `check-constructions.out`, `mertens-check-out.txt` |\n| y = 200000; z = 13; 9889; 9/182 → 9890.1; 162 primes in [17, 997]; seed 13; 200 trials; 1654; 1731.07; 1730.83; 1153; 1.43; x′ = 10861; 1321 classes; 0 uncovered | §5 | `n5-recipe.md`, `n5-verify-out.txt`; every figure equals `redteam-0820-math.md` §3.4's |\n| 1.98156 = 200000/100930.55 | §5 | `n5-recipe.md` §6 |\n| 1220 primes, x′ = 10711, ratio 2.0123 (greedy, z = √y); 2137, 19597, 1.0326 (injective, z = √y); 1331, 11071, 1.9400 (greedy, z = √y/ln y); 6210, 61871, 0.2930 (injective, z = √y/ln y); 1257 primes, x′ = 10301, ratio 2.1013 (greedy above z = 13) | §5 | `check-constructions.out` (referee report 15's checker, reproduced), `n5-theorem-literal.txt` |\n| x′ ≈ 16400, ratio ≈ 1.2 | §5 | `import-hypergraph-prereg.md`, the N5 prediction |\n| 1 and 119 uncovered under corruption | §5 | `n5-negative-control.txt` |\n| 2.29 s, 240 MB, 0.30 s, 1.1 s | §5 | `n5-recipe.md`, `mertens-check-out.txt` |\n| 10^{134.1} (all-constants-one estimate, a floor on the onset) | §6 | `research/two-class-lower-bounds.md` §4c; `paper/kk-lower-bound.md` §8 |\n| ll x/lll x = 3.21 at x = 10¹⁰⁰ | §6 | `mertens-check-out.txt` |\n| 0.1496 against 0.02 | §9 | `redteam-0820-math.md` §3.4 |\n| 1217 problems, #687, #970 | §7 | `research/covering-dive.md` Q5 |\n| 469aaa3 | §9 | `import-hypergraph-prereg.md` custody line, `prop-xlnx-lower-bound.md` §2 |\n\nFiles produced for this note and their sha256:\n\n| file | sha256 |\n|---|---|\n| `verify-cover.py` | ece0d1548d3c8c43889154f5ba0471a208ea1f3b60999eca513e8c7b8e844fa1 |\n| `n5-recipe.md` | 3fe9830ec7f6ae8d6515ed04392d0a4c49ac91a104eaa5cb4678ddec982db75a |\n| `n5-cover.json` | 1b73e1d4a574bab9c98d7e611869611f2c504428cc7f68a479c4b8a3b646f7b1 |\n| `n5-verify-out.txt` | cf7bc45c24d74f91c2821cc135b8f048df46bedf95f3523391bfe96150e61571 |\n| `n5-negative-control.txt` | 73ddd8d2d536cbdc4028737a0521a819b8c43eeb9e7715e10c915606c8be1be0 |\n| `n5-theorem-literal.txt` | d12599a84a6f4f2fd32008d5c0d089ce261288b2eb857592c1f1ae9cb5cccf36 |\n| `n5-embed-check.txt` | b4726e7f6683c357698fa9e3458e5e7ed4657354622dd5ddcb4de55ec17abafd |\n| `mertens-check.py` | e7f25abe8031c3a6959ae2bfa59e6183dd503202469dcefecbfe97c2cc2791f6 |\n| `mertens-check-out.txt` (Draft 1 file, with three timing lines) | 985f9f3b07e1f158e4dfb9d1c6d25d567a6bf22ed6b7ac2a49866eb6d68ec713 |\n| stable stdout of `python3 mertens-check.py 20000000` (no timing lines; referee report 15 §2 E) | 1a02897ff5a033866ba120837119a8a2c2cae2183e5dc182260a41e3688020d5 |\n| `check-constructions.py` (referee report 15 §5, saved verbatim) and `check-constructions.out` | uploaded with this revision |\n\nServed inputs: `research/import-hypergraph-01-instance.js` c186818de4ebf28edba158ad816667f8b01c9dea07c1f15b87f21260bba19370; `research/qc/embed.js` eedf53eb0c6ecda0aa8aee0eebe1533d60d07e923fce52b3bd1cb4a3b43c2a3a; `research/qc/tailfmt.js` ad688e4769b535c0b5cc27c526c1df7c091e9cb9ad4f4fc8beca975b5d6578b7.\n\n## Appendix B. Custody residuals in the underlying records\n\nListed, not silently fixed.\n\n1. `import-hypergraph.md` §4 step 2 and `redteam-0820-math.md` §3.3 item 2 write the two-class Mertens product as (C₂ + o(1))/ln²z; the constant is 4 C₂ e^{−2γ} (§2). `paper/kk-lower-bound.md` §9 step 2 repeats it and then names the constant C₃ without defining it.\n2. `prop-xlnx-lower-bound.md` §1 states the CRT consequence as G₂(x#) ≥ y − O(1); Proposition 1 gives y + 1.\n3. `redteam-0820-math.md` §3.4 describes the finite rebuild as \"seed 13, 200 trials, greedy mop-up\" without stating that its fixed stage stops at z = 13, so a reader takes the echo for the theorem's two-stage construction; it is a three-stage one (§5).\n4. `covering-dive.md` §4.2, `redteam-0820-math.md` §3.3 and `prop-xlnx-lower-bound.md` §1 to §2 carry \"published theorem consumed as a theorem, read at source\" for [KK] Corollary 1 without the proof slip that `paper/kk-lower-bound.md` §11.2 records.\n5. `redteam-0820-math.md` §3.3's rendering of [KK] Lemma 1's hypotheses omits |r_d| ≤ g(d) (§8.1).\n6. `two-class-lower-bounds.md` §4b's mop-up capacity 2x/ln x assumes two survivors per prime without an argument; the proof as written out uses one (§3).\n\n## Appendix C. Registry updates this draft implies\n\nProposed, not made, since this note is written under a fence that permits no edits to existing files.\n\n- `paper/proposals/PROPOSALS.md`, row `prop-xlnx-lower-bound.md`: the draft now exists as its own file; the row's parenthetical should point here as well as at `kk-lower-bound.md` §§3, 9, 10.\n- `paper/proposals/prop-xlnx-lower-bound.md` §1: replace \"G₂(x#) ≥ y − O(1)\" with \"G₂(x#) ≥ y + 1\"; §1 to §2: qualify \"consumed as a theorem\" for [KK] Corollary 1 with the proof slip and the [HR] citation; §4: add [KK] Remark 1 to the prior-art position.\n- `research/G2-STATE.md` §3a, the x ln x row: the constant threshold 1/(8 C₁ C₂ e^{−2γ}) and the citation to [HR] Theorem 2.2 with [KK] as printed instance.\n- `research/history/staging/import-hypergraph.md` §4 and `research/history/staging/redteam-0820-math.md` §3.3: frozen staging files; the Mertens constant slip is recorded here (Appendix B item 1) and in `research/history/CHANGELOG.md` if the owner wishes, not edited in place.\n\n*Superseded claims are recorded in `research/history/CHANGELOG.md`.*\n\n"}