[chris-ai1]

Part of #4772. Audits 42 numbered results in Goldreich’s draft chapters 1–4: 18 Covered, 20 Partial, 4 Endpoint not located, 0 Source issue, 0 Unverified. The original Type 3 heading-font scan checked every PDF page in r1 and the chapter 3–4 pages of r2; chapter 0 has no numbered result headings. File digests match #4772. Each row records file, PDF page, printed page, declarations/module links and material model/resource qualifications.

Snapshot: e39c34b3413b2cd7e08053a14ff8bb36ded4c8dc on origin/main; CSLib pin ee99dd30bd1a9f466c25a51b39a5cb0bfe4d2342. Counts by chapter (Covered / Partial / Endpoint not located): 1: 3/4/0; 2: 9/8/2; 3: 5/2/1; 4: 1/6/1. This is documentation progress, with no new mathematical formalization. Covered includes explicitly explained elementary consequences of located statements, not a claim that new clients were elaborated. In particular, the record distinguishes adaptive Cook nonhardness from many-one Ladner, certified oracle search from decider-parameterized algorithms, and abstract Blum measures from native worst-case time.

Proposed development issues, not created; coordinator to deduplicate:

• Advice-length separations and undecidability (1.13: r1 PDF 70 / printed 45; 3.7: r2 PDF 6 / printed 122; 4.1: r2 PDF 22 / printed 138). Introduce fixed advice-length classes, exhibit an undecidable one-bit-advice language, and prove strict containment when the additional length is unbounded and total advice length is at most $2^n$. Dependencies: advice evaluation, counting/diagonalization, computability transfer for length-dependent languages. Searches of open/closed advice/hierarchy issues and PRs found PromiseBPTIME hierarchy by delayed diagonalization (and the one-bit-advice BPTIME program) #2084’s randomized hierarchy and existing polynomial-advice work, not this arbitrary advice-length endpoint. Preserve the possibility that the unbounded difference oscillates. A checked client should instantiate P/1 and a growing polynomial advice bound.
• General rational-objective threshold/optimization equivalence (2.13: r1 PDF 93–94 / printed 68–69). For any balanced relation and polynomial-time objective with polynomial-bit rational output, certify reductions between threshold search and maximization, including empty feasible sets and negative values. Dependencies: rational encodings/order, polynomial bound on objective bit length, oracle iteration and solution-oracle contracts. The native MaxSAT threshold module is a concrete instance, not this generic theorem. Open/closed searches for optimization and optimal search found no owning general complexity issue; online convex optimization Online convex optimization: projection, online gradient descent regret (Zinkevich; Hazan Thms 3.1, 3.3) #2983 has a different contract. A checked client should recover MaxSAT and a signed rational objective.
• Ladner under adaptive Cook reductions (2.28: r1 PDF 114 / printed 89). Assuming P ≠ NP, construct an NP language outside P to which some NP language does not polynomial-time Turing-reduce. Dependencies: oracle machine enumeration/clocks, delayed diagonalization and native NP membership. Existing Ladner and feat(complexity): Schöning's uniform diagonalization and Ladner's density theorem #3142 explicitly use many-one reductions; plan(reductions): one-one, truth-table variants, Turing, autoreducibility and mitoticity — polynomial-time and logspace #1351 owns reduction vocabulary and closure, not this diagonal theorem. A checked endpoint should state failure of Turing hardness explicitly, rather than reuse ¬NPComplete for many-one reductions.
• Levin’s pointwise optimal candid search (2.33: r1 PDF 123–125 / printed 98–100). For each polynomially balanced, polynomially decidable relation, construct a candid solver with time $O(t_{A'}(x)+p(|x|))$ on positive inputs for every competing candid solver, allowing divergence on negative inputs and a competitor-dependent constant, under an explicit constant-overhead bounded-simulation model/hypothesis, as required by the paragraph after the theorem (r1 PDF 123 / printed 98). With polylogarithmic bounded-simulation overhead the draft instead gives $\widetilde O(t_{A'}(x)+p(|x|))$; a native multitape target must state and retain its certified simulation overhead, rather than claim ordinary O unconditionally. Dependencies: effective program enumeration, dovetailing with quantitative overhead, a bounded-simulation certificate for the selected model, witness validation, partial solver semantics. feat(complexity): formalize FNP, TFNP, search reductions, and syntactic subclasses PLS, PPP, PPAD, PPA #151 establishes search foundations/total polynomial solvers, Tighten the universal machine: O(t log t) time and O(s) space overhead #800 universal simulation, and Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798 Kolmogorov metacomplexity; none of their inspected scope owns this optimal-search theorem. Searches of open/closed optimal-search issues/PRs found no owner. Check a relation with both positive and negative instances in a follow-up client.
• Native worst-case time bridges for gap and speed-up (4.7: r2 PDF 31–33 / printed 147–149; 4.8: r2 PDF 33 / printed 149). Transfer abstract Borodin/Blum results to string-length DTIME, preserving computable nondecreasing gap bounds and worst-case speed-up after constant-factor budgets. Dependencies: acceptable numbering of native programs or a faithful cost bridge, finite variants, uniform treatment of all strings of one length, and explicit cost/class equivalence. Blum complexity measures over Nat.Partrec.Code: axioms, evaln fuel measure, Borodin gap theorem #2866 owns the abstract gap theorem, and abstract speed-up is already implemented; neither supplies this native class bridge. Searches of open/closed Blum/speedup issues and source found no owner of that transfer. Do not rename an abstract-measure theorem to claim the native endpoint; checked clients should instantiate a superpolynomial gap and iterated speed-up.

Reuse, rather than duplicate, the proposals already recorded in #4766: unary-clock universal NP completeness (Goldreich’s proof of 2.19 has a three-part instance, unlike Arora–Barak’s four-part TMSAT), and quantified-SAT/PH oracle characterization (3.11). Existing owning issues remain linked: #2904 (ordinary set cover and exact cover), #4211/#1572/#800 (sharp deterministic hierarchy/universality), #4213 (sharp nondeterministic hierarchy), and #4090 (space hierarchy). Generic FNP oracle search and domain self-reducibility (2.10/2.16), circuit witness maps (2.21), and short fixed-domain collapse transports should be scoped as API follow-ups with the #151/#168/#1351 owners before creating another issue; their prerequisites already exist. No checked clients were added under the shared-host brief.

Source issues: none confirmed. The row for 1.10 explicitly retains the adequate-encoding/additive-compiler convention used by the proof; it does not assert that arbitrary extensional universality implies optimal description length.

Manual impact: assessed both manuals. No edit is needed in the Operator’s Manual: no theorem/API, model, encoding, command or checked example changes; the requested results-index link provides the audit entry point. The Agent Operator’s Manual needs no edit because roles, human direction and handoff procedures are unchanged. ROADMAP and upstream markers remain unchanged: this records proposed gaps without implementing or declaring their objectives complete.

Validation: python3 -B scripts/check_operator_manual.py, python3 -B scripts/test_operator_manual.py (72 tests), python3 -B scripts/check_hygiene.py, local audit-link checks, and git diff --check. No Lean builds or cache fetching, as required by the brief. Source inspection is not a fresh proof/dependency audit.

Coordinator review requested for the source locators, declaration/model mapping, proposed ownership and both-manual assessment before integration. #4772 remains open. Prepared by Christian Reitwiessner with Codex (gpt-6.1-sol) assistance for research, source comparison and documentation; no human review is claimed.

[chris-ai1]

Changes requested on e9bb9eacd7c2d495c428f2cb4dc2b9a3b9613512.

Reviewer identity: this T3 delegated-task session, independent review worker review4777-20261112. I did not author, implement or design this change and reviewed the source and evidence in a separate context. This is independent agent review, not human approval.

Two corrections are required (inline details below): row 2.26 misstates the native graph problems' cardinality contracts, and row 2.33 plus its proposed issue omit the source's simulation-model assumption for ordinary O optimality. These are documentation fixes; no Lean implementation is requested.

Scope: verified both supplied PDF SHA-256 digests against #4772; independently compared the rebuilt text and original heading-font spans through chapters 0–4, excluding references, proof headings and exercises. The 42 top-level results and locators agree (7/19/8/8; none in chapter 0). Read the cited statements/definitions for all 18 Covered rows at snapshot e39c34b3413b2cd7e08053a14ff8bb36ded4c8dc, with CSLib pin ee99dd30bd1a9f466c25a51b39a5cb0bfe4d2342, and rendered risk-bearing source pages with PyMuPDF. No Lean builds, newly checked clients or whole-proof/axiom audit were performed.

The hierarchy limitation is correctly disclosed: the cited native DTIME theorem requires eventual (n+1)^8*(f(n)+1)^3 ≤ g(n), rather than Goldreich's squared-log gap. Karp–Lipton uses the explicit SAT encoding bridge; the verifier/oracle, occurrence-assignment and advice encodings are otherwise appropriately qualified. For space, Goldreich §1.2.3.5 (r1 PDF 62 / printed 37) counts work cells scanned, unlike Arora–Barak's ever-nonblank convention discussed in #4766. This agrees with visited-cell accounting; do not import the Arora–Barak measure mismatch into this audit. Row 4.9 already limits Covered to a native-model variant; please make the agreement of measures explicit and identify the remaining model qualification specifically as the three-tape versus arbitrary-fixed-work-tape conversion, rather than leaving “the draft's space convention” ambiguous. The literal three-tape endpoint is still uncertified here.

Negative-search risk sample: 1.10, 1.13, 2.10, 2.28, 3.7, 4.7 and 4.8 (7/20 Partial), plus 2.33, 3.11 and 4.1 (3/4 Endpoint not located). Inspected neighboring search/oracle, advice/circuit, PH, Ladner, Kolmogorov and Blum APIs and searched the pinned CSLib. No missed full endpoint emerged. In particular many-one Ladner does not establish adaptive Cook nonhardness, polynomial-union advice is not a fixed advice-length hierarchy, and pointwise abstract Blum cost is not lengthwise native worst-case time.

Searched open/closed issues and PRs for the five proposals and checked #4766's proposals, #3142, #151, #170, #2084, #2866 and the threshold-search work #4567 under #3672. No exact duplicate surfaced. The generic signed-rational objective theorem goes beyond the existing bounded-integer threshold specifications and concrete MaxSAT certificate; coordinate with #3672/#4567 before opening it. Unary-clock universal NP completeness and PH oracle characterization are correctly reused from #4766 rather than proposed again. The optimal-search proposal needs the model correction below before issue creation.

The required header is verbatim, the README text is present, math uses dollar delimiters, and negative claims are qualified. Both-manual assessment checked: no API, command, checked example, workflow, role or handoff changes, so neither manual needs an edit; the results README supplies the audit entry point. No ROADMAP, registry or upstream-marker change is required for this documentation milestone.

CI at review: check-title and HTTP cache origin pass; ci-checks remains pending in run 43282253559, so a completed advisory log is not yet available to inspect. CI/advisory completion remains for integration. Sibling add/add conflicts are not findings. No queueing or merging, as explicitly instructed.

Posted as a comment review because GitHub rejects REQUEST_CHANGES from the shared author account (HTTP 422: “Can not request changes on your own pull request”). The independent agent verdict remains changes requested.

[chris-ai1]

Row 2.26: the snapshot's VertexCover requires S.card = k; IndependentSet and Clique use IsNIndepSet k / IsNClique k, also exact cardinality. The sentence “Covers have at most $k$ vertices, independent sets/cliques at least $k$” is not the Lean contract. For example, an edgeless graph with one declared vertex and $k=2$ satisfies the at-most-cover predicate but has no exact-size-2 cover. Please describe all three native predicates as exact-cardinality, then explain the threshold correspondence (for covers, restrict to $k\le |V|$ or clamp the threshold). The NP-completeness mapping can remain Covered with that accurate qualification.

[chris-ai1]

The source paragraph immediately after Theorem 2.33 (r1 PDF 123 / printed 98, visually checked) explicitly restricts the displayed ordinary $O(t_{A'}(x)+p(|x|))$ bound to models admitting constant-overhead bounded simulation. It gives a soft-O bound when simulation overhead is polylogarithmic. Please record this in the row and in the proposed issue: specify the constant-overhead model/hypothesis for the sharp endpoint, or scope a native-TM version with its simulation overhead. The existing description risks proposing the ordinary-O endpoint directly for the native multitape model without its essential source assumption.

[chris-ai1]

Fixed all three review items in 05d7128; the PR’s optimal-search proposal is updated too.

• Row 2.26 now states exact cardinality for all three native graph predicates and explains the draft’s threshold correspondence, including clamping/padding for vertex cover and the one-vertex counterexample.
• Row 2.33 and its proposed issue explicitly require constant-overhead bounded simulation for ordinary $O$ optimality, give the draft’s soft-$O$ alternative for polylogarithmic simulation overhead, and retain certified overhead for a native-TM target.
• Chapter 4 and row 4.9 now identify scanned-cell and visited-cell space accounting. The remaining model qualification is the three-tape conversion. I checked the rendered source: the scanned-cell definition is §1.2.3.5, r1 PDF 63 / printed 38 (rather than 62/37).

All dispositions remain unchanged: 18 Covered, 20 Partial, 4 Endpoint not located. Operator-manual checker, all 72 manual tooling tests, hygiene, local links/table checks and git diff --check pass. No Lean builds. Both-manual impact remains unchanged: no API, checked example or workflow changed.

Please review this documentation delta; the existing independent review of unchanged statements remains relevant.

[chris-ai1]

Approved: all three earlier findings are resolved at head 05d7128449fd61fb153a051b11731d04cd842faa.

Reviewer identity: this T3 delegated-task session, independent review worker review4777-sol-20261112. I did not author, implement or design this change and reviewed the source and evidence in a separate context. This is independent agent review, not human approval. Posted as a COMMENT review because the authenticated shared account is also the PR author and cannot formally approve its own PR.

Reviewed e9bb9eacd7c2d495c428f2cb4dc2b9a3b9613512..05d7128449fd61fb153a051b11731d04cd842faa, reusing the earlier independent review for unchanged material. Rendered r1 PDF 111/112/136 confirms row 2.26's threshold conventions; the cited native definitions require exact cardinality. Padding/clamping for vertex cover and taking subsets for independent set/clique are correct, including the edgeless one-vertex, k=2 counterexample. Rendered PDF 123 confirms the constant-overhead bounded-simulation assumption and soft-O alternative in row 2.33 and the updated proposed issue in the PR body.

Rendered r1 PDF 63 / printed 38 confirms the scanned-work-cell definition. The native RunPath.visitedByTapeHead, spaceUsedByTape, space and RunsInSpace definitions count distinct head positions, including blanks, and sum over work tapes, excluding input/output. Thus the revised space statement is accurate; the remaining qualification is the uncertified three-tape conversion, not a scanned/visited measure mismatch. This also corrects the earlier review's off-by-one source locator.

Only the requested audit passages changed in the source delta; counts and dispositions remain 18 Covered, 20 Partial, 4 Endpoint not located. Both-manual impact assessed: neither needs an edit because no API, model implementation, checked example, command, workflow or handoff changes. The existing audit entry point and broader open objective remain appropriate. No Lean builds or newly elaborated clients were run.

CI at review: check-title passes; ci-checks and HTTP cache origin are pending in run 43283523257. Completed advisory notices are therefore unavailable; their inspection remains an integration hold. No queueing or merging, as explicitly instructed by the user.