{"id":2140,"job_id":null,"problem_id":1,"lane_id":null,"type":"audit","user_id":1,"model":"gpt-6.1-sol","provider":"openai","report_md":"Correct the quantifier overclaim in Q-hsub-reductions at its owning note. All prime-base power pairs suffice for limit existence and the prime infimum by the supplied log-density/liminf proof. The explicit generic monotone n=6 witness separates the original all-integer formula. Preserve all-base Reduction 1, finite readings and PARTIAL; no true-G2 cap is proved. See report.md and audit-manifest.json for proof, exact bases/candidates and independent check. QUESTIONS is generated companion only; refetch/rebase and regenerate without replacing pending corrections.","patch":"--- a/research/history/staging/attack-hsub-01.md\n+++ b/research/history/staging/attack-hsub-01.md\n@@ -5,7 +5,7 @@\n status: PARTIAL\n todo: 1d\n question: Can (H-sub) be proven or refuted, and what does the fold machinery reach?\n-verdict: Neither, but the statement is smaller: three reductions of the hypothesis are proven, the lemma consuming only power pairs so that it weakens to (H-sub-pow) with the conclusion unchanged, the fold machinery's inability to reach any of them is made exact, and the hunt over all 111 reachable pairs found no drifting family and no counterexample.\n+verdict: Neither H-sub nor a true-G2 uniform power-pair cap is proved or refuted. All-integer-base power pairs preserve the full Fekete infimum formula; a log-dense subset of bases, in particular all primes, already suffices for limit existence and its restricted-base infimum. The all-integer formula and witness equivalence do not follow from prime-only pairs for generic monotone f. The fold-budget obstruction and the attributed finite 111-pair no-counterexample reading remain at their stated scope.\n -->\n \n *2026-08-20. Producer: `research/attack-hsub-01.js` (0.1 s,\n@@ -41,9 +41,11 @@\n >    `[1.0761, 1.3946)` (0.3185 nats) to **`[1.0033, 1.3946)` (0.3913 nats,\n >    trusted)** and `[0.9694, 1.3555)` (0.3861, custody-only). **[PROVEN /\n >    VERIFIED]**\n-> 2. **One chain carries the TPC face; no chain carries existence.** A single\n->    base `b₀` with chain defect `K < S(b₀)` forces `limsup < 2`; limit\n->    existence needs chains at inf-realizing bases. And the chains that\n+> 2. **One chain carries the TPC face; prime-base chains suffice for existence.** A single\n+>    base `b₀` with chain defect `K < S(b₀)` forces `limsup < 2`. For\n+>    existence alone, all prime bases suffice, with the infimum restricted\n+>    to primes. The full all-integer formula is not guaranteed by prime-only\n+>    pairs; the original all-integer theorem supplies it. And the chains that\n >    decide the trap (bases 16 and 66) have **zero reachable pairs** — the\n >    decisive family is dataless. **[PROVEN / VERIFIED]**\n > 3. **The doubling slice is trap-free and prize-bearing.** `Ĝ(2s) ≤ C₂·Ĝ(s)`\n@@ -107,11 +109,40 @@\n   two-sidedly pinned steps `a·n_j ≤ n_{j+1} ≤ b·n_j` (`a > 1`) and\n   `f(n_{j+1}) ≤ f(n_j) + f(b) + K` gives `limsup ≤ (f(b)+K)/ln a`. Steps\n   pinned only from above lose the denominator and give nothing. **[PROVEN]**\n-- **Existence face.** No single chain, and no base subset `B`, gives limit\n-  existence: `limsup ≤ inf_{b∈B}(f(b)+K)/ln b` but `liminf ≥ L` takes the\n-  inf over ALL `n`, and the two close only when `B` realizes the inf —\n-  unknowable in advance, so the clean sufficient family is all-bases power\n-  pairs (Reduction 1) and nothing smaller. **[PROVEN]**\n+- **Existence face (quantifier correction, 2026-10-02).** A single base\n+  gives only the displayed limsup bound. A proper subset can nevertheless\n+  suffice for existence. Let `f : {2,3,…} → [0,∞)` be nondecreasing, and\n+  let `B` be a nonempty set of integer bases such\n+  that for every sufficiently large integer `n` one can choose `b(n) ∈ B`,\n+  `b(n) ≤ n`, with `ln b(n)/ln n → 1`. Assume one `K ≥ 0` satisfies the\n+  power-pair inequality for every `b ∈ B` and `k ≥ 1`. Then\n+  `β = lim f(n)/ln n = L_B := inf_{b∈B}(f(b)+K)/ln b`. **[PROVEN, conditional]**\n+\n+  Proof: the same fixed-base iteration and monotonic bridge give\n+  `limsup f(n)/ln n ≤ L_B < ∞` and hence `f(n) = O(ln n)`. Choose\n+  `n_j → ∞` realizing `ℓ := liminf f(n)/ln n` and put `b_j = b(n_j)`.\n+  Monotonicity gives\n+  `L_B ≤ (f(b_j)+K)/ln b_j ≤ (f(n_j)+K)/ln b_j → ℓ`,\n+  because `b_j → ∞`, the log ratio tends to 1 and `f(n_j)/ln n_j` is bounded.\n+  Thus `limsup ≤ L_B ≤ liminf`, proving the assertion.\n+\n+  In particular all primes form such a set: Bertrand's theorem supplies\n+  a prime `n/2 < p ≤ n` for every sufficiently large integer `n`, so\n+  `ln p/ln n → 1`. Prime-base power pairs therefore suffice for existence\n+  and `β = inf_p (f(p)+K)/ln p`, with\n+  `β < 2 ⇔ S(p) > K` at some **prime**. No PNT input is needed.\n+\n+  This does **not** retain the all-integer infimum or all-integer witness\n+  equivalence for generic monotone `f`. Take `f(n) = 2 ln n` at every\n+  integer `n ≥ 2` except `f(6) = 2 ln 5`, and `K = 0`. It is nonnegative\n+  and nondecreasing; no prime power equals 6, so every prime-base\n+  power-pair inequality holds with equality. Its limit and prime infimum\n+  are 2, while the all-integer infimum is at most `2 ln 5/ln 6 < 2` and\n+  `S(6) = 2 ln(6/5) > 0`. This is a counterexample to the generic formula\n+  transfer, **not** a true-G2 counterexample. The full all-integer\n+  hypothesis at `K = 0` does not hold for this witness. Reduction 1's\n+  unchanged full conclusion remains valid.\n+  **[PROVEN, explicit separation witness]**\n - **The decisive chains are dataless.** No base `b ≥ 10` has a single\n   reachable pair (`b² > 82`), so the chains at the threshold bases 16 and 66\n   — the ones whose `K < S(b₀)` would be TPC — are constrained by no\n@@ -257,10 +288,13 @@\n   the diagonal is neither seen nor excluded; the -01 blind spot stands.\n - **de Bruijn–Erdős Theorem 22 remains unopened**, consistent with the\n   bounded reading; nothing here cites its content.\n-- **Whether the reductions compose** (e.g. power pairs at prime bases only,\n-  giving the prime-base threshold `max_q S(q) = 1.2946` trusted) was\n-  computed in exploration but not carried into the producer; the all-bases\n-  form of Reduction 1 is the operative statement.\n+- **Prime-base composition is now resolved for existence**, by the\n+  conditional log-dense-base argument in §2; the original exploration's\n+  prime-base threshold `max_q S(q) = 1.2946` remains an attributed finite\n+  reading, not a newly reproduced value. Prime-only pairs yield the prime\n+  infimum and prime-witness equivalence, not the unchanged full formula.\n+  All-integer-base Reduction 1 remains the operative statement whenever\n+  that full conclusion or a composite witness is used.\n \n ## 8. Sources and reproduction\n \n@@ -277,3 +311,12 @@\n \n Reproduce with `node research/qc/embed.js --check research/attack-hsub-01.js`;\n the fingerprint matches as of 2026-08-20.\n+\n+2026-10-02 quantifier-audit sources: P. Erdős, *Beweis eines Satzes von\n+Tschebyschef*, Acta Litt. Sci. Szeged 5 (1932), pp. 194–198, opening\n+statement p. 194, https://users.renyi.hu/~p_erdos/1932-01.pdf (Bertrand's\n+theorem); Z. Füredi and I. Z. Ruzsa, *Nearly subadditive sequences*,\n+arXiv:1810.11723v1 (2018), §§2–3, Theorems 1–2 and equations (10)–(11),\n+https://arxiv.org/html/1810.11723v1 (a nearby additive restricted-pair\n+result, not an arithmetic G2 ratio bound). The §2 argument and separation\n+witness are given here; no numerical producer or published census was rerun.\n--- a/research/QUESTIONS.md\n+++ b/research/QUESTIONS.md\n@@ -205,7 +205,7 @@\n | 1d | `Q-delta-reader-0830` Can any instrument read the sign of the log-power correction delta in G2 ~ c n^beta (ln n)^delta at reach 79, passing the one-class control first? | ANSWERED | No. Six readers were pre-registered against stepped synthetic laws and the one-class control; the four power-chain readers (the diagonal meter among them) are killed by the P(n) stepping alone, the joint fit is calibrated but reads the control's finite-reach delta NEGATIVE (-0.38 +- 0.14 at 64 terms) where its conjectured asymptotic delta is +2, and the one reader that passes does so by importing the exponent, its sign being the sign of (1.777 - beta_hat). delta's sign for G2 is unreadable at reach 79 by any instrument tried, and the control shows a finite-reach reading would not carry the asymptotic sign anyway; item 1d's all-bases form stays unattackable. | [measure-0830-delta-reader.md](history/staging/measure-0830-delta-reader.md) |\n | 1d | `Q-fekete-1d-defect47` Does the bounded-defect Fekete route survive a probe at 47#? | PARTIAL | The defect at 47# is ordinary and the 47# enumeration cannot move item 1d's TPC threshold whatever value it returns; the bounded-defect Fekete lemma is stated exactly and proved with every hypothesis except the candidate itself discharged, so the route reduces to one named inequality and is neither closed nor open beyond that. | [fekete-1d.md](history/staging/fekete-1d.md) |\n | 1d | `Q-g2-falls-decision-rule` Does G2(x#)/x^2 fall, and what pre-registered decision rule would settle it? | PARTIAL | The instrument is calibrated and sharp, resolving the one-class control at 11.6 sigma on the same nine points where it returns 0.9 sigma on G2, and the honest band on the slope is +/-0.117 at nine terms, so the rule is registered; but the power analysis puts separation at x = 53 only if the falling law is x ln^2 x and at x = 151 if it is x ln^3 x, so phase 1's extra terms settle nothing and no reachable exact ladder does either. | [phase1-T3prep-decision-rule.md](history/staging/phase1-T3prep-decision-rule.md) |\n-| 1d | `Q-hsub-reductions` Can (H-sub) be proven or refuted, and what does the fold machinery reach? | PARTIAL | Neither, but the statement is smaller: three reductions of the hypothesis are proven, the lemma consuming only power pairs so that it weakens to (H-sub-pow) with the conclusion unchanged, the fold machinery's inability to reach any of them is made exact, and the hunt over all 111 reachable pairs found no drifting family and no counterexample. | [attack-hsub-01.md](history/staging/attack-hsub-01.md) |\n+| 1d | `Q-hsub-reductions` Can (H-sub) be proven or refuted, and what does the fold machinery reach? | PARTIAL | Neither H-sub nor a true-G2 uniform power-pair cap is proved or refuted. All-integer-base power pairs preserve the full Fekete infimum formula; a log-dense subset of bases, in particular all primes, already suffices for limit existence and its restricted-base infimum. The all-integer formula and witness equivalence do not follow from prime-only pairs for generic monotone f. The fold-budget obstruction and the attributed finite 111-pair no-counterexample reading remain at their stated scope. | [attack-hsub-01.md](history/staging/attack-hsub-01.md) |\n | 1d | `Q-hsubpow-K` Can (H-sub-pow) be proven with an explicit K in the legal zone? | CLOSED | NO by three mechanisms: the CRT lift (K* >= pi(y') - pi(y) diverges), anchored caps (diverge at every base), Iwaniec at two classes (it IS beta2-note); TODO 1d's legal zone is mis-stated, the trusted zone is [1.3946, 11.3568). | [hsubpow-explicit-K.md](history/staging/hsubpow-explicit-K.md) |\n | 1d | `Q-hsubpow-K-0829n` Can (H-sub-pow) be proven with an explicit K inside the trusted legal zone [1.3946, 11.3568) by a mechanism the 2026-08-28 pass did not close? | OPEN | No K is proven at any base; the single open inequality is the uniform-in-k ratio cap G(b^(k+1))/G(b^k) <= e^K G(b), which is a proof gap at a fixed base and a possible truth gap across bases, since for any law G ~ c n^beta (ln n)^delta the all-bases hypothesis holds with finite K if and only if delta >= 0. | [attack-0829n-hsubpow-K.md](history/staging/attack-0829n-hsubpow-K.md) |\n | 1d | `Q-import-interp` Does the Bayati-Gamarnik-Tetali interpolation method reach the G2 Fekete object? | ANSWERED | No: BGT closes on hypothesis H1, since the constraint count never splits (pi(st) - pi(s) - pi(t) is zero at no pair with st >= 25, minimum 2, maximum 12, VERIFIED on 104 pairs), and the one coordinate that does split has limit +infinity; the row lands as WALL-ADDRESS plus the identity that the submultiplicativity defect is the Overshoot slack. | [import-interp.md](history/staging/import-interp.md) |\n@@ -492,7 +492,7 @@\n | `Q-history-dial` | ANSWERED | Does revealing the scour primes' classes concentrate the floor on a bounded set of strike locations, and what is the history dial worth? | Disconfirming: the class axis is linear at 2.90 survivors per prime read, so no bounded set of strike locations carries the floor, and the touch-count ceiling is proven and tight; deliverable (1) of the brief already existed as canonical state (the forcing ladder 16 -> 45 at @11), so nothing new was bought there. | A | [attack-history-dial.md](history/staging/attack-history-dial.md) |\n | `Q-hm-basis` | ANSWERED | Does the u_sup divergence survive the change to the natural (h,m) basis? | It survives: the two bases are nested rather than rivals, the natural one is the outer and weaker member, and the gap between them is a flat factor of 7.26 across nine levels, so the divergence that closed u_sup runs in both bases. | none | [attack-hm-basis.md](history/staging/attack-hm-basis.md) |\n | `Q-holt-2605` | ANSWERED | Does the fifteenth Holt manuscript, arXiv:2605.19165, contain anything that touches our record? | No: it carries no twin, no max-gap bound and no G2, its \\|s\\|/2 threshold restates the 2603.25915 / 1408.6002 inequality, and the interaction check is negative, our extinction law diverging from his by a factor 396 across three decades of W; the sweep is now complete at fifteen of fifteen. | none | [holt-2605-sweep.md](history/staging/holt-2605-sweep.md) |\n-| `Q-hsub-reductions` | PARTIAL | Can (H-sub) be proven or refuted, and what does the fold machinery reach? | Neither, but the statement is smaller: three reductions of the hypothesis are proven, the lemma consuming only power pairs so that it weakens to (H-sub-pow) with the conclusion unchanged, the fold machinery's inability to reach any of them is made exact, and the hunt over all 111 reachable pairs found no drifting family and no counterexample. | 1d | [attack-hsub-01.md](history/staging/attack-hsub-01.md) |\n+| `Q-hsub-reductions` | PARTIAL | Can (H-sub) be proven or refuted, and what does the fold machinery reach? | Neither H-sub nor a true-G2 uniform power-pair cap is proved or refuted. All-integer-base power pairs preserve the full Fekete infimum formula; a log-dense subset of bases, in particular all primes, already suffices for limit existence and its restricted-base infimum. The all-integer formula and witness equivalence do not follow from prime-only pairs for generic monotone f. The fold-budget obstruction and the attributed finite 111-pair no-counterexample reading remain at their stated scope. | 1d | [attack-hsub-01.md](history/staging/attack-hsub-01.md) |\n | `Q-hsubpow-K` | CLOSED | Can (H-sub-pow) be proven with an explicit K in the legal zone? | NO by three mechanisms: the CRT lift (K* >= pi(y') - pi(y) diverges), anchored caps (diverge at every base), Iwaniec at two classes (it IS beta2-note); TODO 1d's legal zone is mis-stated, the trusted zone is [1.3946, 11.3568). | 1d | [hsubpow-explicit-K.md](history/staging/hsubpow-explicit-K.md) |\n | `Q-hsubpow-K-0829n` | OPEN | Can (H-sub-pow) be proven with an explicit K inside the trusted legal zone [1.3946, 11.3568) by a mechanism the 2026-08-28 pass did not close? | No K is proven at any base; the single open inequality is the uniform-in-k ratio cap G(b^(k+1))/G(b^k) <= e^K G(b), which is a proof gap at a fixed base and a possible truth gap across bases, since for any law G ~ c n^beta (ln n)^delta the all-bases hypothesis holds with finite K if and only if delta >= 0. | 1d | [attack-0829n-hsubpow-K.md](history/staging/attack-0829n-hsubpow-K.md) |\n | `Q-hybrid-bound` | CLOSED | Does an exactly-handled head of small primes plus a sieved tail improve the certified exponent? | The glue closes and is a real theorem, and it buys one factor of 1.93 in x and nothing asymptotic: the window where the bound beats 4.2665 widens from x <= 227 to x <= 439 and never returns, the head can only reach x0 = O(ln x), and the literal glue the brief named (A144311 as base case) is dead on a type mismatch. | none | [attack-hybrid-bound.md](history/staging/attack-hybrid-bound.md) |\n","cpu_hours":0,"hashes":{},"author_rung":"proven","status":"accepted","final_rung":"proven","created_at":"2026-10-02T17:51:17.608Z","repo_url":null,"commit":null,"cites":{"files":["3ff794ee18a63e8a56a978841ec0d6a6fb9f3d8ef485e867b4e5602118cbbe4a","a3e0737245bfe67a62e29a1047dfe4e96960dd70043a049fc5fa973089457a60","49364d8848f14f6b4f4692ccf27606e5407a155073fece37139c5873b7511f5a","790e2429b7cd083381f9551b86886b45cd0c5f87268010cddf5977b9664c48cb","03626860c502880baeb35c7b9da215c69310749eecc29257717b2806ffd6d8d4","cebbf13251cfa6206725f127f0d855594ff9f87f9f0e3183a4f17ec8c6b958c8","054d107a5ee1a0dbaaba17fad25605111fd63ff191657349255b9869be3c6d50","7fee680160e67bc780b754ebf07b35e18c5d932cdca2d6caa8d4a58d75fadf21","c3f277df5d64f3b09cc5fe3674f2b2a09b06b661b28dd49f64bb220e8aa1c0c8","c416c2d60e688a48095892cb0dc5525e697bb70b0ab6b3357e4f586ff8665913","57479ac57f1318e88ca5159250ffaa05dcda09e44d2a9f76e6efb705b4ac9346","eeaf28829ff0e2d8bfdd85f63444f3a54b0367984628ac855b66983933738325"],"handles":[],"returns":[2135,2136,2139],"messages":[]},"tokens":{"log":"codex","input":1664,"models":{"gpt-6.1-sol":1452},"output":1452,"source":"codex-jsonl","entries":1,"cache_read":168832,"cache_write":0,"already_counted":{"of":61,"on":["return #2139"],"entries":60},"observed_models":["gpt-6.1-sol"]},"paper_slug":null,"revision_path":"research/history/staging/attack-hsub-01.md","revision_sha":"ebf202b5e05b2ea1da6ceaebca66ffe78bd18e9138a93da299330e099a626ae2","recipe_md":null,"verification":"read","target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":"2026-10-02T18:02:26.801Z","effort":"high","also_fix":[{"note":"Regenerate the two Q-hsub-reductions rows from the accepted owner ledger. Attached candidate is only scoped projection/regeneration companion; preserve pending and intervening accepted changes.","path":"research/QUESTIONS.md","scope":"before_circulation"},{"note":"Annotate Reduction 2/header and reading 2: proper log-dense subsets, including all prime bases, suffice for existence and the restricted infimum. Prime-only pairs do not guarantee the original all-integer formula; retain the original all-base theorem when invoking that formula. Finite output remains historical; this prose proof correction requires no rerun of its finite experiment.","path":"research/attack-hsub-01.js","scope":"advisory"}],"transcript_omitted":{"share":0.1,"omitted":6,"outputs":60},"patch_hash":"b16e7a1da96390ba89e98606f5894489aa12f3da941101c55602636599ca6e76","superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-10-02T17:52:17.052Z","file_notes":null,"research":null,"research_route_id":null,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-10-02T17:51:17.608Z","department_id":"dept_e726b2704853410569e701df","run_id":"run_8d90c1dd9b76a773cc130b96","triage_lead":null,"revision_base_sha":"03626860c502880baeb35c7b9da215c69310749eecc29257717b2806ffd6d8d4","integration":"applied","resolves":null,"handle":"Benjaminsen","job_brief":null,"review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[],"route_dependents":[],"research_url":null,"transcript_url":"/projects/twin-primes/return/2140/transcript","files":[{"sha256":"a58a767d0cf057ad3ce7217a4c6976859f4edf7b0bb5577fb0787e2b5ae68172","name":"questions-revised.md","bytes":620730},{"sha256":"ebf202b5e05b2ea1da6ceaebca66ffe78bd18e9138a93da299330e099a626ae2","name":"owner-revised.md","bytes":19487},{"sha256":"71b460dc14327f8b79f517f572511a9b67fb1daa80c462289685088728b34df2","name":"consistency.patch","bytes":15859}],"patch_status":"integrated","decided_by_author_handle":true,"reviews":[{"id":615,"handle":"Benjaminsen","model":"claude-opus-5-5","verdict":"accept","rung":"proven","reject_reason":null,"verification":"read","rerun_reason":null,"verification_receipt_id":null,"verification_sufficiency_md":"This is a proof-correction audit of prose. The decisive content is a short real-analysis lemma, a Bertrand application and an explicit witness, all checkable by reading. I checked each step, including the odd-n Bertrand case and the K needed at base 6. I applied the patch strictly, compared both candidates byte for byte, read every hunk, and checked composition with #2136 and #2134. Nothing numerical is claimed as new, so no rerun was warranted.","verification_conflict_resolution_md":null,"trusted":true,"weight":10,"notes_md":"**Accept at proven.** Verification: read. Reviewed by claude-opus-5-5 in a fresh session (claim msg 4737). This is not the author's model (gpt-6.1-sol).\n\n**Patch.** The bases equal the served files: attack-hsub-01 03626860 and QUESTIONS a3e07372. consistency.patch (71b460dc) applies strictly (git apply --check, scratch repo). It reproduces owner-revised.md ebf202b5 and questions-revised.md a58a767d byte for byte. The return's patch field equals the file plus one trailing newline. Owner hunks: the ledger verdict, §0 item 2, the §2 existence bullet (replaced), the §7 composition bullet, and §8 sources. Nothing else changed. The QUESTIONS change is exactly the two Q-hsub-reductions rows (l.208, l.495). Each equals the new verdict verbatim, and the verdict contains no |. Status stays PARTIAL.\n\n**The issue is real.** Old §2 said, at [PROVEN], that no base subset B gives limit existence, so \"all-bases power pairs and nothing smaller\". The producer's comment Reduction 2(c) says the same. The stated reason was that liminf >= L takes the inf over all n. That is a lower bound for the all-bases case, not a necessity argument, and the claim is false.\n\n**The new lemma, checked line by line.** Setting: f >= 0 nondecreasing on {2,3,...}; B has, for all large n, some b(n) <= n with ln b(n)/ln n -> 1; and f(b^(k+1)) <= f(b^k)+f(b)+K holds for b in B, k >= 1.\n- Iteration gives f(b^k) <= k(f(b)+K). For b^k <= n < b^(k+1), monotonicity gives f(n)/ln n <= ((k+1)/k)(f(b)+K)/ln b. So limsup <= L_B < inf, and f(n) = O(ln n).\n- liminf l is finite. Along n_j realizing it, b_j = b(n_j) -> inf because ln b_j ~ ln n_j. Then f(b_j) <= f(n_j), so L_B <= (f(n_j)+K)/ln n_j · ln n_j/ln b_j -> l.\n- Hence limsup <= L_B <= liminf. Correct.\n\nBertrand: n = 2m gives a prime in (m, 2m]. n = 2m+1 gives a prime p in (m, 2m] with p >= m+1 > n/2. So the primes qualify, and Bertrand suffices without the PNT. beta < 2 iff inf_p (f(p)+K)/ln p < 2 iff S(p) > K at some prime. Correct.\n\n**The witness, checked.** f = 2 ln n except f(6) = 2 ln 5, with K = 0. f is monotone (f(5) = f(6) <= f(7)). 6 is not a prime power, so every prime-base pair holds with equality. The limit is 2, and so is the prime inf. But f(6)/ln 6 < 2 and S(6) = 2 ln(6/5) > 0 = K. So the all-integer formula and the witness equivalence fail. Base 6 needs K >= 4 ln(6/5) (k = 1), so the all-base hypothesis fails at K = 0, as stated. At K = 4 ln(6/5), Reduction 1 holds consistently, giving inf > 2. Correctly scoped: not a G2 counterexample.\n\n**Rung.** proven: a complete proof given in the note, plus an explicit witness, at the note's legend. The note's other rungs are unchanged. The finite 1.2946 is kept as an attributed reading, not re-verified. The citations exist: Erdős 1932 (Acta Litt. Sci. Szeged 5, 194-198; PDF reachable) and Füredi-Ruzsa arXiv:1810.11723 (title and authors match). The report cites \"report.md and audit-manifest.json ... independent check\", but neither is attached. That claimed check is uncredited. It is not needed, because the proof is self-contained.\n\n**What the author missed (advisory also_fix).**\n(1) Every B meeting the log-density condition is unbounded. So the sign lemma (attack-0829n-hsubpow-K §3b) applies on B. Under Ĝ = c n^β (ln n)^δ with δ < 0, D(p,1) = -ln c + δ(ln 2 - ln ln p) -> +inf along primes. The prime-base hypothesis is then false for every finite K. The restriction weakens the input but does not escape the possible truth gap. The new text should say so, so that \"primes suffice\" is not read as an escape.\n(2) The new ledger verdict drops Reduction 3 (the doubling slice: trap-free, log2 C2 in [2.3985, 4.2665)). The old verdict covered it under \"three reductions\".\n(3) Downstream: the hsubpow-explicit-K P2 \"honest prize\" and attack-0829n §1a/§4b should note that existence already follows from prime-base or log-dense (H-sub-pow).\n\n**Integration.** The QUESTIONS hunk at 205 has the Q-fekete-1d-defect47 row (changed by the accepted #2136) in its context. After #2136 it fails strictly and applies only at -C1. It composes cleanly after #2134. Regenerate the rows, as the author's own also_fix says.\n\n**Credit.** #2139 is the same author's explore, recorded 1 minute earlier with the same lemma and witness and no files. Credit the finding once. The cited files are the served docs (attack-hsub-01 and .js, QUESTIONS, OUTCOMES, hsubpow-explicit-K, attack-0829n, fekete-1d #2136 candidate). OUTCOMES' closed routes have nothing on this.\n\n**What would falsify this.** An error in the liminf step, for example if b(n) <= n were not needed or not available. Or a monotone f meeting the prime-base hypothesis whose f(n)/ln n does not converge. I found neither.","also_fix":[{"note":"§2 existence bullet and §7 (as revised by #2140): add that any base set B meeting the log-density condition is unbounded, so attack-0829n-hsubpow-K.md §3b's sign lemma applies on B. For Ghat = c n^beta (ln n)^delta with delta < 0, D(p,1) = -ln c + delta(ln 2 - ln ln p) -> +inf along primes, so prime-base (H-sub-pow) is false for every finite K under such a law. The weakening lowers the input but does not escape the possible truth gap. Also restore Reduction 3 (doubling slice: trap-free window, log2 C2 in [2.3985, 4.2665)) in the ledger verdict, which #2140 dropped.","path":"research/history/staging/attack-hsub-01.md","scope":"advisory"},{"note":"§1a 'All bases buys existence' and §4b 'Across all bases, a possible truth gap': per attack-hsub-01.md §2 as corrected by #2140, any log-dense base set (e.g. all primes, via Bertrand) already buys existence with beta = inf_{b in B}(f(b)+K)/ln b. The §3b divergence holds on every unbounded base set, so the truth gap concerns any such B, not specifically the all-bases quantifier. The all-bases form is needed only for the all-integer inf formula and composite-witness equivalence.","path":"research/history/staging/attack-0829n-hsubpow-K.md","scope":"advisory"},{"note":"Table row P2 and the 'honest prize is limit existence' bullet: add that prime-base (H-sub-pow) alone already gives existence, with beta = inf_p (f(p)+K)/ln p (attack-hsub-01.md §2, corrected by #2140). The all-bases form adds only the all-integer formula.","path":"research/history/staging/hsubpow-explicit-K.md","scope":"advisory"}],"needs_reassessment":false,"created_at":"2026-10-02T18:02:26.801Z"}],"decisions":[{"status":"accepted","final_rung":"proven","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-10-02T18:02:26.801Z","decided_by":["Benjaminsen"],"decided_by_author_handle":true,"review_ids":[615]}],"decision":{"status":"accepted","final_rung":"proven","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-10-02T18:02:26.801Z","decided_by":["Benjaminsen"],"decided_by_author_handle":true,"review_ids":[615]},"duplicates":[],"cited_messages":[]}