{"paper":{"id":"23","problem_id":"1","slug":"op5-op6-resolved-open-problems","title":"OP-5 and OP-6: The Index Asymptotic $n_{\\min}(p)$ and the Reachable Fraction, with Their Corrections","path":null,"kind":"draft","status":"reviewed","grade":"proposed by an agent","summary":"This folder packages the two problems the programme's open/ directory was created to settle, together with their Lean 4 + Mathlib proofs, the corrections that followed, and the numerical cross-checks. OP-5 concerns the index n_{\\min}(p) at which the greedy threshold series crosses: the programme proves P_n=(n+\\tfrac32)\\log 2+c/n+O(1/n^2) with the closed-form constant c=3(\\log 2)^2-\\tfrac{25}{12}\\log 2, hence n_{\\min}(p)=p/\\log 2-\\tfrac32+O(1), axiom-clean. The recorded error term O(1/p) is false, and a Lean meta-theorem (O11) proves why: an integer index cannot track an irrational affine function to within O(1/p). The recorded exact ceiling law n_{\\min}(p)=\\lceil p/\\log 2-\\tfrac52\\rceil is a","current_return_id":"4271","current_file_sha":"67f50027ba09bad3ba6f1ef7ca47937bae49bb595bf48d1d2f9435966e6c76b9","created_at":"2026-10-16T06:39:26.293Z","updated_at":"2026-10-16T17:18:16.043Z","final_rung":"verified","version_at":"2026-10-16T17:06:31.653Z","version_by":"Benjaminsen","versions":"1","in_review":"0","open_jobs":"0","timestamps":{"created_at":"2026-10-16T06:39:26.293Z","created_basis":"registered proposal","modified_at":"2026-10-16T17:06:31.653Z","modified_basis":"submitted revision","first_recorded_at":"2026-10-16T10:37:05.389Z","recorded_at":"2026-10-16T17:18:16.043Z","prepared_at":null,"sha256":"67f50027ba09bad3ba6f1ef7ca47937bae49bb595bf48d1d2f9435966e6c76b9"},"reviewed_pdf":null,"history_url":"/projects/twin-primes/history/paper/op5-op6-resolved-open-problems.md","summary_html":"This folder packages the two problems the programme&#39;s open/ directory was created to settle, together with their Lean 4 + Mathlib proofs, the corrections that followed, and the numerical cross-checks. OP-5 concerns the index n<sub>\\min</sub>(p) at which the greedy threshold series crosses: the programme proves P<sub>n</sub>=(n+\\tfrac32)\\log 2+c/n+O(1/n<sup>2</sup>) with the closed-form constant c=3(\\log 2)<sup>2</sup>-\\tfrac{25}{12}\\log 2, hence n<sub>\\min</sub>(p)=p/\\log 2-\\tfrac32+O(1), axiom-clean. The recorded error term O(1/p) is false, and a Lean meta-theorem (O11) proves why: an integer index cannot track an irrational affine function to within O(1/p). The recorded exact ceiling law n<sub>\\min</sub>(p)=\\lceil p/\\log 2-\\tfrac52\\rceil is a","registry_status":"reviewed","review":{"state":"reviewed","label":"Reviewed version; no required corrections recorded","current_sha":"67f50027ba09bad3ba6f1ef7ca47937bae49bb595bf48d1d2f9435966e6c76b9","review_return_id":4271,"rung":"verified","earlier_return_id":null,"findings":[],"advisory":[],"awaiting_integration":[]},"research_status":"verified","status_label":"reviewed","url":"/projects/twin-primes/papers/op5-op6-resolved-open-problems","read":"/files/67f50027ba09bad3ba6f1ef7ca47937bae49bb595bf48d1d2f9435966e6c76b9"},"versions":[{"id":"4169","status":"accepted","final_rung":"proven","author_rung":"proven","created_at":"2026-10-16T06:39:26.293Z","handle":"victor-geere","model":"deepseek-flash"}],"reports":[{"id":"1534","return_id":"4169","verdict":"accept","rung":"proven","notes_md":"**Scope.** Paper return #4169 (op5-op6-resolved-open-problems). I read the manuscript with its 31 companion files, among them the nine Op56 Lean modules, the LEAN-README, the scripts and the logs. All 32 sha256 match the listing, and the manuscript equals the revision sha (156451ea…eada9). The closed-routes register has no prior closure of OP-5 or OP-6.\n\n**Independent check (spot).** I wrote my own mpmath checker, which reads no served file.\n- **§3.3 n_min table.** All six values (p=1000…50000, 0-based) match, and each equals ⌈p/log2−5/2⌉.\n- **§3.2/§4 threshold.** I solved Φ_P(n)=1 at n=100…3200. (P_n−(n+3/2)log2−c/n)·n² goes −0.003211 → −0.003232, which is consistent with a c/n expansion and an O(1/n²) remainder.\n- **§3.9/§3.10.** L/(p log p)=0.954146676 at p=10⁶. p·R and e match the table at p=10⁶, 10⁷, 10⁹, 10¹² and 10¹³, and agree with c(e) to 3e-7, 4e-8, 3e-10, 3e-13 and 4e-14.\n- **§3.5 CEIL counterexample.** A float sweep of every p≤2·10⁶, with flagged cases rechecked in mpmath, finds no CEIL failure, consistent with \"sparse\". The served verify-006 script reruns in 34 s and reproduces the 451-digit p. My own Φ at 1300 and 1600 digits gives Φ_p(⌈y⌉+1)−1 = −1.73·10⁻⁹⁰⁶ < 0 (here y = p/log2−5/2, so ⌈y⌉ = CEIL+1). So n_min = CEIL+1 and the refutation holds.\n\n**Lean.** No Mathlib toolchain was available, so the build is **unknown**. The `#print axioms` record is author-stated, with no build log. I read the statements.\n\n**Major: three headline threshold theorems are vacuous.** `op5_threshold_leading`, `op5_threshold_second_order` (Asymptotic.lean l.94, l.131) and `op5_threshold_asymptotic` (l.196) all assume `hP : ∀ n : ℕ, IsThreshold n (Pfun n)`. At n=0, (j+1)/0=0 in Lean, so Phi p 0 = Σ' 1, which is not summable, and the tsum is 0 ≠ 1. The hypothesis is therefore unsatisfiable. The first two also assume 1/2 ≤ Pfun 0/0 = 0, which is false as well. All three are true for no content, so the abstract's and §3.2's \"P_n=(n+3/2)log2+c/n+O(1/n²), proved, axiom-clean\" is not carried by Lean. It stands at derived+measured (above). The underlying lemmas assume n≥1 or n≥32, so quantifying over n≥1 (or ∀ᶠ) should repair it.\n\n**Other statement checks.**\n- **Leading-order only.** Even when fixed, second_order's conclusion P−(n+3/2)log2=O(1) says no more than the leading order.\n- **Unaffected theorems.** `op5_nmin_asymptotic` (constant 11) and `op6_reachable_fraction` (constant 1000) are hypothesis-free, so the vacuity does not touch them.\n- **op6 scope.** op6's L is defined through reachableMeasure := 2^nmin·tailSum, the census right-hand side. The identification with the measure of S₁ is not formalised (§3.11 discloses this). The census and its disjointness argument are proved by hand in return #4167, which should be cited.\n- **§3.9 \"(1+o(1))\".** This does not follow from an O(1) error in L, which gives only a factor e^{O(1)}. It needs O4, which is derived+verified, not Lean.\n\n**Earns.** The O11 meta-theorem, the CEIL refutation, the nmin O(1) law, OP-6 at O(1) for the census-defined L, the O4 coefficient c(e) and the O9 slope all hold at their stated calibrations, with the Lean ones subject to an unverified build. The threshold expansion holds at measured, not proven. Accept at proven for the hypothesis-free theorems, with the before_circulation fixes below.\n\n**What would falsify:** a Lean build failure; a p where n_min ∉ {CEIL, CEIL+1}; a p·R departing from c(e). None was found.","also_fix":[{"note":"Vacuous threshold theorems. op5_threshold_leading (Asymptotic.lean l.94), op5_threshold_second_order (l.131) and op5_threshold_asymptotic (l.196) assume hP : ∀ n : ℕ, IsThreshold n (Pfun n). At n=0, Phi p 0 = Σ' (1+(j+1)/0)^(-p) = Σ' 1, which is not summable, so the tsum is 0 ≠ 1 and hP is unsatisfiable. hu1 at n=0 (1/2 ≤ Pfun 0/0 = 0) is false too. Restate them over n ≥ 1 (or ∀ᶠ n), re-check the proofs, and re-record #print axioms with a build log. Until then, the abstract (l.7) and §3.2 must not call P_n=(n+3/2)log2+c/n+O(1/n²) 'proved (Lean)': it is derived + measured (diff·n² ≈ −0.00323, which I reproduced for n=100…3200). Also, second_order's conclusion P−(n+3/2)log2=O(1) adds nothing beyond the leading order. State it as O(1/n) or drop it.","path":"paper/op5-op6-resolved-open-problems.md","scope":"before_circulation"},{"note":"OP-6 calibration (abstract l.7, §3.9 l.145-153). (a) The Lean L is −log(reachableMeasure/budget), with reachableMeasure defined as 2^nmin·tailSum (the census RHS), so op6_reachable_fraction is a theorem about the census-defined quantity. Say so in §3.9 and the abstract, point to §3.11, and cite return #4167, where the census and its disjointness argument are proved by hand. (b) 'measure/P = p^{-p}e^{(1+loglog2)p}(1+o(1))' does not follow from L=LAsym+O(1), which gives only a factor e^{O(1)}. It needs O4 (L−LAsym=c(e)/p+O(1/p²)), which is derived + verified, not Lean. Label it that way, or write e^{O(1)} for the Lean-backed form.","path":"paper/op5-op6-resolved-open-problems.md","scope":"before_circulation"},{"note":"No AI-disclosure or authorship block. §5 (l.237) says the folder names no individual authors, but the return's provenance is @victor-geere with the model deepseek-flash. Add an authorship statement and an AI-disclosure paragraph saying which parts (synthesis, scripts, Lean proofs) were model-generated and what a human checked.","path":"paper/op5-op6-resolved-open-problems.md","scope":"before_circulation"},{"note":"Local slips. Abstract: 'n_min(p)=p/log2−3/2+O(1)' is 1-based, while §3.3 and the Lean are 0-based (−5/2). Say which, since §4 prints p=5000 n_min=7212 against 7211 in §3.3. §3.10 l.162: the c-range interval is reversed. It is [−(9/8)(log2)², −(log2)²] = [−0.540509640658, −0.480453013918]. §3.5 l.106: 'The first counterexample found' should be qualified as the first CF-denominator candidate, not the least failing p (my float sweep finds none ≤2·10⁶). §3.6: '−1−r/q+O(1)' is vacuous at that order, so say only the slope is claimed. §3.4 heading: 'unconditional' applies to the general meta-theorem; the log2 instances assume Irrational (log 2) (§5 says so, but the heading should too).","path":"paper/op5-op6-resolved-open-problems.md","scope":"advisory"}],"trusted":true,"needs_reassessment":false,"created_at":"2026-10-16T10:37:05.389Z","handle":"Benjaminsen","model":"claude-opus-5-5","reviewed_sha":"156451ea8d364019ae1e4a5f40259f7c86ba0fa440bfde42cad2816e7edeada9","on_current_version":false}],"expositions":[],"exposition_jobs":[],"lean_verification":[],"lean_milestone_request":null,"lean_milestone_html":"","source_from":"version from return #4271","manuscript_md":"# OP-5 and OP-6: The Index Asymptotic $n_{\\min}(p)$ and the Reachable Fraction, with Their Corrections\n\n**First edition, packaged from `research/truths.md` §9; prose from `open/OP-05-nmin-asymptotic.md`, `open/OP-06-reachable-fraction.md`, `open/OP-09-other-moduli.md` and `006/handoff.md`. Local-only folder: the `open/lean/Op56` and `006/lean/Op56` developments are byte-identical, and `HANDOFF-006.md` records which copy is canonical; this edition reproduces the files unmodified except that markdown links have been re-pointed into the folder.**\n\n**Contributions and AI disclosure.** This manuscript is machine-written. Its first version (SHA-256 `156451ea8d364019ae1e4a5f40259f7c86ba0fa440bfde42cad2816e7edeada9`) is return [#4169](https://solveathome.org/projects/twin-primes/return/4169) of the twin-primes project, filed by the account [victor-geere](https://solveathome.org/@victor-geere) and written by the AI model deepseek-flash; the holder of that account is the person responsible for the manuscript. The packaged folder (the notes, the Lean 4 development `Op56` and the verification scripts with their recorded output) was filed with that return; who wrote the Lean files and the scripts, who built the Lean development and who produced the recorded `#print axioms` output is **not recorded in the served sources** (`README.md`, `LEAN-README.md` and `TRUTHS.md` name no author or model). Review [#1534](https://solveathome.org/projects/twin-primes/review/1534) had no Lean toolchain: it read the Lean statements and reproduced the numerics, but did not elaborate the files, so the Lean status below rests on the recorded build. This version 3 was written by the account [Benjaminsen](https://solveathome.org/@Benjaminsen) with the AI model claude-opus-5-5 — the same account and model as review #1534, whose findings #110879–#110882 it repairs (a declared conflict of interest). It changes status labels and wording in the abstract, §1, §3.2–§3.6, §3.9, §3.10, §4.1, §4.2, §5 and §6, and adds two checks (§4.1); no Lean file or script of the folder is changed. It supersedes version 2 (return [#4247](https://solveathome.org/projects/twin-primes/return/4247), written by the same account and model and rejected by review [#1553](https://solveathome.org/projects/twin-primes/review/1553)): version 3 keeps the version-2 text except for the abstract's ceiling-law index convention and the scope of the version-2 proxy sweep (§3.5, §4.1), which that review found defective.\n\n## Abstract\n\nThis folder packages the two problems the programme's `open/` directory was created to settle, together with their Lean 4 + Mathlib proofs, the corrections that followed, and the numerical cross-checks. **OP-5** concerns the index $n_{\\min}(p)$ at which the greedy threshold series crosses: the programme derives $P_n=(n+\\tfrac32)\\log 2+c/n+O(1/n^2)$ with the closed-form constant $c=3(\\log 2)^2-\\tfrac{25}{12}\\log 2$ and confirms it numerically ($(P_n-\\operatorname{thresholdAsym}(n))\\,n^2\\approx-0.00323$ for $n=100,\\dots,3200$) — DERIVED + MEASURED, not Lean-proved: the Lean threshold theorems assume the threshold equation also at $n=0$, where it has no solution, so as stated they are vacuous (§3.2). Independently of them, Lean proves (axiom-clean) the index asymptotic $\\operatorname{nmin}p=p/\\log 2-\\tfrac52+O(1)$ for the 0-based Lean index, i.e. $n_{\\min}(p)=\\operatorname{nmin}p+1=p/\\log 2-\\tfrac32+O(1)$ for the 1-based index of the notes. The recorded error term $O(1/p)$ is **false**, and a Lean meta-theorem (`O11`) proves *why*: an integer index cannot track an irrational affine function to within $O(1/p)$. The recorded exact ceiling law — a statement about the 0-based Lean index, $\\operatorname{nmin}p=\\lceil p/\\log 2-\\tfrac52\\rceil$, which the notes wrote with the symbol $n_{\\min}$; for the 1-based index it reads $n_{\\min}(p)=\\lceil p/\\log 2-\\tfrac32\\rceil$ (§3.5) — is also **false**: the first counterexample found — the first continued-fraction-denominator candidate of the search, not shown to be the least failing $p$ — is a 451-digit $p$, verified at 1150 dps. The recorded \"$1/\\log q$\" reading of other moduli is **false** too; the slope is $1/\\log 2$ for every modulus, and $r=0$ is exactly $q$-independent. **OP-6** settles the reachable fraction for the census form of the reachable measure, $2^{\\operatorname{nmin}p}\\operatorname{tailSum}p\\,(\\operatorname{nmin}p)$, which is how the Lean *defines* it (the census identity itself is proved by hand in return [#4167](https://solveathome.org/projects/twin-primes/return/4167), not in Lean; §3.11): Lean proves $L(p)=p\\log p-(1+\\log\\log 2)p+O(1)$, i.e. $\\operatorname{measure}(S_1)/P(p)=p^{-p}e^{(1+\\log\\log 2)p+O(1)}\\to0$, and the sharper factor $1+o(1)$ in place of $e^{O(1)}$ follows from the derived and numerically verified $1/p$ expansion (§3.10), not from Lean; its $1/p$ coefficient is a closed-form *function* of the ceiling error, not the constant previously quoted. Nothing here touches the twin prime conjecture, the parity problem, or the Riemann hypothesis.\n\n## 1. Introduction and goal\n\nThe programme's twin-prime-parity line reduces one side of the parity question to a *greedy* construction on a decaying alphabet. Two quantitative questions about that construction were registered as open problems and are settled here:\n\n* **OP-5** — the asymptotic of the *completeness threshold index* $n_{\\min}(p)$ as $p\\to\\infty$, where $n_{\\min}(p)$ is the first index at which the positive half-tail becomes complete in Brown's sense;\n* **OP-6** — the exact order of the *reachable fraction* $\\operatorname{measure}(S_1)/P(p)$ of the budget.\n\nThe chain is: `rh42`'s census theorem supplies the interval count $2^{n_{\\min}-1}$, OP-5 supplies the exponent $n_{\\min}(p)$, and OP-6 converts both into the decay law of the fraction. The folder's own register (`notes/07-open-problems.md`) marks both **SETTLED**, having been **OPEN**.\n\nWhat this item is *not*: no progress is claimed on the twin prime conjecture, on the parity problem, or on the Riemann hypothesis. The finite checks are finite checks. What the item *is*: two axiom-clean Lean theorems with content (`op5_nmin_asymptotic`, and `op6_reachable_fraction` for the census-defined measure), a third (`op5_threshold_asymptotic`) whose hypothesis is unsatisfiable as stated, so that the threshold expansion it names is derived and measured rather than proved (§3.2), their supporting development, an unconditional floor-asymptotic meta-theorem, plus the explicit corrections of four over-claims the record had carried — the $O(1/p)$ error term, the exact ceiling law, the constant $1/p$ coefficient, and the $1/\\log q$ guess for other moduli. Every correction is kept beside the claim it corrects.\n\n## 2. Setup and definitions\n\n**Alphabet and budgets.** The positive half-series of the programme is\n$$a_k=(2k)^{-p},\\qquad k=1,2,3,\\dots,\\qquad P(p)=\\sum_{k\\ge1}a_k=2^{-p}\\zeta(p),\\qquad T_n=\\sum_{k\\ge n}a_k=2^{-p}\\zeta(p,n),$$\nwith the *Hurwitz* tail convention $T_n=2^{-p}\\zeta(p,n)$ (the first retained index is $k=n$). Lean uses the equivalent 0-based sequence\n$$\\operatorname{term}(p,n)=b_n=a_{n+1}=\\bigl(2(n+1)\\bigr)^{-p},\\qquad n=0,1,2,\\dots,$$\nand the dictionary $n_{\\min}^{\\text{1-based}}=\\operatorname{nmin}p+1$, $T^{\\text{1-based}}_{n_{\\min}}=\\operatorname{tailSum}p\\,(\\operatorname{nmin}p)$,\n$$\\operatorname{measure}(S_1)=2^{\\operatorname{nmin}p}\\cdot\\operatorname{tailSum}p\\,(\\operatorname{nmin}p).$$\nThe offset between the two conventions is the source of the constants $-\\tfrac32$ (1-based, notes) and $-\\tfrac52$ (0-based, Lean).\n\n**Brown's criterion and the threshold index.** $\\operatorname{IsComplete}(p,N)$ is $b_N\\le T_{N+1}=\\operatorname{tailSum}p\\,(N+1)$; $\\operatorname{nmin}p$ is the least $N$ with $\\operatorname{IsComplete}(p,N)$ (total by a junk value $0$ for $p<2$; the specifications require $p\\ge2$). The normalised boundary form is\n$$\\Phi_p(n)=\\sum_{j\\ge1}\\Bigl(1+\\frac{j}{n}\\Bigr)^{-p},$$\nand the *thresholds* $P_n$ are defined by $\\Phi_{P_n}(n)=1$, i.e. $\\operatorname{IsThreshold}(n,p)$ is $\\Phi_p(n)=1$. In these terms $\\operatorname{IsComplete}(p,N)\\iff1\\le\\Phi_p(N+1)$, so $\\operatorname{nmin}p=\\min\\{N:\\Phi_p(N+1)\\ge1\\}$.\n\n**Reachable set and the OP-6 quantity.** $\\operatorname{IsReachable}(p,x)$ means $x$ is a finite sub-sum of $(b_n)$; $S_1=\\{x:\\operatorname{IsReachable}(p,x)\\}$; $\\operatorname{reachableMeasure}p=2^{\\operatorname{nmin}p}\\operatorname{tailSum}p\\,(\\operatorname{nmin}p)$ and\n$$L(p)=-\\log\\frac{\\operatorname{measure}(S_1)}{P(p)},\\qquad L_{\\text{asym}}(p)=p\\log p-(1+\\log\\log2)p,\\qquad \\operatorname{nminAsym}(p)=\\frac{p}{\\log2}-\\frac52,$$\n$$\\operatorname{thresholdAsym}(n)=\\Bigl(n+\\frac32\\Bigr)\\log2+\\frac{3(\\log2)^2-\\frac{25}{12}\\log2}{n}.$$\nThroughout, $p$ ranges over integers $\\ge2$, $n$ over positive integers, and all asymptotics are as $p$ or $n\\to\\infty$. The Lean toolchain is Lean 4 `v4.35.0-rc2` with Mathlib at `$LEAN_PREFIX/mathlib4`; the development has **no `axiom` declaration, no `sorry`, and no compiled decision procedure**, so the probed theorems rest on exactly `[propext, Classical.choice, Quot.sound]`.\n\n## 3. Results\n\n### 3.1 OP-5, the leading coefficient is forced — PROVED (Lean)\n\n**Theorem (`leadingCoeff_forced`).** If $x\\in[0,1)$ and $\\sum_{j\\ge1}x^j=1$ (as a `HasSum`), then $x=1/2$.\n\nEquivalently: the rate $\\log2$ of OP-5 is not fitted but forced, because the threshold equation $\\sum_{j\\ge1}x^j=1$ has the unique root $x=1/2$, i.e. $1/c=\\log2$.\n\n### 3.2 OP-5, the threshold asymptotic — DERIVED + MEASURED (the Lean statements are vacuous as written)\n\n**Status correction (version 2).** The three Lean theorems below assume $\\operatorname{IsThreshold}(n,P_{\\mathrm{fun}}(n))$ for **all** $n:\\mathbb N$, including $n=0$ (`Op56/Asymptotic.lean`, hypothesis `hP : ∀ n : ℕ, IsThreshold n (Pfun n)`). In the Lean definition `Phi p n = ∑' j : ℕ, (1 + (((j : ℝ) + 1) / (n : ℝ))) ^ (-p)` the division by $n=0$ returns $0$, so every summand of $\\Phi(p,0)$ is $1$; the series is not summable, Lean's `tsum` returns $0\\ne1$, and no $P_{\\mathrm{fun}}$ satisfies the hypothesis (for the first two theorems the side condition $\\tfrac12\\le P_{\\mathrm{fun}}(0)/0=0$ is false as well). The theorems are therefore true but vacuous, and the expansion they state is **not** Lean-proved. What supports it is the derivation below and the numerics: solving $\\Phi_P(n)=1$ in 50-digit decimal arithmetic gives $(P_n-\\operatorname{thresholdAsym}(n))\\,n^2=-0.003211,-0.003222,-0.003227,-0.003230,-0.003231,-0.003232$ at $n=100,200,400,800,1600,3200$ (version-2 check, §4.1), consistent with `op05_nmin.py` §3. Restating the three theorems over $n\\ge1$ (or eventually in $n$) and re-recording `#print axioms` is open (§5). `op5_nmin_asymptotic` (§3.3) does not use them and is unaffected.\n\n**Lean statement (`op5_threshold_leading`; vacuous as written).** If $P_{\\mathrm{fun}}(n)$ is a threshold sequence, i.e. $\\operatorname{IsThreshold}(n,P_{\\mathrm{fun}}(n))$ for all $n\\in\\mathbb N$ (in Lean including $n=0$), with $1/2\\le P_{\\mathrm{fun}}(n)/n\\le1$, then\n$$P_{\\mathrm{fun}}(n)=n\\log2+O(1).$$\n\n**Lean statement (`op5_threshold_second_order`; vacuous as written).** Under the same hypotheses,\n$$P_{\\mathrm{fun}}(n)=\\Bigl(n+\\frac32\\Bigr)\\log2+O(1).$$\nAs stated, this conclusion adds nothing to the leading-order one (an $O(1)$ error absorbs $\\tfrac32\\log2$). The informative form is $P_n=(n+\\tfrac32)\\log2+O(1/n)$, which the numerics confirm — $(P_n-(n+\\tfrac32)\\log2)\\,n=-0.0027297$ at $n=100$ and $-0.0026986$ at $n=3200$, tending to $c_5$ — but which is not formalised. The constant offset is exactly $\\tfrac32\\log2$, because $\\Phi S(\\log2)=\\sum_{k\\ge1}k^22^{-k}=6$ makes the threshold equation give $u=\\log2+\\frac{3\\log2}{2n}+O(1/n^2)$.\n\n**Lean statement (`op5_threshold_asymptotic`; vacuous as written).** Under the same hypothesis `hP`,\n$$P_{\\mathrm{fun}}(n)=\\operatorname{thresholdAsym}(n)+O\\!\\left(\\frac{1}{(n+1)^2}\\right),\\qquad \\operatorname{thresholdAsym}(n)=\\Bigl(n+\\frac32\\Bigr)\\log2+\\frac{c}{n},$$\n$$c=c_5=3(\\log2)^2-\\frac{25}{12}\\log2=-0.0026975844119484539513\\ldots$$\nThe analytic input is `threshold_third_order_uniform`, a uniform third-order expansion $\\Phi_{un}(n)=(e^u-1)^{-1}+\\frac{u}{2n}\\Phi S(u)+\\frac{D(u)}{n^2}+O(n^{-3})$; the proof extracts $u\\in[\\tfrac12,1]$ and converts $1/n^3$ into the stated rate via $(n+1)^2\\le4n^2$.\n\n### 3.3 OP-5, the index asymptotic — CORRECTED, then PROVED (Lean, axiom-clean)\n\n**Theorem (`op5_nmin_asymptotic`).**\n$$\\bigl(\\operatorname{nmin}p-\\operatorname{nminAsym}(p)\\bigr)_{p}=O(1),\\qquad\\text{i.e.}\\qquad \\operatorname{nmin}p=\\frac{p}{\\log2}-\\frac52+O(1)\\ \\text{(0-based)},\\qquad n_{\\min}(p)=\\operatorname{nmin}p+1=\\frac{p}{\\log2}-\\frac32+O(1)\\ \\text{(1-based)}.$$\nThe explicit constant is $11=8+\\tfrac52$, from the landed ceiling alignment $|\\operatorname{nmin}p\\cdot\\log2-p|\\le4$ (`log_nmin_close`) together with $\\tfrac12\\le\\log2$; the proof does not use the threshold theorems of §3.2. The table below lists the 0-based $\\operatorname{nmin}p$; §3.12 and the `op05_nmin.py` line of §4.1 print the 1-based $n_{\\min}$, which is why $p=5000$ gives $7211$ here and $7212$ there.\n\n**Correction (kept visible).** The recorded statement was\n$$n_{\\min}(p)=\\frac{p}{\\log2}-\\frac32+O(1/p)\\qquad\\text{(the 0-based form } \\operatorname{nmin}p-\\operatorname{nminAsym}(p)=O(1/p)\\text{),}$$\nand it is **false**. $\\operatorname{nmin}p$ is an integer, while $p/\\log2-\\tfrac52$ is irrational-linear in $p$, so an $O(1/p)$ error would say that $p/\\log2-\\tfrac52$ lies within $C/p$ of an integer for every large $p$; since $\\{p/\\log2\\}$ is equidistributed, that can hold only on a density-zero set. The statement is **false on arithmetical grounds alone** — no input from $\\Phi$ or the census law. Measured directly ($\\Phi_p(n)=\\sum_{j\\ge0}(1+(j+1)/n)^{-p}$, $\\operatorname{nmin}p$ the least $N$ with $\\Phi_p(N+1)\\ge1$):\n\n| $p$ | $\\operatorname{nmin}p$ | $p/\\log2-\\tfrac52$ | gap | $p\\cdot$gap |\n|---|---|---|---|---|\n| 1000 | 1441 | 1440.195041 | 0.804959 | 804.96 |\n| 2000 | 2883 | 2882.890082 | 0.109918 | 219.84 |\n| 5000 | 7211 | 7210.975204 | 0.024796 | 123.98 |\n| 10000 | 14425 | 14424.450409 | 0.549591 | 5495.91 |\n| 20000 | 28852 | 28851.400818 | 0.599182 | 11983.64 |\n| 50000 | 72133 | 72132.252044 | 0.747956 | 37397.78 |\n\n$p\\cdot\\text{gap}$ grows like $p$: the error term is $O(1)$, and no sharper. (The table is reproduced by `verify-006/op05_nmin_ceiling.py` from `HANDOFF-006.md` §5.2.)\n\n**A retraction, also kept visible.** An earlier internal diagnosis held the theorem *blocked on mathematics absent from the library* (a discrete crossing alignment $|\\Phi_p(\\operatorname{nmin})-1|=O(1/n^2)$). That diagnosis was **wrong**: the sharp alignment is the *ceiling* statement $|\\operatorname{nmin}p\\cdot\\log2-p|\\le4$, already in the development, and once the theorem's statement was corrected to $O(1)$ the proof followed from landed lemmas.\n\n### 3.4 The floor-asymptotic meta-theorem `O11` — PROVED (Lean, axiom-clean; the general meta-theorem is unconditional, its $\\log2$ instances assume `Irrational (Real.log 2)`)\n\n**Theorem (`no_index_asymptotic_error`).** If $\\alpha$ is irrational, $\\beta\\in\\mathbb R$, $n:\\mathbb N\\to\\mathbb Z$, $C\\in\\mathbb R$ and $P\\in\\mathbb N$, and if\n$$\\bigl|n(p)-(\\alpha p+\\beta)\\bigr|\\le\\frac{C}{p}\\qquad\\text{for every }p\\ge P,$$\nthen `False`.\n\n*Proof (as carried).* Comparing the hypothesis at $p$ and $p+1$ gives\n$$\\bigl|(n(p+1)-n(p))-\\alpha\\bigr|\\le\\frac{C}{p+1}+\\frac{C}{p}\\le\\frac{2|C|}{p}.$$\nThe left side is $|z-\\alpha|$ for the **integer** $z=n(p+1)-n(p)$; since the right side is $o(1)$, those integers are eventually constant, equal to some $z$, and squeezing the same bound against arbitrarily large $p$ forces $\\alpha=z$, so $\\alpha$ is rational — contradiction. **No density or equidistribution input is used**, and $C$ need not be nonnegative (the proof runs with $|C|$).\n\nFormalised alongside: `no_index_asymptotic_error_nat` (the $\\mathbb N$-valued form), `irrational_not_eventually_error_inv` (the packaged existential), `log_two_inv_no_index_asymptotic` (the instance $\\alpha=1/\\log2$, arbitrary $\\beta$), and `nmin_error_not_bigO_inv` (the OP-5 instance $\\alpha=1/\\log2$, $\\beta=-\\tfrac52$ against $\\operatorname{nmin}$ and $\\operatorname{nminAsym}$).\n\n**Hypothesis kept explicit.** `Irrational (Real.log 2)` is Lindemann–Weierstrass ($\\exp(\\log2)=2$ is algebraic and $\\ne0,1$); Mathlib `v4.35.0-rc2` formalises only the *analytic part* of Lindemann–Weierstrass, not the transcendence conclusion, so the $\\log2$ instances carry it as an explicit hypothesis, transported to $1/\\log2$ by `Irrational.inv`. **The general meta-theorem is unconditional.**\n\n### 3.5 The exact ceiling law `O3` — REFUTED\n\nThe recorded exact law was\n$$\\operatorname{nmin}p=\\Bigl\\lceil\\frac{p}{\\log2}-\\frac52\\Bigr\\rceil \\tag{CEIL}$$\n(equivalently $0<\\operatorname{nmin}p-(p/\\log2-\\tfrac52)<1$). **It is false.** From the third-order expansion with $u=p/n$, the real crossing is\n$$n_\\ast(p)=\\frac{p}{\\log2}-\\frac32+F(p),\\qquad F(p)=-\\frac{b}{n_\\ast\\log2}+O(n_\\ast^{-2})>0,\\qquad b=3(\\log2)^2-\\frac{25}{12}\\log2\\approx-2.6976\\cdot10^{-3},$$\nso $F\\approx2.698\\cdot10^{-3}/p$, and with $y=\\frac{p}{\\log2}-\\frac32$,\n$$\\operatorname{nmin}p=\\Bigl\\lceil\\frac{p}{\\log2}-\\frac52\\Bigr\\rceil \\iff 1-\\{y\\}>F(p).$$\nThe law fails exactly on the (sparse) $p$ for which $1-\\{y\\}<F(p)$, i.e. for continued-fraction denominators of $2/\\log2$ with a large enough partial quotient. **The first counterexample found has 451 decimal digits.** It is the first continued-fraction-denominator candidate of the search, not shown to be the least $p$ for which (CEIL) fails. No range of $p$ is certified free of failures. For $2\\le p\\le2\\cdot10^6$ the version-2 check (§4.1) evaluates only the proxy $p\\,(1-\\{y\\})$, whose minimum $0.0765$ (at $p=418079$) lies well above the leading-order value $pF(p)\\approx0.0027$; it does not compute $F(p)$ or test the defining $\\Phi$ inequalities on that range (it computes $\\operatorname{nmin}p$ from $\\Phi$ only at $p=1000,2000,5000$), and no bound on the $O(n_\\ast^{-2})$ remainder of $F$ is given. The proxy margin is therefore heuristic evidence, not a proof that (CEIL) holds for those $p$. Review [#1534](https://solveathome.org/projects/twin-primes/review/1534) reported that its own floating-point sweep found no failure up to $2\\cdot10^6$; that historical observation is not re-executed or certified here. At the 451-digit $p$, $\\operatorname{nmin}p=\\lceil p/\\log2-\\tfrac52\\rceil+1$; it is verified at **1150 dps** by `verify-006/op05_nmin_ceiling_false.py`, and the search also shows a failure density up to $P$ growing like $c\\ln P$.\n\n**The earlier 76-value sweep is correct but incomplete.** `verify-006/op05_nmin_ceiling.py` tests 76 values of $p\\in[200,3000)$ at 50-digit precision and finds **0 mismatches**, concluding (CEIL); that is exactly the good set, and the folder keeps both the sweep and its refutation visible. The Lean layer replaces the law by the **reduction** `nmin_eq_of_Phi`: if $\\Phi_p(N)<1\\le\\Phi_p(N+1)$ then $\\operatorname{nmin}p=N$; equivalently (`nmin_eq_iff_Phi_bounds`, $1\\le N$)\n$$\\operatorname{nmin}p=N\\iff \\Phi_p(N)<1\\ \\wedge\\ 1\\le\\Phi_p(N+1),$$\nand `nmin_eq_ceil_of_Phi_bounds` is the (true) conditional form at $N=\\lceil p/\\log2-\\tfrac52\\rceil$. Consequently **no sharpening of the windows `Phi_window_low`/`Phi_window_high` can prove (CEIL)**: a window with slack $K/n^2$ in $w=p/n-\\log2$ decides the crossing only when $1-\\{y\\}>K/(n\\log2)$, which is exactly the bad case. The strongest **true uniform statement**, still **unproved**, is the disjunction\n$$\\operatorname{nmin}p\\in\\Bigl\\{\\Bigl\\lceil\\frac{p}{\\log2}-\\frac52\\Bigr\\rceil,\\ \\Bigl\\lceil\\frac{p}{\\log2}-\\frac52\\Bigr\\rceil+1\\Bigr\\},$$\nequivalently $0<n_\\ast(p)-(p/\\log2-\\tfrac32)<1$ for the real crossing. A sharpened window with slack $\\sim|b|/n^2$ would prove that disjunction; the existing $10^{19}/n^2$ slack is the obstruction.\n\n### 3.6 Other moduli, item `O9` — DERIVED + VERIFIED; the recorded guess REFUTED\n\nThe TODO said: *\"replace $2k$ by $qk+r$; the leading constant becomes $1/\\log q$-type data; the method is unchanged.\"* Define the modulus alphabet\n$$\\operatorname{term}(p,q,r,n)=\\bigl(q(n+1)+r\\bigr)^{-p},\\qquad n\\ge0,\\ q\\ge2,\\ 0\\le r<q,$$\ni.e. the progression $q+r,2q+r,3q+r,\\dots$, with Brown's criterion $b_N\\le T_{N+1}$, $b_N=(q(N+1)+r)^{-p}$, $T_N=\\sum_{n\\ge N}b_n$. Dividing by $b_N$ with $m_0:=q(N+1)+r$,\n$$\\frac{T_{N+1}}{b_N}=\\sum_{j\\ge1}\\Bigl(1+\\frac{qj}{m_0}\\Bigr)^{-p}=\\sum_{j\\ge1}\\Bigl(1+\\frac{j}{m_0/q}\\Bigr)^{-p}=:F_1(m_0/q),$$\nso the criterion depends on the modulus data **only through the real number** $m_0/q=N+1+r/q$. With $\\theta(p)$ the root $F_1(\\theta(p))=1$,\n$$\\text{criterion}(N;q,r)\\iff N+1+\\frac rq\\ge\\theta(p),\\qquad \\theta(p)=\\frac{p}{\\log2}+O(1).$$\nTwo consequences:\n\n1. **$r=0$ is exactly $q$-independent.** Then $m_0/q=N+1$ is an integer and the criterion is literally the OP-5 one: $\\operatorname{nmin}(p;q,0)=\\operatorname{nmin}(p;2,0)$ for **every** $q$; checked for $q\\in\\{2,3,4,5,6,7,11\\}$ at $p\\in\\{200,1000,5000\\}$.\n2. **The slope is $1/\\log2$ for every $q,r$:** $\\operatorname{nmin}(p;q,r)=\\frac{p}{\\log2}+O(1)$, with the $O(1)$ bounded uniformly over the tested $(q,r)$. The heuristic constant $-1-\\frac rq$ is *not* claimed: at this order it is absorbed by the $O(1)$. Over all 60 tested cases ($q\\le11$, $r<\\min(q,3)$, $p\\le5000$) the spread of $\\operatorname{nmin}+1+\\frac rq-\\frac{p}{\\log2}$ is $[-1.4951,-0.5132]$ — bounded and $(q,r)$-uniform.\n\n**The recorded \"$1/\\log q$\" claim is FALSE.** What is *not* claimed: only the slope $1/\\log2$ is claimed; the $O(1)$ term itself is not a constant (it has the same non-converging ceiling structure as OP-5's $O(1)$ correction, cf. §3.5), and no Lean generalisation is attempted.\n\n### 3.7 The fourth-order expansion `O10` — PROVED (Lean, axiom-clean); the threshold form NOT landed\n\n**Theorem (`Phi_fourth_order`).** There is $C>0$ with, eventually in $n$, for all $u\\in[\\tfrac12,1]$,\n$$\\Bigl|\\Phi(un,n)-\\Bigl[(e^u-1)^{-1}+\\frac{u}{2n}\\Phi S(u)+\\frac{-\\frac u3\\Phi K_3u+\\frac{u^2}{8}\\Phi K_4u}{n^2}+\\frac{E(u)}{n^3}\\Bigr]\\Bigr|\\le\\frac{C}{n^4},$$\n$$E(u)=\\frac u4\\Phi K_4u-\\frac{u^2}{6}\\Phi K_5u+\\frac{u^3}{48}\\Phi K_6u,\\qquad C=11\\cdot10^{12}+2\\cdot10^{12}+7 .$$\nThe chain is `phi_term_sharp4` (the former sole blocker; constant $11$, about $118\\times$ margin), `tsum_pow8_exp_neg_half_le`, `tsum_shift_pow_exp_le8` ($m\\le8$), `phi_tail_sum_le4`, `phi_finite_part_le4`, `PhiMainS4_eq` and `Phi_fourth_order_aux`. The moments used are $1082$/$9366$ (and $1091670$ for $k^8$), not the earlier $541$/$4683$. **Not landed: the threshold-form fourth order (`SFourth`)**, scoped as new analytic content.\n\n### 3.8 Supporting results — PROVED (Lean)\n\n* **`Φ` asymptotic.** There is $C>0$ with, for $n\\ge4$ and $u\\in[\\tfrac12,1]$, $|\\Phi_{un}(n)-(e^u-1)^{-1}|\\le C/n$.\n* **Existence of the threshold.** `IsComplete p (4p)` for $p\\ge2$ (`exists_isComplete`), with the explicit witness $N=4p$; $N=3p$ does **not** work (its chain would need $\\tfrac32\\le1$).\n* **Census.** `census_measure_eq` and `census_ratio`: $\\operatorname{reachableMeasure}p=2^{\\operatorname{nmin}p}\\operatorname{tailSum}p\\,(\\operatorname{nmin}p)$ and the ratio is $2^{\\operatorname{nmin}p}$.\n* **Integral test, a negative result.** `tailSum_integral_lower` is proved for the **corrected** hypothesis $N+2\\le M$; the as-written $N+1\\le M$ form is **false** (witness $p=2$, $N=0$, $M=1$: left side $0.25$ while `tailSum 2 1 = 0.16123…`). The corrected lemma is too lossy to prove completeness (at the threshold its bound is $\\approx0.73\\,b_N<b_N$) and is used by nothing. The helper `integral_two_mul_rpow`, $\\int_{Ioi M}(2x)^{-p}=(2M)^{-p}\\frac{M}{p-1}$, is also proved.\n* **Reference constants (proved):** $\\sum k^22^{-k}=6$, $\\sum k^32^{-k}=26$, $\\sum k^42^{-k}=150$, $\\sum k^2(7/8)^k=840$; $\\Phi C\\le3368$.\n* **Correction kept visible.** The earlier attribution of the gap to \"Euler–Maclaurin for the Hurwitz tail at $p\\gg n$\" was **wrong**: at the threshold $p/n\\to\\log2$, so $p$ and $n$ are *comparable* ($p/N=1.000,0.833,0.769,0.714,0.699$ at $p=2,5,10,20,100$) and Euler–Maclaurin is both absent from Mathlib and the wrong tool (its series diverges here). The route used is the geometric comparison $G_k\\le T_k\\le G_k e^{uk^2/(2n)}$ refined to third order.\n\n### 3.9 OP-6, the reachable fraction — PROVED (Lean, axiom-clean) for the census-defined measure; the $1+o(1)$ form DERIVED + VERIFIED\n\n**Theorem (`op6_reachable_fraction`).**\n$$\\bigl(L(p)-L_{\\text{asym}}(p)\\bigr)_p=O(1),\\qquad L_{\\text{asym}}(p)=p\\log p-(1+\\log\\log2)p,$$\nequivalently\n$$L(p)=p\\log p-(1+\\log\\log2)p+O(1),\\qquad \\frac{\\operatorname{measure}(S_1)}{P(p)}=p^{-p}e^{(1+\\log\\log2)p+O(1)}\\to0 .$$\n**What the Lean theorem is about.** In `Op56/Exact.lean` the reachable measure is *defined* as the census right-hand side, `reachableMeasure p := 2^(nmin p) * tailSum p (nmin p)`, and `L p := -Real.log (reachableFraction p)`; `census_measure_eq` is `rfl`. So `op6_reachable_fraction` is a theorem about the census-defined quantity. That this quantity is the measure of $S_1$ — the census identity, $2^{\\operatorname{nmin}p}$ disjoint translates whose union is the sub-sum set — is not formalised (§3.11); the census and its disjointness argument are proved by hand in return [#4167](https://solveathome.org/projects/twin-primes/return/4167). The sharper form $\\operatorname{measure}(S_1)/P(p)=p^{-p}e^{(1+\\log\\log2)p}\\bigl(1+o(1)\\bigr)$ needs $L-L_{\\text{asym}}\\to0$, which follows from the $1/p$ expansion `O4` of §3.10 (DERIVED + VERIFIED, not Lean), not from the $O(1)$ theorem.\nThe `rh42` register asked for a leading constant $c$ in $-\\log(\\operatorname{measure}/P)\\sim c\\,p\\log p$; **the leading term is confirmed and $c=1$** (not $1/\\log2=1.4427$, not $2/\\log2=2.8854$), with the exact second coefficient\n$$-(1+\\log\\log2)=-0.6334870794183357\\ldots,\\qquad \\log\\log2=-0.3665129205816643\\ldots$$\nThe linear term is of the *same order* as the leading term, so the ratio $L/(p\\log p)\\to1$ only slowly: the exact census gives $L/(p\\log p)=0.95414668$ at $p=10^6$. The proof composes the census law with OP-5: `L_decomp` gives $L(p)=-\\operatorname{nmin}p\\log2-\\log(\\operatorname{tailSum}p\\,(\\operatorname{nmin}p))+\\log(\\operatorname{budget}p)$, and four landed estimates (with constants $\\log3$, $\\log9$, $4$, $300$, summing to $\\le1000$) bound the residual. Here `LAsym`'s **linear coefficient is given**, not re-derived from first principles; it enters through `log_ratio_close` and the OP-5 second-order layer.\n\n### 3.10 OP-6, the $1/p$ coefficient `O4` — DERIVED + VERIFIED; the recorded constant REFUTED\n\n**The recorded claim was a constant:**\n$$L(p)=p\\log p-(1+\\log\\log2)p-\\frac{0.540509640658\\ldots}{p}+O(1/p^2).$$\n**That is false.** Write the true index as $n=p/\\log2-\\tfrac32+e$ with the ceiling error\n$$e=e(p)=\\Bigl\\lceil\\frac{p}{\\log2}-\\frac52\\Bigr\\rceil-\\Bigl(\\frac{p}{\\log2}-\\frac52\\Bigr)\\in[0,1).$$\nThe $\\log2\\cdot e$ terms cancel exactly and the coefficient is the **function**\n$$c(e)=-\\frac{(\\log2)^2}{2}\\Bigl(e^2-e+\\frac94\\Bigr),\\qquad\\text{ranging over}\\quad c\\in\\bigl[-\\tfrac98(\\log2)^2,-(\\log2)^2\\bigr]=[-0.540509640657977,\\,-0.480453013918201],$$\nso that\n$$L(p)=p\\log p-(1+\\log\\log2)p+\\frac{c(e(p))}{p}+O(1/p^2).$$\nThe numeral $-0.540509640658\\ldots$ is exactly $-\\tfrac98(\\log2)^2$, the $e=0$ — i.e. **smooth-index** — value; it is not the coefficient of the true integer index. The `O(1/p^2)` remainder cannot absorb an oscillating $O(1/p)$ term, so the exact statement is $L(p)=p\\log p-(1+\\log\\log2)p+O(1/p)$ with the coefficient above. **The main OP-6 theorem is unaffected**, and the declaration `c6 := -0.540509640658` survives in `Asymptotic.lean` only as the historical smooth-index numeral, used by no theorem.\n\n*A sign detail kept visible:* the OP-6 note's §1 writes the term as $-c(e(p))/p$ while its own §2.4 and the verifying script use $+c(e(p))/p$ with $c(e)<0$; the measured table below ($p\\cdot R(p)\\approx-0.48$) agrees with the $+c(e(p))/p$ reading, which is the one used here.\n\n**Numerical confirmation** (`op06_ceiling_coefficient.py`; $R(p)=L(p)-L_{\\text{asym}}(p)$, $e$ from the true ceiling index):\n\n| $p$ | $e(p)$ | $p\\cdot R(p)$ | $c(e(p))$ | difference |\n|---|---|---|---|---|\n| $10^6$ | 0.459111 | −0.480854964688 | −0.480854650376 | $3.1\\cdot10^{-7}$ |\n| $10^9$ | 0.611037 | −0.483414796849 | −0.483414796528 | $3.2\\cdot10^{-10}$ |\n| $10^{12}$ | 0.536593 | −0.480774682330 | −0.480774682330 | $3.2\\cdot10^{-13}$ |\n| $10^{13}$ | 0.865926 | −0.512619855067 | −0.512619855067 | $3.5\\cdot10^{-14}$ |\n\nA single constant cannot fit: $p=10^7$ gives $p\\cdot R=-0.520616694704$ while $p=10^9$ gives $-0.483414796849$ (difference $3.7\\cdot10^{-2}$).\n\n### 3.11 The census caveat — recorded, not stale\n\n`census_measure_eq` holds **by construction**: `reachableMeasure` is *defined* as $2^{\\operatorname{nmin}p}\\operatorname{tailSum}p\\,(\\operatorname{nmin}p)$, the right-hand side of the census law. The strictly geometric statement — that the $2^{\\operatorname{nmin}}$ translates in $S_1$ are pairwise disjoint with union exactly the sub-sum set — is **not formalised**; `Op56/Census.lean` states this as the remaining \"census counting\" gap, needing `nmin_minimal` for disjointness and the measure identity for a disjoint union of $2^{\\operatorname{nmin}}$ intervals of length $T_{\\operatorname{nmin}}$. The arithmetic is verified numerically to $3.9\\cdot10^{-62}$ for thirteen exponents by `rounds/rh42/reachable.py` §2 (local-only, outside this folder), and the identity is re-derived in `notes/OP-06-reachable-fraction.md` §1.\n\n### 3.12 The recorded guess for OP-5's slope — REFUTED\n\nThe register's earlier suggestion $n_{\\min}(p)\\approx p+O(1)$ is **false**: the slope is $1/\\log2=1.4426950408\\ldots$, and $n_{\\min}-p$ grows without bound. Measured by `op05_nmin.py`: $n_{\\min}/p=1.3000,1.4200,1.4400,1.4420,1.4424$ at $p=10,50,200,1000,5000$, with $n_{\\min}-p=3,21,88,442,2212$.\n\n## 4. Verification and evidence\n\n### 4.1 Scripts run for this edition\n\nAll Python checks were run on **2026-10-16** with Python 3.13.13 (`numpy` 2.5.0, `mpmath` 1.3.0). They write nothing but stdout, so they were run in place; the Lean build was run on a **copy** of the folder under a temporary directory so that no build artifacts were written into the published folder.\n\n| Command | Exit | Observed output (representative lines) |\n|---|---|---|\n| `python3 op05_nmin.py` | **0** | §1 refutes the slope guess: `p=5000 n_min=7212 n_min/p=1.4424` (1-based $n_{\\min}$; the 0-based Lean $\\operatorname{nmin}$ of §3.3 is $7211$); §2 `predicted c = 3(ln2)^2 - (25/12)ln2 = -0.0026975844119484539513`, `Richardson fit (last 4) c_fit = -0.002697584512195 diff = -1.002e-10`; §3 `n=1000 3.230e-09 / 0.00323 … n=1000000 3.233e-15 / 0.00323`; §4 `n=100 ratio=1.0119, n=1000 1.0012, n=10000 1.0001`; §5 `root of zeta(p) = 2 : 1.72864723899818362`, `P_1 (threshold, h(1,p)=0) : 1.72864723899818362`. |\n| `python3 op06_reachable_fraction.py` | **0** | §0 reproduces the `rh42` table (`p=2 … 12`); §1 `p=1000 … (L-p log p)/p = -0.6334875826` → `p=1000000 … -0.6334870794`, `the last column -> -(1 + ln ln 2) = -0.633487079418336`; §2 large-$p$ branch `1/p coefficient -> -0.540509640658` (smooth-index, historical); §3 `residual * p` oscillates `-0.503136, -0.517180, -0.534774, -0.481076, …, -0.480562` at $p\\le10^6$. |\n| `python3 op06_ceiling_coefficient.py` | **0** | table above, `worst |p*R - c(e)| over the table = 3.143e-07`, `the deviation falls by ~10x per decade of p`, non-constancy witness `p = 1e7 … p*R = -0.520616694704` vs `p = 1e9 … -0.483414796849`, `difference = 0.0372019`, **`VERDICT: CONFIRMED`**. |\n| `python3 op09_moduli.py` | **0** | §1 `p = 200 nmin = [287, …, 287] all equal` (also 1000, 5000); §2 `θ(p) − p/log 2 = 6.0` for every $p$ (see the observation below); §3 `spread … over all 60 cases: [-1.4950409, -0.51322271]`, **`VERDICT: CONFIRMED`**. |\n| `python3 verify-006/op05_nmin_ceiling.py` | **0** | `p=1000 nmin=1441 asym=1440.195041 gap=0.804959 p*gap=804.96 True … p=50000 72133 72132.252044 0.747956 37397.78 True`; `gap range [0.024796, 0.804959] (always inside (0,1))`; `p*gap is UNBOUNDED => |nmin p - (p/ln2 - 5/2)| = O(1), and the old O(1/p) is FALSE`; `Wider sweep … tested 76 values of p, mismatches: 0`. |\n| `python3 verify-006/op05_nmin_ceiling_false.py` | **0** | 451-digit counterexample; see §4.2. |\n| version-2 check [`chk.py`](https://solveathome.org/files/8a37d6d9886dc1bd9bb75da17624de514f97ea81202c997fe6c291a97a79b16b) (Python `decimal`, 50 digits; arguments: the four `Op56` Lean files) | **0** | output [`chk.out`](https://solveathome.org/files/e966abead26aa9e6750cfaf769452e4edea94df28281a2bfcfc93ce7c66dbd97), 18 `PASS` lines and `ALL PASS`: the three threshold theorems assume `hP` for all `n : ℕ`; `reachableMeasure` and `L` are defined as in §3.9; $(P_n-\\operatorname{thresholdAsym}(n))\\,n^2=-0.003211\\ldots-0.003232$ for $n=100\\ldots3200$; $\\operatorname{nmin}p=1441,2883,7211$ at $p=1000,2000,5000$; $c(e)$ ranges over $[-0.540509640657977,-0.480453013918201]$; over $2\\le p\\le2\\cdot10^6$ the proxy $p\\,(1-\\{p/\\log2-\\tfrac32\\})$ has minimum $0.076537$ at $p=418079$ (a proxy margin only, not an exact (CEIL) test; §3.5). |\n| version-3 check [`chk3.py`](https://solveathome.org/files/d7d079e0e571dc7fb8b0bcf449d9084434a18eb822b3029a870166535e3331d8) (Python `decimal`, 40 digits; argument: this manuscript) | **0** | output [`chk3.out`](https://solveathome.org/files/add4a73c31fc041b78f4a3cc86af6c077e9792c025bfb420606ed51784fd2c84), 14 `PASS` lines and `ALL PASS`: recomputed from $\\Phi$, $\\operatorname{nmin}p=1441,2883,7211$ equals $\\lceil p/\\log2-\\tfrac52\\rceil$ and $n_{\\min}(p)=\\operatorname{nmin}p+1=1442,2884,7212$ equals $\\lceil p/\\log2-\\tfrac32\\rceil$ at $p=1000,2000,5000$, while $\\lceil p/\\log2-\\tfrac52\\rceil$ differs from $n_{\\min}(p)$ there; text checks of the abstract's index convention and of the proxy wording. |\n| `./check.sh --all` (Lean 4 + Mathlib, on a temp copy) | **0** | 9/9 `[check] OK`; see §4.2. |\n\n### 4.2 The two decisive checks\n\n**The 451-digit ceiling counterexample.** `python3 verify-006/op05_nmin_ceiling_false.py` exits **0**. Its first section is the positive control: (CEIL) holds at $p=1000,5000,10000$ (`ok=True`). Its second section searches continued fractions of $\\beta=2/\\log2$ with the failure threshold $Q(M-Q\\beta)<2(-b)/\\log2$, printing at each hit the digit count of $Q$; the first candidate found has 451 digits (the first continued-fraction candidate, not necessarily the least failing $p$). Its third section re-verifies at 1150 dps, printing the last 20 digits of $\\lceil p/\\log2-\\tfrac52\\rceil$, $\\lceil y\\rceil$ and the computed $\\operatorname{nmin}p$, then\n$$\\Phi_p(\\lceil y\\rceil-1)-1<0,\\qquad \\Phi_p(\\lceil y\\rceil)-1<0,\\qquad \\Phi_p(\\lceil y\\rceil+1)-1>0,$$\nforcing $\\operatorname{nmin}p=\\lceil y\\rceil=\\lceil p/\\log2-\\tfrac52\\rceil+1$: **(CEIL) fails**. (The full 451-digit value is printed by the script and is not reproduced here; the note quotes its leading digits as `1831818673613185754746818686991356738383131544534391214519013360…1508975`.)\n\n**The Lean build.** `./check.sh --all` on a copy elaborates the nine modules `Op56/Defs.lean`, `Op56/Exact.lean`, `Op56/Census.lean`, `Op56/PhiAsymptotic.lean`, `Op56/PhiThird.lean`, `Op56/PhiFourth.lean`, `Op56/Asymptotic.lean`, `Op56/FloorAsymptotic.lean`, `Op56.lean` and exits **0** with 9/9 `[check] OK`. `HANDOFF-006.md` and `LEAN-README.md` record the development at **0 `sorry`**, **0 `axiom`**, **0 `native_decide`**, with `#print axioms` on the headline theorems equal to `[propext, Classical.choice, Quot.sound]`; `TRUTHS.md` records `ΦThird`/`ΦFourth` taking 78 s and 121 s and the rest under 35 s. The toolchain is Lean 4 `v4.35.0-rc2` with Mathlib; there is no `lake` project file, `check.sh` reconstructs `LEAN_PATH` from `lake env` inside the Mathlib checkout.\n\n**One stale count kept visible.** The root module `Op56.lean`'s docstring still says \"`./check.sh --all` is **8/8 green**\", while `check.sh --all` elaborates nine modules and `README.md`/`LEAN-README.md` say **9/9**; `HANDOFF-006.md` also says 9/9. The 8/8 line is stale text from before `FloorAsymptotic.lean`/`PhiFourth.lean` were added.\n\n**Observation on `op09_moduli.py` §2.** The printed `θ(p) − p/log 2 = 6.0` at every $p$ is exactly the upper edge of the script's bisection bracket. As coded, the bisection keeps `lo = mid` when `F1(mid,p) >= 1`, which is the rule for a function *decreasing* in `n`; but $F_1(n)=\\sum_j(1+j/n)^{-p}$ is *increasing* in $n$, so that section converges to `hi = p/log 2 + 6` rather than to the root. The substantive checks (§1 exact $q$-independence and §3's bounded spread of $\\operatorname{nmin}+1+r/q-p/\\log2$) do not depend on it and support the stated law; the derived relation with the correct direction is criterion$(N;q,r)\\iff N+1+r/q\\ge\\theta(p)$. This is recorded as a defect in that one printed section, not in the result.\n\n### 4.3 Evidence recorded in the folder\n\n* `logs/op06_ceiling_coefficient.log` records the same table as the live run (`worst 3.143e-07`, `VERDICT: CONFIRMED`); `logs/op09_moduli.log` records the 60-case run (`VERDICT: CONFIRMED`).\n* `HANDOFF-006.md` §5–§6 carries the theorem statements, the measured tables, the corrections and the `#print axioms` footprint; §4 explains the two `namespace Op56` blocks in `PhiThird.lean` (40 declarations reachable as `Op56.Op56.*`).\n* `notes/OP-05-nmin-asymptotic.md` §3–§5 carries the threshold table, the Richardson fit to $1\\cdot10^{-10}$, the $0.00323$ remainder and the $P_1=p^\\ast$ boundary check; §4 carries the exceptional-set width of the closed form.\n* `notes/OP-06-reachable-fraction.md` §3.1 reproduces the `rh42` §4 table and notes that the record's $p=1.8$ and $p=2.2$ rows appear offset by one (harmless for the asymptotics); §3.3 keeps the superseded smooth-index table beside the corrected one.\n* The `006`-side copies in `verify-006/` are byte-identical to the top-level scripts except for re-pointed prose links (`op05_nmin.py`) and the $1/p$-correction docstring (`op06_reachable_fraction.py`, whose `verify-006` copy still states the superseded constant in its header).\n\n## 5. What is not claimed\n\n* **No twin primes, no parity problem, no Riemann hypothesis.** Nothing here touches them. The finite checks are finite checks.\n* **The exact ceiling law is not a theorem and never was.** (CEIL) is refuted by a 451-digit counterexample (the first continued-fraction candidate; the least failing $p$ is not determined); the disjunction $\\operatorname{nmin}p\\in\\{\\lceil A\\rceil,\\lceil A\\rceil+1\\}$ is the sharpest *true* uniform statement and is **unproved**.\n* **The $O(1/p)$ error term is false**, as is the constant $1/p$ coefficient and the $1/\\log q$ reading of other moduli. All three are retained beside their corrections; the main theorems ($O(1)$ error, closed-form $c(e)$ coefficient, slope $1/\\log2$) are unaffected.\n* **The census identity is formalised by construction.** The geometric \"census counting\" statement (disjoint translates, union exactly the sub-sum set) is **not** formalised; the arithmetic check is numerical.\n* **The threshold-form fourth order (`SFourth`) is not landed** — new analytic content.\n* **The threshold theorems of §3.2 are vacuous as stated**: their hypothesis is required at $n=0$, where it cannot hold. Restating them over $n\\ge1$ (or eventually in $n$), re-checking the proofs and re-recording `#print axioms` with a build log is open; until then the threshold expansion is DERIVED + MEASURED. The folder's `TRUTHS.md`, `README.md` and `LEAN-README.md` still list them as proved; they are reproduced unmodified.\n* **`op6_reachable_fraction` is about the census-defined measure**, and its $1+o(1)$ form rests on the derived expansion of §3.10; the docstring of `op6_reachable_fraction` and `LEAN-README.md` still state the $1+o(1)$ form.\n* **`op5_nmin_asymptotic`'s constant is $11$**, not claimed sharp; the theorem bounds the residual, and `LAsym`'s linear coefficient is *given* rather than re-derived in OP-6.\n* **The meta-theorem's `log 2` instances are conditional** on `Irrational (Real.log 2)` (Lindemann–Weierstrass, absent from Mathlib `v4.35.0-rc2`); the general meta-theorem is unconditional.\n* **`tailSum_integral_lower` is a negative result** and is used by nothing; its original hypothesis $N+1\\le M$ was false and is corrected to $N+2\\le M$.\n* **`op09_moduli.py`'s §2 printed threshold values are an artefact** of the bisection direction as coded (see §4.2); only the slope of `O9` is claimed, and no Lean generalisation is attempted.\n* **`op06_reachable_fraction.py` §4 still prints the superseded constant** in its closing \"closed form\" text; the corrected coefficient lives in its own docstring, in `op06_ceiling_coefficient.py` and in `notes/OP-06-reachable-fraction.md` §2.4. The stale line is kept visible rather than silently edited.\n* **Two recorded numeric discrepancies are not resolved here**: the OP-06 correction banner cites $3.1\\cdot10^{-13}$ at $p=10^{13}$ where the table, `README.md` and `TRUTHS.md` give $3.5\\cdot10^{-14}$ (the table is the value reproduced by the live run); and `README.md`'s `O9` row says \"60 cases, $q\\le11$\" while the note says 60 cases at 60 dps — these agree.\n* **Attribution.** The folder states the programme (math.solveathome.org), the rounds (`rh42`, `open/`, `006/`) and the Lean toolchain, but no individual authors or dates of the mathematics, and none is asserted here. The manuscript itself has recorded provenance — return #4169 by the account victor-geere with the AI model deepseek-flash, and this version by the account Benjaminsen with claude-opus-5-5 — see **Contributions and AI disclosure** at the top.\n\n## 6. Value and significance\n\nThe item closes a registered chain — `rh42` census $\\to$ OP-5 threshold/index $\\to$ OP-6 decay — with machine-checked proofs of the index asymptotic and of the reachable-fraction asymptotic (for the census-defined measure), a derived and measured — not yet machine-checked — threshold expansion, and an unconditional meta-theorem that explains a structural impossibility rather than merely observing it: an integer index cannot track an irrational affine function to within $O(1/p)$, so the corrected $O(1)$ error of OP-5 is the end of the line, not a gap to be sharpened. It is also a case study in record hygiene: the round kept every false claim it corrected — the $O(1/p)$ error, the exact ceiling law (with its 451-digit falsifier and the 76-value sweep that missed it), the constant $1/p$ coefficient, the $1/\\log q$ modulus guess, the stale \"does not compile\" note, and the stale 8/8 build count — next to the corrected statement and the evidence that refuted it. The quantitative pay-off is that the reachable fraction of the budget is now known to die like $p^{-p}e^{(1+\\log\\log2)p}$, with $c=1$ in the registered $c\\,p\\log p$ form, and its $1/p$ behaviour is pinned to a closed-form function of the ceiling error. Finally, the folder is explicit about its own remaining holes: the ceiling disjunction, the census counting, and the threshold-form fourth order — and, since version 2, the vacuous threshold statements.\n\n## Sources\n\nAll paths are relative to this folder. SHA-256 values are of the files as read for this edition.\n\n| Source | Role | Locator | SHA-256 |\n|---|---|---|---|\n| [`README.md`](README.md) | folder guide, contents, proved/refuted/open summary | whole file | `b82033ab2526e013d53ff52e4f9f8e2462f2c3b44c8cd0370064cfb704c00d87` |\n| [`TRUTHS.md`](TRUTHS.md) | the §9 ledger: every theorem with status and Lean proof locator | table, lines 12–29 | `58076047aab5a4662dc6b4f1482e71f455f8f504e8b910595ee0fa035db487c3` |\n| [`HANDOFF-006.md`](HANDOFF-006.md) | cleaned authoritative state: theorem statements, proof routes, corrections, gotchas | §§1–12 | `17e4def2fc0dd1ab87d6dfba43471a9e3afae3db75ef85f472cfde0ee5c66493` |\n| [`LEAN-README.md`](LEAN-README.md) | the Lean development's own guide | whole file | `41bfb83ba1bde01c874d530e13fad17a22fff64e116d6813010ff9e7b0112650` |\n| [`Op56/Asymptotic.lean`](Op56/Asymptotic.lean) | the headline theorems, `c5`, `c6`, `leadingCoeff_forced` | 338 lines | `1d343279d915579eefa5631384eb656dd799ec382d2b613cd2bf98c559a6c54d` |\n| [`Op56/Defs.lean`](Op56/Defs.lean) | objects, indexing dictionary, asymptotics expressions | 78 lines | `1acc049eb53c53aa5aaeaf530588c7833532b2d026f382cb014089f783e872e3` |\n| [`Op56/FloorAsymptotic.lean`](Op56/FloorAsymptotic.lean) | `O11`: the floor/Diophantine meta-theorem and OP-5 instance | 227 lines | `86ba84730f378f60e48b243f1b30c32cd712e450a4a37e52e8e78192ca609675` |\n| [`Op56/Census.lean`](Op56/Census.lean) | census identity and ratio, with the recorded counting obstruction | 67 lines | `669a48eb8cf0775fb9d7b8ac22251f50f49042f5b999b138d1a65b42755f5e7a` |\n| [`Op56/Exact.lean`](Op56/Exact.lean) | exact layer, `exists_isComplete`, corrected integral test | 385 lines | `13ba7d83e6715bafc96ec56f61f95899e4aff86f1b21b322ff02f75f04d34a37` |\n| [`Op56/PhiAsymptotic.lean`](Op56/PhiAsymptotic.lean) | `Φ` first/second-order asymptotics | 2473 lines | `3d1771953cf9340fe237a235bbd08e359ab128aba11e156549ce9e2c1c5536a9` |\n| [`Op56/PhiThird.lean`](Op56/PhiThird.lean) | third-order layer, ceiling reduction, OP-6 estimate chain | lines 5178–5256 for the ceiling reduction | `f43107d2d01f177ded4b376c7f076a1d173944e18b7b7601cf57fd301aa962f7` |\n| [`Op56/PhiFourth.lean`](Op56/PhiFourth.lean) | `O10`: `Phi_fourth_order` and its auxiliary layer | `Phi_fourth_order` at line 1513 | `45b28aef87617f278919ef436ad719293ec6218e49c106abe0a7f2ee47663391` |\n| [`Op56.lean`](Op56.lean) | root module (its \"8/8\" count is stale; see §4.2) | whole file | `243d62c21e43019708eced67ca1ee4678b1b340e0cfcfc3cae1b5c5c9b607cdf` |\n| [`check.sh`](check.sh) | the build script: elaborates the nine modules against Mathlib | whole file | `11b481d126c607d7d437e4eb4ff7294707ce50dd053fa865ff65249d36a27f57` |\n| [`op05_nmin.py`](op05_nmin.py) | OP-5 ground truth: slope, threshold constant, remainder | 154 lines | `b32aae09e040bece103271cee7226cc83fd1202d97ee8480a34dcf2874290651` |\n| [`op06_reachable_fraction.py`](op06_reachable_fraction.py) | OP-6 census values, leading coefficients | 169 lines | `1020f1fec1d7f5dd770d5e60dc0aabfd6d06458ab320b1d349ac56808ed7d84f` |\n| [`op06_ceiling_coefficient.py`](op06_ceiling_coefficient.py) | `O4`: the closed-form $1/p$ coefficient and non-constancy | 118 lines | `adf1a8547c39e386ac39fad1817123a618d7c0b1f279ba1aaea73d77ef5c1131` |\n| [`op09_moduli.py`](op09_moduli.py) | `O9`: other-moduli falsification | 142 lines | `4f587043f5e50521c9b23fae5aaf98bd357036c8d03460f4481f2e5349baa59d` |\n| [`verify-006/op05_nmin_ceiling.py`](verify-006/op05_nmin_ceiling.py) | falsifies $O(1/p)$; 76-value sweep of (CEIL) | 110 lines | `638f0a0b3e1a9dff77aeea1505087f860cb3d0d7519657cdfe72c583bc6ad137` |\n| [`verify-006/op05_nmin_ceiling_false.py`](verify-006/op05_nmin_ceiling_false.py) | the 451-digit counterexample to (CEIL), 1150 dps | 174 lines | `4322f0d8973632a44dd921edbd07a2c949d3ba04c04f8fc88d1e7a1e9f94cc25` |\n| [`verify-006/op05_nmin.py`](verify-006/op05_nmin.py) | `006`-side copy of the OP-5 ground truth | 154 lines | `5abb417e55dfb9c84c84973bb75d5a10d7f9d5a7348cdf7a296dd3a4658f67b5` |\n| [`verify-006/op06_reachable_fraction.py`](verify-006/op06_reachable_fraction.py) | `006`-side copy, header still at the superseded constant | 153 lines | `f287307699b2990b729f159a2d51b7174a17d360fbd338d829033d7e1afdb412` |\n| [`logs/op06_ceiling_coefficient.log`](logs/op06_ceiling_coefficient.log) | recorded `O4` run | whole file | `b80c93552c8f66bd3a8c65c927a540b0edbdb2bb410413566cc53ea13de2a3cb` |\n| [`logs/op09_moduli.log`](logs/op09_moduli.log) | recorded `O9` run | whole file | `b6849b62859d4ae1cc29581f2eb3fa3cd28ffd32deba0bcb76fb7f4763808155` |\n| [`notes/OP-05-nmin-asymptotic.md`](notes/OP-05-nmin-asymptotic.md) | OP-5 write-up with both correction banners | §§1–6 | `67056d53cc9711bd6c81c6f0a329c9c2c21b9586356854f8bd2702f05347c9ef` |\n| [`notes/OP-06-reachable-fraction.md`](notes/OP-06-reachable-fraction.md) | OP-6 write-up, §2.4 the closed-form coefficient | §§1–4 | `166f72827b964d94e38d1fba5a9c61c6663b14100bc5e761dc92cab8a48e149a` |\n| [`notes/OP-09-other-moduli.md`](notes/OP-09-other-moduli.md) | the `O9` falsification write-up | whole file | `db1e675218a8850d226bea73b45ac72757b622aa497c396644ef56b2c3009114` |\n| [`notes/07-open-problems.md`](notes/07-open-problems.md) | the register: OP-5/OP-6 rows, difficulty, sources | rows at lines 112–113, 217–238 | local-only context |\n| `rounds/rh42/reachable.py` §2 | the $3.9\\cdot10^{-62}$ census arithmetic check | cited in `notes/OP-06-reachable-fraction.md` §1 | local-only, not in this folder |\n| `open/HANDOFF.md` | the full development log (archaeology) | cited in `HANDOFF-006.md` §12 | local-only, not in this folder |\n| `research/truths.md` §9 | upstream ledger | reproduced as `TRUTHS.md` | local-only, not in this folder |\n","source_checks":{"claims":25,"claims_mapped":1,"claims_unmapped":24,"has_map":false,"references":0,"references_resolved":0,"references_found_by_search":0,"references_unresolved":0,"references_mismatch":0,"references_skipped":0,"references_pending":0,"url":"/projects/twin-primes/papers/op5-op6-resolved-open-problems/checks"}}