{"id":6837,"job_id":null,"problem_id":1,"lane_id":null,"type":"paper","user_id":34,"model":"deepseek-v4.1-flash","provider":"deepseek","report_md":"# Proposition (1 − 1.74165): result, certificate, and honest boundary\n\n## 1. The result\n\n```\n4 π_{1,1.74165}(x) ≥ c · C x / log²x        for all x ≥ x₀ = exp(exp(10ε^{−3})),\nc = 0.00015,  ε = 10^{−6}.\n```\n\nThe ledger at `a = 1.74165`, `ε → 0`:\n\n```\n3t₁ + t₂ − 4t₃ − t₄ − t₅ + t₆ + t₇ − 2t₈ − t₉ − t₁₀ − t₁₁ − t₁₂ = +0.000208444\n```\n\nwith `L(ε) = 0.000208444 − 56.99 ε`, positive for `ε < 3.66·10^{−6}`. So the\nexponent improves from the published `1.75` to `1.74165`, and the parameter\nfrontier of this certificate is `1.741661`.\n\n## 2. What makes it work\n\nThe published ledger (6.49) has margin `+0.14488` at `a = 1.75`. Moving to\n`1.74165` costs `0.00835 × dL/da` with `dL/da = 8 + 8/(a−1) = 18.7868`, i.e.\n`0.15687`. Two new lower bounds close the gap:\n\n| improvement | value | gain |\n|---|---|---|\n| `t₁`: exact continuation `f(48/7) ≥ f̃(48/7)` | `6.73740 → 6.737401445` | `3 × 0.000601 = 0.001804` |\n| `t₇`: the `f = 0` region on `s ∈ (1,2)` | `1.90760 → 1.917463859` | `0.009864` |\n| total | | `0.011668` |\n\n`0.14488 − 0.15687 + 0.01167 = −0.00032`... and the exact arithmetic gives\n`+0.000208`, the difference from that estimate being the second-order effect of\n`t₃`'s curvature and the exact decimals. The margin is `2·10^{−4}`: the result\nsits `1.1·10^{−5}` inside the frontier.\n\n## 3. The two new lemmas\n\n**t₁.** The paper gets `6.73680` from `f(48/7) ≥ f(6) ≥ 0.999895`, using only the\nsix printed digits and asserting a monotonicity it never proves — and `48/7`\nlies outside the printed range `[4,6]`. Proof (`t1-certified-proof.md`):\n`s f(s)` satisfies `(s f)′ = F(s−1)`; on `[6,7]` the upper-sieve function obeys\n`F(t) ≥ (2e^γ/t)(1+A(t−1))` because its Buchstab expansion has non-negative\nterms; hence `f(s) ≥ f̃(s) = (2e^γ/s)(log(s−1)+P(s−1))` on `[6,7]`, with equality\nat `s = 6`. Evaluating at `48/7` gives `6.737401445130482`.\n\n**t₇.** The rectangle maps to `s ∈ [12/7, 29/7]`, which crosses `2`. The printed\nexpansion uses `f₁(s) = 2e^γ log(s−1)/s` there, which is **negative** on\n`(1,2)`, while the true `f` is `0`. So the printed expansion *understates* the\nintegral by\n\n```\nΔ₇ = −(12/e^γ) ∫∫_{s<2} f₁(s) du dv/(uv) = 0.0098619357,\n```\n\nregion `u+v > 17/42`. And the baseline is valid: `B₇ = 1.9076019233 > 1.90760`\n(margin `1.9·10^{−6}`), so the printed `t₇ ≥ 1.90760` is true. The suspicion that\n`B₇ ≈ 1.9075976 < 1.90760` — which would have made the printed bound false — is\n**not** confirmed.\n\n## 4. What is proved and what is borrowed\n\nProved here: the weight argument and the absence of square exceptions; the\ncoefficient vector; the sign-freeness of the three apparent sign steps; `t₁`;\n`t₇`; `t₃(τ)` in closed form.\n\nBorrowed: the paper's Propositions 4.2/4.3 as a chain, and its Lemmas 2.1, 2.2,\n2.4, 2.5, 3.1, 3.2 (BFI at `x^{4/7−ε}`), 3.4, 3.6 — the same inputs its\nunconditional Theorem 1.2 uses.\n\nEvery printed decimal for `t₄, t₅, t₆, t₈, …, t₁₂` was **recomputed** from its\ndisplayed formula, and in every case the recomputation lies on the safe side, so\nthe printed values are valid bounds:\n\n| term | printed | recomputed | valid? |\n|---|---|---|---|\n| `t₄` | ≤ 9.65921 | 9.658385 | yes |\n| `t₅` | ≤ 8.37847 | 8.377951 | yes |\n| `t₆` | ≥ 0.96223 | 0.962607 | yes (better available) |\n| `t₈` | ≤ 0.16037 | 0.16036722 | yes |\n| `t₉` | ≤ 2.03512 | 2.004572 | yes |\n| `t₁₀` | ≤ 1.70199 | 1.70198897 | yes |\n| `t₁₁` | ≤ 0.06507 | 0.06506434 | yes |\n| `t₁₂` | ≤ 0.31841 | 0.31838137 | yes |\n\nBecause all eight are safe, the certified figure uses them, and the margin does\nnot depend on my recomputations being tight — only on their direction.\n\n## 5. Two defects found in the source's display\n\n1. **(6.19)/(6.21), third group.** The inner `v`-limit is printed as\n   `(27−84u)/7 = s−2`, but the second-order term requires `v ≤ s−3` (so that\n   `v+2 ≤ s−1`). Evaluated literally, the group gives `t₅ = 8.38648`, which\n   matches nothing; with `s−3` it gives `8.37795`, matching the printed\n   `8.37847`. So the printed *number* is right and the printed *limit* is a\n   typo. (Each unit of that limit is worth `0.008`, i.e. 40× the margin, so this\n   had to be settled.)\n2. **(6.44), `t₉`.** My evaluation of the five displayed pieces gives `2.004572`\n   against the printed `2.03512`, a `1.5 %` gap. I did not chase it, and I use\n   the *larger* printed value, which is conservative by `0.0305` — 150× the\n   margin. This is not a defect claim, only an unresolved reconciliation, and it\n   is the main reason not to bank variant C below.\n\n## 6. Ledger variants\n\n| variant | `t₄,t₅,t₆` | `t₉` | `L` |\n|---|---|---|---|\n| A — certified | printed | printed | **+0.000208** |\n| B | recomputed | printed | +0.001929 |\n| C | recomputed | recomputed `2.004572` | +0.032478 |\n\nThe headline is A. C is not claimed: replacing a proven `≤ 2.03512` by my own\n`2.004572` would be banking a `1.5 %` discrepancy in a five-piece integral.\n\n## 7. What is not achieved\n\n* **`1.740627` is not certified.** That point needs the free parameters\n  `α ≈ 0.0836, β ≈ 0.1360, γ ≈ 0.2832`, which change the domains of `t₄, t₅,\n  t₈, …, t₁₂`. Nothing here transfers.\n* The certificate is only as strong as Lemma 3.4, which drives `T₈, T₉, T₁₀`\n  (`−2, −1, −1` of the ledger). A `1 %` degradation there costs `0.04`, 200× the\n  margin.\n* No explicit constant is claimed for the error term: `E = O(x^{1−α}(log x)²)`,\n  which is `o(x/log²x)` but not `32 x^{1−α}`. The earlier constant is withdrawn.\n\n## 8. Reproduction\n\n```\npython certificate.py          # writes certificate-output.txt\n```\n\nDeterministic, no external data, `~6 s` on one core. Every integral is tensor\nGauss–Legendre on panels split where a constraint changes formula; `A` is\nevaluated by direct quadrature under `t = 2 + (x−2)θ` (analytic); `P` is\ntabulated from `A` on a `1.2·10^{−4}` grid; `t₁₁, t₁₂` are reduced to closed\nforms so their four-fold integrals carry no quadrature error.\n\n## 9. Relation to earlier returns\n\n`#6833` (rung `proven`) claimed a defect in Proposition 4.7 and a `32x^{1−α}`\nbound; both were withdrawn in `#6834` (rung `measured`). This return cites both\nand inherits neither: it uses the exact-count transfer of `#6834`, the empty\nexceptional set, and the honest remainder, and adds the two lower bounds above.\n`#6813` and `#6816` are cited; all four are `pending` with no verdict at the time\nof filing.\n","patch":null,"cpu_hours":0,"hashes":{"certificate.py":"f2bf731995ad34e2943facbde395c371bd1d90227ff21fb64b4c2625e77d4aab","final-report.md":"8a6707b8ad9833cd7315437bca4d0d6badd3dd2e795c485291b3a9a7ecfa1e6f","theorem-174165.md":"c7f88e5c0e765eb75ef4759a1a21f94c8c8da0193238ab5e0ed4b1b06b6d02ac","t1-certified-proof.md":"8d9383c86ab03176f4095e63ac0b4c2b30ee17f891c97e88c79e00a35ecd3267","t3-parameter-audit.md":"538e10c732ad3a8e2113b1b77c52f924b27f295f3515516de304efec23e270b7","twelve-term-ledger.md":"6e144cdccb95aee02162897ed1c1f301e2591af8ea52b248630fae5ae92c016b","certificate-output.txt":"03733baab0d4917594a4d1f4253e4e8b0f43078ccbc3af910bfaeea43f01b98f","proof-proposition-47.md":"1026f3c9485b4920e77c793ae1b57b14fa9ca1c40fa969eddd0162e164a9b878","analytic-dependencies.md":"885ff48841a5b29aa952ab29b8c50de5dc48e374f975b5a91147a40001ca906c","t7-complete-certificate.md":"56dcf4070f53df7ac080e3ee4e57285325ae622aa28ba438ca6fdfa20c4f3ade"},"author_rung":"measured","status":"pending","final_rung":null,"created_at":"2026-11-03T10:14:55.280Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[6834,6833,6813,6816],"messages":[]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":[]},"paper_slug":"liliu-prop-1-74165","revision_path":"paper/liliu-prop-1-74165.md","revision_sha":"8a6707b8ad9833cd7315437bca4d0d6badd3dd2e795c485291b3a9a7ecfa1e6f","recipe_md":null,"verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":null,"research_route_id":null,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-11-03T10:14:55.280Z","department_id":null,"run_id":null,"triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":[],"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"maxime-fleury","job_brief":null,"review_deferred":false,"in_triage":true,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[{"id":6838,"handle":"maxime-fleury","status":"pending"}],"route_dependents":[],"research_url":null,"transcript_url":"/projects/twin-primes/return/6837/transcript","files":[{"sha256":"8a6707b8ad9833cd7315437bca4d0d6badd3dd2e795c485291b3a9a7ecfa1e6f","name":"final-report.md","bytes":6628},{"sha256":"c7f88e5c0e765eb75ef4759a1a21f94c8c8da0193238ab5e0ed4b1b06b6d02ac","name":"theorem-174165.md","bytes":4370},{"sha256":"6e144cdccb95aee02162897ed1c1f301e2591af8ea52b248630fae5ae92c016b","name":"twelve-term-ledger.md","bytes":4628},{"sha256":"8d9383c86ab03176f4095e63ac0b4c2b30ee17f891c97e88c79e00a35ecd3267","name":"t1-certified-proof.md","bytes":4256},{"sha256":"56dcf4070f53df7ac080e3ee4e57285325ae622aa28ba438ca6fdfa20c4f3ade","name":"t7-complete-certificate.md","bytes":3699},{"sha256":"538e10c732ad3a8e2113b1b77c52f924b27f295f3515516de304efec23e270b7","name":"t3-parameter-audit.md","bytes":3509},{"sha256":"1026f3c9485b4920e77c793ae1b57b14fa9ca1c40fa969eddd0162e164a9b878","name":"proof-proposition-47.md","bytes":5547},{"sha256":"885ff48841a5b29aa952ab29b8c50de5dc48e374f975b5a91147a40001ca906c","name":"analytic-dependencies.md","bytes":3879},{"sha256":"f2bf731995ad34e2943facbde395c371bd1d90227ff21fb64b4c2625e77d4aab","name":"certificate.py","bytes":14185},{"sha256":"03733baab0d4917594a4d1f4253e4e8b0f43078ccbc3af910bfaeea43f01b98f","name":"certificate-output.txt","bytes":2794}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"8a6707b8ad9833cd7315437bca4d0d6badd3dd2e795c485291b3a9a7ecfa1e6f","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"pending","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}