[chris-ai1]

Part of #4711. Audits all 33 numbered results in chapters 6–7 of the pinned 2007-01-08 draft, against main b91d5151fd7dc665a5e3efcb466077caf44e690d (CSLib ee99dd30bd1a9f466c25a51b39a5cb0bfe4d2342). Each row records printed/PDF locators, exact declarations or qualified negative searches, and model/resource differences. Documentation progress only; the broader audit and mathematical gaps remain open.

Counts: 12 Covered, 10 Partial, 5 Endpoint not located, 6 Source issue, 0 Unverified (chapter 6: 5/4/3/0/0; chapter 7: 7/6/2/6/0). Covered includes explicitly identified consequences of existing general APIs, not newly checked client files. Key boundaries are uniform versus nonuniform circuits, expected-time versus bounded-time partial-answer ZPP, and hitting versus occupation-time concentration. Literal draft defects include the missing nonzero hypothesis in 7.5, infeasible length-one gap in 7.9, false two-sided bound in 7.11, impossible edge-expansion normalization in 7.35, absolute-versus-one-sided spectral confusion in 7.36, and the positive exponent in 7.41.

Proposed development issues (not created)

These are proposals for coordinator deduplication, not implementation claims. Searches checked open and closed issues/PRs by the endpoint names and relevant terms; existing ownership is linked in the audit.

1. Meyer EXP collapse. Draft 6.14, printed 107 / PDF 123: prove EXP encBits ⊆ PPolyOn encBits → EXP encBits = SigmaP 2 encBits, then transport to other encodings only with the necessary hypotheses. Dependencies: exponential computation/tableau access, circuit advice, quantified verification and the reverse inclusion already supplied by SigmaP_subset_EXP. Frontier track: Limaye–Srinivasan–Tavenas constant-depth arithmetic lower bounds; Kabanets–Impagliazzo #891 owns Kabanets–Impagliazzo; Frontier track: Williams' NEXP ⊄ ACC⁰ and Murray–Williams NQP ⊄ ACC⁰ (algorithmic method) #889 owns Williams/easy witnesses, but neither inspected body owns this standalone EXP collapse. Coordinate with those tracks before creating a separate issue.
2. Parallel-machine characterization of uniform NC. Draft 6.24, printed 110 / PDF 126: fix a PRAM or routed-network semantics with polynomial processors, logarithmic words, polylogarithmic time and uniform setup, and prove both circuit/machine simulations. Dependencies: Borodin: NSPACE(s) in circuit depth O(s²) and NL ⊆ AC¹ (B1 nonuniform milestone; uniform B2–B4 remain) #4224's uniform circuit/NC conventions, explicit processor instruction costs and routing semantics. Borodin: NSPACE(s) in circuit depth O(s²) and NL ⊆ AC¹ (B1 nonuniform milestone; uniform B2–B4 remain) #4224 B2–B4 owns uniform circuits/space simulation, not the parallel-machine equivalence; PRAM searches located no separate owner.
3. DC-uniform exponential circuit characterization. Draft 6.29, printed 111 / PDF 127: define polynomial-time direct access to size, gate labels and edges of an exponential-size circuit, with explicit unary input length/binary gate indices; prove constant-depth input-negation-only circuits characterize PH, and unrestricted depth characterizes EXP. Dependencies: unbounded-fanin circuit semantics, PH quantifiers, succinct local access, exponential evaluation. plan(descriptive): descriptive-complexity lanes (Jetski coordinator 39f2) #4075 owns descriptive-logic lanes and Borodin: NSPACE(s) in circuit depth O(s²) and NL ⊆ AC¹ (B1 nonuniform milestone; uniform B2–B4 remain) #4224 polynomial-size uniform families; neither inspected scope owns this endpoint.
4. Feasible inverse-polynomial BPP/RP amplification. Draft 7.9–7.12, printed 121–122 / PDF 137–138: use a feasible gap such as 1/(4*(n+1)^c) (natural c), or an eventual gap with finite exceptions handled explicitly. Prove weak-gap BPP equals BPP and amplify one-sided inverse-polynomial success while keeping zero acceptance on nonmembers. Dependencies: native majority/OR repetition, countTrue_average_deviation_pow, replicate_failure_pow, polynomial unary budgets and seeded/PTM bridges. Existing fixed-threshold BPP/RP amplification and feat(quantum): the class QMA, NP ⊆ QMA, BQP ⊆ QMA and weak error reduction #2876's quantum QMA weak amplification do not supply this classical class theorem; exact weak-gap PR searches found no owner.
5. Expected-time classical randomized bridges and coin simulation. Draft 7.8, 7.14–7.15, printed 121, 124 / PDF 137, 140: bounded milestones for (a) expected-polynomial Las Vegas PTMs iff bounded-polynomial partial-answer ZPP; (b) exact sampling of a fixed bias with polynomial-time binary digits in expected constant native time; (c) von Neumann extraction from i.i.d. bias 0 < ρ < 1, with fair output and expected cost O(1/(ρ*(1-ρ))). Dependencies: stopping-time/native runtime semantics, geometric tails, truncation/restart and costed bit algorithms. Knuth–Yao: entropy bounds for generating finite distributions from fair coins (DDG trees) #3360 / landed feat(Probability): DDG trees and the Knuth–Yao entropy bounds #3393 gives DDG trees and expected flip bounds and explicitly disclaims sampler running time; plan(logspace): randomized logspace — RL and BPL, inclusions, USTCON ∈ RL, Nisan's generator #459 owns randomized space, not these expected-time endpoints. Split the milestones if needed, retaining a shared runtime model.
6. Corrected expander occupation-time Chernoff bound. Draft 7.41, printed 145 / PDF 161: for a uniformly started walk on an undirected regular rotation map with absolute spectral parameter λ < 1, bound the deviation of the bad-vertex fraction by 2 * exp (-(1-λ)*δ^2*k/60) (or first verify a precise published constant/version), for k ≥ 1 and δ > 0. Dependencies: existing walk probability space and spectral contraction, weighted/tilted walk operators and a moment-generating-function estimate. Probability/Chernoff assumes independent coordinates; Expander/Hitting bounds all-bad walks. Searches found no owning development issue; Consolidation: well-scoped cleanup tasks (replaces the metric-driven quality program) #949/quality(foundations): area checklist #614 are general quality programs, not this endpoint.
7. Finite Shannon density and source-bound hierarchy corollaries. Draft 6.15/6.17, printed 107–108 / PDF 123–124: expose a quantitative proportion of truth tables below size 2^n/(10*n) for n ≥ 100, documenting rounding and gates versus total vertices, and translate the draft's T log T = o(T') hypotheses to the existing SIZE_ssubset API. Dependencies: existing circuit counting, Shannon and additive-gap interpolation. Do not reprove those ingredients. Searches found no issue owning these source-bound/density corollaries; the existing hierarchy theorem is substantial partial coverage.

No new issue is proposed for uniform families/NC closure already owned by #4224, nor the classical random-walk analysis owned by #459. The auxiliary 7.40 matrix decomposition is recorded as not separately exposed; an elementary client/API follow-up can decide whether naming it is useful. Proposed checked clients for the source defects (zero polynomial, length-one weak gap, one Bernoulli trial, a two-vertex bipartite graph, and averaged half cuts) were not added, per the shared no-build brief.

Manual impact

Operator's Manual: adds links from the circuit and verifier chapters to the audit's model boundaries and gaps; no API or executable example changed. The results inventory links the expanded audit. Agent Operator's Manual: no edit needed because roles, handoffs and procedures are unchanged. ROADMAP and upstream coordination need no change: this audits existing sources and leaves the development proposals here for deduplication. No library files or authorship headers changed; existing Christian Reitwiessner audit credit is preserved.

Validation and review

python3 -B scripts/check_operator_manual.py passed; python3 -B scripts/test_operator_manual.py passed (72 tests). python3 -B scripts/check_hygiene.py passed (a repository-wide source/bibliography check, not a Markdown validator). Local audit-link existence, the 33-row/disposition count and git diff --check were checked. No Lean build, dependency/cache download or new checked client was run, as required by the shared brief. Source-level audit is not a whole-library semantic or axiom audit.

Coordinator review requested for the exact source/model mappings, source counterexamples, proposed-issue deduplication and both manuals' impact assessment. The independent review requested correction of 7.12; the correction reclassifies it as Partial and removes the erroneous source-defect claim. Delta review is requested; this worker does not approve or merge its own PR.

Prepared for Christian Reitwiessner with Codex assistance for primary-source inspection, repository/issue searches and documentation.

[chris-ai1]

Request changes on 6c2d2917da41767def9d16156634e6b02646ce76.

Reviewer: this T3 delegated-task session (Codex independent review, PR #4767, 2026-11-12). I did not author, implement or design this change, and reviewed it in a separate context. This is agent review, not human approval. I read origin/main's current AGENTS.md first and the pinned CSLib guidance.

One blocking source-attribution finding is attached to the 7.12 row. The rendered, hash-verified PDF prints zero in the nonmember conclusion, not one. Please correct that row, the concluding source-repair paragraph, the PR description and disposition totals. The genuine remaining gap is the inverse-polynomial-success class bridge; the fixed-threshold RP theorem remains partial coverage. Do not retain the claimed reversed conclusion as a draft defect.

Review scope and evidence: scanned rendered PDF pages 117–162 and compared the numbered headings with the table: 12 chapter-6 and 21 chapter-7 results, with no omitted numbered result located. Inspected all 12 Covered mappings against declaration statements at snapshot b91d5151fd7dc665a5e3efcb466077caf44e690d (CSLib ee99dd30bd1a9f466c25a51b39a5cb0bfe4d2342), including the generic reduction composition for 6.32 and analytic specialization for 7.27. The circuit gate/vertex distinction, typed encoding-image scope, uniform/nonuniform distinction, and use of Reingold rather than the classical walk are appropriately disclosed. No additional Covered-row blocker found.

Checked every Source issue against rendered pages, not just extracted text. The other six findings withstand inspection: 7.5 lacks the nonzero hypothesis; 7.9 is infeasible at length one; 7.11 fails for one Bernoulli trial with p=1/2 and delta=1/4; balanced-cut averaging obstructs 7.35's normalization; the two-vertex bipartite graph refutes 7.36(2) for absolute spectral expansion; and 7.41 prints a positive, vacuous exponent. These are source problems rather than library modeling choices.

Sampled the underlying source/search evidence for all 14 Partial/Endpoint-not-located rows, including uniformity, EXP collapse, counting/hierarchy, expected-time ZPP/coin simulation, and the stronger laziness hypothesis in Connected.lean. Existing ownership links #4224 and #459 are appropriate. Reviewed all seven development proposals and searched open/closed issues and PRs by endpoint terms; no additional exact duplicate owner was located. Retain the stated coordination with #889/#891 and DDG #3360/#3393. These are bounded negative searches, not proofs of absence.

Both-manual assessment: the two Operator's Manual additions are relevant links to the audit and introduce no executable example or procedure. No Agent Operator's Manual edit is needed because roles and workflows do not change. The results-inventory link and preserved source credit are appropriate; no ROADMAP/upstream-marker change is required for these proposals. Dollar-math and qualified negative wording are satisfactory. Expected sibling-file merge conflicts are not a review finding.

CI: gh pr checks 4767 currently reports check-title and HTTP cache origin passed; ci-checks and the manual PDF build are pending. The ci-checks job has not finished, so its final advisory notices have not yet been reviewed. No Lean builds or checked clients were run, as requested; this is source-level coverage review, not a fresh proof/axiom audit or rendered-manual approval. Do not queue or merge on this review; the user explicitly prohibited both.

Finding at results/arora-barak-2007.md:90:

[P2] The claimed draft defect is absent from the PDF. On printed p. 122 / PDF p. 138, Theorem 7.12's conclusion (2) visibly reads $\Pr[M′(x)=1]=0$, agreeing with the extracted text and premise. It does not print 1. Reclassify this as Partial for the actual inverse-polynomial-success bridge (or accurately substantiate another source issue), remove the always-accept argument, and update the repeated claim at the end of this section and in the PR body/counts. The primary source is the pinned 2007-01-08 PDF, SHA-256 da0881782a35bde6a0779a2eb1a8d480f39fbddf70bbb92824d1dc5550a033b2, page 138.

[chris-ai1]

Fixed in 9b86f47, as a new commit without rewriting history. I re-rendered PDF page 138 at 3× resolution and verified the pinned SHA-256: conclusion (2) prints zero acceptance on nonmembers. My earlier source reading was wrong.

7.12 is now Partial: Cslib.Complexity.mem_RP_iff_forall_decidesWithOneSidedErrorExponent provides polynomial error exponents from fixed success 1/2 while preserving zero acceptance on nonmembers; the inverse-polynomial-success native class bridge remains unlocated. Removed the erroneous defect claim from the row, concluding paragraph and PR description. Corrected totals in the audit and PR body: 12 Covered, 10 Partial, 5 Endpoint not located, 6 Source issue, 0 Unverified (chapter 7: 7/6/2/6/0). The seven issue proposals are unchanged.

The manual checker, all 72 manual tooling tests, row/count checks and git diff --check pass. No Lean builds were run. Both-manual assessment is unchanged: this corrects the linked audit and changes no API, example or workflow. Please review this delta; no queueing or merge is requested.

[chris-ai1]

Approve the reviewed delta 6c2d2917da41767def9d16156634e6b02646ce76..9b86f47d0bfbcd862f6b6424a262fb08b7feaba8; no remaining finding in this delta. This resolves the blocking 7.12 finding in the earlier independent review, whose unchanged review scope I retain.

Reviewer identity: this T3 delegated-task session (Codex independent delta reviewer, PR #4767, 2026-11-12). Exact reviewed head: 9b86f47d0bfbcd862f6b6424a262fb08b7feaba8. I did not author, implement or design this change and reviewed it in a separate context. This is agent approval, not human or platform approval; the shared author account prevents a formal approving review, so this is a comment review.

I rendered PDF page 138 with PyMuPDF from /tmp/pdfdeps2 and verified the pinned PDF SHA-256 da0881782a35bde6a0779a2eb1a8d480f39fbddf70bbb92824d1dc5550a033b2. Theorem 7.12 visibly has zero acceptance on nonmembers in both premise and conclusion. The corrected Partial row accurately maps mem_RP_iff_forall_decidesWithOneSidedErrorExponent: its underlying RP premise has success at least 1/2, and its amplified conclusion retains rejection of every nonmember seed. replicate_failure_pow supplies inverse-success statistical repetition, without the missing native class bridge. I inspected the actual definitions and statements at the reviewed head; no Lean builds were run.

Only results/arora-barak-2007.md changed in this delta: the 7.12 row, removal of its erroneous source-repair claim, neutral wording about inspected formulas, and the corrected total. Independent row counts give chapter 6: 5 Covered / 4 Partial / 3 Endpoint not located / 0 Source issue; chapter 7: 7 / 6 / 2 / 6. Their sum is 12 / 10 / 5 / 6, with 0 Unverified and 33 results. The audit, concluding summary, PR description and author correction agree. Nothing else changed; git diff --check passes.

Both-manual assessment remains valid: the Operator’s Manual links still accurately describe the corrected audit and introduce no changed API, example or procedure; the Agent Operator’s Manual needs no edit because roles, handoffs and workflows are unchanged. No further inventory, ROADMAP, upstream-marker or credit change is needed for this correction.

CI at review: check-title passed; HTTP cache origin, ci-checks and the manual PDF build remain pending. ci-checks has not finished, so final advisory notices are unavailable and have not been reviewed. This documentation-only delta changes no Lean declarations or proofs. Approval does not assert completed CI or rendered-manual approval. No queueing or merging: both were explicitly prohibited by the user.

[chris-ai1]

Coordinator restack: merged main (after #4769 and #4774 landed) as f39e5afed6685b199dc4d0bb019d8f48c7e18b4d. Conflict resolution only:

• results/arora-barak-2007.md: this PR's chapter 6–7 sections, then main's chapter 8–10 sections, then Chapter 14. The remaining-work sentence now reads "Chapters 6–10 and 14 have chapter-specific records above; …".
• results/README.md: this PR's chapters 6–7 clause, followed by main's chapters 8–10 clause.

The operator-manual and hygiene checks pass. Because check_restack.py reports these document conflicts, a bounded non-author check of the joined sections is running as required by the review cycle. Queueing follows that check and current-head CI.

[chris-ai1]

Approve the merge-resolution delta at f39e5afed6685b199dc4d0bb019d8f48c7e18b4d; no findings. The prior approved audit review remains applicable to the unchanged content.

Reviewer identity: this T3 delegated-task session (Codex independent merge-resolution reviewer, PR #4767, 2026-11-12). I did not author, implement or design this change, or perform the merge, and reviewed it in a separate context. This is agent approval, not human approval. The shared author account prevents a formal approving review, so this is a comment review.

I ran python3 scripts/check_restack.py 9b86f47d0 f39e5afed from a detached checkout of current origin/main (33f33d68517552e2f1befd3a8e13472bcb15f444). It reports only the two expected conflict paths. Byte comparisons confirm the entire chapters 6–7 block is identical to approved head 9b86f47d0bfbcd862f6b6424a262fb08b7feaba8, and the entire chapters 8–10 and 14 block is identical to merged main. The resulting audit is exactly main plus the approved chapters 6–7 insertion and the accurate change from “Chapters 8–10” to “Chapters 6–10” in Remaining audit work. Headers, order, individual snapshot notes and the open broader objective are preserved, with no loss or duplication. README is exactly main plus the approved chapters 6–7 clause, retaining the chapters 8–10 and Chapter 14 clauses.

Both-manual impact remains valid: the two approved Operator’s Manual additions are preserved exactly; the other manual changes come from main and the replay reports no differences there. No procedure, executable example, role or handoff is changed by this resolution, so no Agent Operator’s Manual edit is needed. Beyond those two approved manual additions and two results files, the tree equals merged main. git diff --check passes. This review covers the resolution and preservation of existing review, not a fresh source audit or rendered-manual approval.

CI at review: check-title passed; HTTP cache origin, ci-checks and the manual PDF build are pending. ci-checks has not finished, so final advisory notices are unavailable and have not been reviewed. No Lean builds were run. No queueing or merging, as explicitly instructed; this verdict does not assert completed CI.

[chris-ai1]

Final technical validation is clear at f39e5afed6685b199dc4d0bb019d8f48c7e18b4d. Native CI passes all six gates and stock/tidy/registry/source checks. Its actual tested merge df75ed626f7753c7610f9ef92a6f7c11688e8c26 preserves every reviewed PR-owned documentation blob exactly. All three complete advisory reports state no eligible changed library file/definition/theorem; no semantic absence/uniqueness claim follows from this documentation-only scope.

Independent merge-resolution approval retains the full source review and the correction of 7.12. The corrected Partial classification, disposition counts and source limits remain intact; this clearance adds no new mathematical coverage claim.

Verified current manual artifact 13978893083: exact clean revision, all 72 Operator chapters plus the Agent chapter, converter/figure inputs, bibliography and both PDF hashes match committed inputs. Operator PDF148/209 (printed140/201) show both approved audit routes readably and preserve model/uniformity/weak-gap qualifications; exact-head links resolve. Agent content is unchanged with verified provenance. No local full rebuild of omitted artifact intermediates is claimed. No Guide workflow is selected for these paths.

A non-author may now queue exactly this revision under the coordinator’s integration plan. #4711 and the formalization objectives remain open. Validation/coordination: Codex /root, session sol-coord-20261112, thread 8d548603-e952-4ccb-9777-18a092187051; this is not an additional independent source approval or human review.

[chris-ai1]

Non-author integration clearance for f39e5afed6685b199dc4d0bb019d8f48c7e18b4d — Codex review session /root, 2026-11-12. I did not implement or design this change. I retain the corrected source review and exact-head merge-resolution approval, including both-manual assessments.

Read current PR/issue comments, current-main queue policy and live checks: no outstanding human/global hold or conflict found. Earlier no-queue instructions limited those review tasks; the current integration request authorizes queueing. All six native CI gates pass; I read the three actual advisory reports, each with no eligible changed library files/declarations. The final technical/manual evidence records the tested-merge blob identity and rendered artifact provenance; those review holds are resolved. This adds no fresh source audit or mathematical coverage claim. Queueing this exact head once using the trusted current-main helper; the parent coordinator owns landing monitoring and subsequent restacking. Agent integration review, not human approval.