[chris-ai1]

Part of #4772. Audits Goldreich’s draft chapters 5–7 against origin/main snapshot e39c34b3413b2cd7e08053a14ff8bb36ded4c8dc (CSLib ee99dd30bd1a9f466c25a51b39a5cb0bfe4d2342). Chapter 7 uses the later March revision r4.pdf, not the overlapping r3.pdf. This is documentation progress only; no missing theorem is implemented and the book-wide objective remains open.

The inventory contains 47 main numbered results and six proof-internal claims, rather than the initial approximate count. A separate PDF glyph-span scan recovered Proposition 6.33. Every row has file/PDF/printed locators, declaration/module evidence or a qualified negative search, and relevant model/resource limits. Internal claims remain traceability records rather than independent research objectives.

Chapter	Covered	Partial	Endpoint not located	Source issue	Unverified
5	5	5	3	0	0
6	4	10	4	1	0
7	3	17	0	1	0
Total	12	32	7	2	0

“Partial” includes existing mathematics whose exact source interface or parameter transport was not established. It is not a claim that all 32 rows require new proofs. In particular, the exponential worst-case/average-case endpoint 7.19 is established by the existing reconstruction schedule and E-membership theorem; it does not certify the draft’s separate derandomized-XOR lemmas.

Proposed development issues — not created

Open and closed issue searches checked endpoint names and related terms, and the proposals in Arora–Barak audit PRs #4764, #4766–#4770 were cross-checked. These proposals are for coordinator deduplication, not implementation claims.

1. PromiseBPP to PromiseCoRP by one-sided randomized Karp reduction. Theorem 6.9, r3 PDF 13 / printed 215. For every PromiseBPP problem, construct a PromiseCoRP problem and a polynomial-time randomized many-one reduction which always maps no-instances to no-instances and maps yes-instances correctly with bounded probability. State off-promise behavior and error orientation explicitly. Dependencies: existing promise PPT characterization, amplification and covering/shift machinery. Searches found promise reduction infrastructure and metacomplexity applications (Hirahara FOCS'22: partial MCSP is NP-hard under randomized reductions (#798 M3.5/M3.6) #4362/feat(MCSP): Ilango–Loff–Oliveira — Multi-MCSP is NP-hard under randomized reductions (#798 M3) #4405/Hirahara FOCS'22: MINKT* (partial-string MINKT) is NP-hard under randomized reductions (#798 M1/M3) #4447), not this general endpoint; plan(complexity-readability): uniform class APIs, general lemmas out of applications, in Computability/Complexity (Jetski coordinator 33f8) #4737 concerns API readability, and total-language Sipser–Lautemann is a different contract.

2. Native NP-oracle approximate counting. Theorem 6.27, r3 PDF 33 / printed 235. For every polynomially balanced polynomial-time relation, construct a randomized polynomial-time NP-oracle relative counter with inverse-polynomial relative error and negligible failure. Dependencies: existing finite relative affine-hash guarantee, encoded witness predicates and NP queries, median/threshold schedules and binary arithmetic. A useful first milestone is the generic additive estimator in Proposition 6.23 (r3 PDF 31 / printed 233), with its actual sampler and rational-output costs. ROADMAP retains the oracle-algorithm form of Stockmeyer; searches found no dedicated owning issue. The finite probability theorem already exists and must be reused. Toda’s oracle containment and its doc(results): audit Arora–Barak chapters 8–10 #4769 proposals do not certify this algorithm.

3. PC search-relation transport to existing counting/isolation/sampling APIs. Theorems 6.18, 6.29 and 6.31, r3 PDF 22, 37, 41 / printed 224, 239, 243. Fix explicit polynomial balance, witness encodings and solution-bijection reductions; prove count-hardness transfer, general complete-relation search isolation, and the bridge from strong parsimonious prefix reductions to a usable self-reduction interface. Dependencies: parsimonious Cook–Levin, the existing SAT isolation reduction, witness reconstruction and FPAUS/FPRAS machinery. Keep the fixed-accuracy oracle constants of 6.31 as a separately stated refinement. JVV: almost-uniform sampling implies FPRAS for self-reducible relations (FPAUS interface) #3039 owns a concrete one-bit self-reducible sampling-to-counting milestone, not this general relation transport; doc(results): audit Arora–Barak chapters 8–10 #4769’s exact Valiant–Vazirani success constant is also distinct. No owner of this general interface was located. Split implementation milestones along these independently useful transports rather than replacing the existing theorems.

4. Exact conditional uniform generation with an NP oracle. Proposition 6.33 and Construction 6.32, r3 PDF 45–47 / printed 247–249; proposition on PDF 46 / printed 248. For any PC relation, produce either a witness or failure, with exactly uniform successful output and inverse-polynomial success, using certified polynomially many charged NP queries. Dependencies: efficient sufficiently independent hashing, NP tests for oversized cells, sorted witness enumeration/recovery and a supplied or computed count-scale estimate. Specify a realizable fair-bit rejection step, using dyadic probabilities if strict polynomial time is required. Existing FPAUS/ExactSampler uses exact counts for its exact PMF sampler; its capped NP-oracle-independent interface is approximate. Neither JVV: almost-uniform sampling implies FPRAS for self-reducible relations (FPAUS interface) #3039 nor its inspected scope owns this general exact-conditional NP-oracle theorem; no dedicated owner was found.

5. A #P-complete count with polynomial-time search: DNF. Theorem 6.19, r3 PDF 23 / printed 225. Prove exact DNF counting is #P-hard under polynomial-time counting/oracle reductions (e.g. via the complement of CNF counts), and supply a polynomial-time procedure finding a satisfying DNF assignment or correctly reporting none. Dependencies: existing SharpSAT completeness, a variable-universe-preserving CNF/DNF complement translation, power-of-two totals and binary subtraction; existing KLM approximation is reused. Karp–Luby–Madras FPRAS for #DNF and an FPRAS interface #2858 owns the FPRAS, not exact-count hardness or this search/count contrast. No dedicated owner was found; do not accidentally demand parsimonious hardness.

Other gaps should be offered to existing owners/proposals first: #459/#1444 for classical cover time and random-walk USTCON; #4224 for circuit uniformity; #2865’s explicitly retained OWF bridge for solved-instance generation (7.2); #3557 for set hard-core rounding. Deduplicate permanent counting (6.20–6.22) with #4769, the separate expected-time ZPP alternative-definition bridge with #4767, and general-hardness schedules/sharp XOR tradeoffs with #4768. The arbitrary-ensemble hard-region and correlated-generator auxiliaries need further scoping alongside those amplification proposals; they are not silently declared complete by the existing final endpoint. No new issue is proposed for the proof-specific global-tape model solely to reproduce an alternative proof of an already covered endpoint.

Source issues

• 6.5, r3 PDF 10 / printed 212: the explanatory oracle contract below the proposition requires a root r < s/2; for prime P=5 and residue s=1 the roots are 1 and 4. The construction’s smaller-root convention is bounded by P/2. This is a defect in the accompanying specification, not a counterexample to the intended primality reduction.
• 7.18, r4 PDF 31 / printed 295: injectivity of m does not define its inverse on every input length. The displayed example ell(N)=N³ gives m(n)=3n, leaving lengths 3k+1 undefined. State padding/off-image extension and its hardness transfer.

A future checked client could verify these two finite/root and length examples and the correlation-versus-agreement rescaling used for 7.19; no client files were added under the shared no-build brief.

Validation and manual impact

Passed python3 -B scripts/check_operator_manual.py, python3 -B scripts/check_hygiene.py, git diff --check, the 53-row/disposition count and local source-link checks. No Lean builds, cache downloads or new client tests were run, as required by the shared-host brief. Six ambiguous source pages were rendered and inspected; a separate glyph-layout scan checked result-label line starts across the chapter PDF ranges. The audit records these limits rather than claiming full visual or semantic completeness.

The Operator’s Manual adds a route from “Find and apply a result” to the audit’s model boundaries and distinguishes Goldreich’s bounded partial-answer ZPP from the separate expected-time interface. Chapter 5 explicitly discloses native visited cells and Goldreich’s scanned-cell convention; fixed alphabet/control factors preserve asymptotic bounds, while exact bounds remain qualified. The results inventory links the new audit using the shared wording. The Agent Operator’s Manual was assessed: no edit is needed because roles, authority, review and handoff procedures are unchanged. ROADMAP, upstream markers and coordination threads need no edits: this audit implements no endpoint or dependency change and leaves all development proposals for deduplication.

Coordinator review requested for the source inventory/locators, statement mappings, source issues, proposed ownership and both-manual impact. Independent review remains pending; the worker does not approve or merge this PR.

Prepared for Christian Reitwiessner with Codex assistance for source research, repository/issue searches and documentation. Worker session t3-33154868, branch t3/goldreich-chapters-5-7-audit.

[chris-ai1]

Changes requested on head 1346569ca29b68dcb7b4354e45dc00fbac3aeff3.

Reviewer identity: this T3 delegated-task session, independent review worker review4776-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 or platform approval. The PR author and reviewer use the same GitHub account, so this COMMENT review records the verdict.

Two source mappings need correction: 5.6 identifies whole-graph connectivity with designated-vertex reachability, and 6.10 incorrectly attributes the expected-time definition to the draft's primary ZPP theorem. Inline comments give the source locators and fixes. Also disclose the native visited-cell convention explicitly and remove the blank line that detaches 6.33 from its table. Update counts and the PR/manual wording as appropriate.

Sampling-plus-risk scope: an independent baseline/glyph scan of r2 pages 39–84, r3 pages 1–64 and the later r4 pages 1–50 recovered exactly the table's 53 distinct result labels (47 main results and six internal claims). I checked all 12 Covered rows against the cited Lean statements and source pages, plus both Source issue rows. Partial sampling covered 5.1–5.3, 5.5, 6.3, 6.9–6.10, 6.15, 6.27, 6.31, 6.33 and 7.8 (12/32); negative sampling covered 5.7, 5.9, 5.10 and 6.13 (4/7), including targeted source searches and the difference between global/local oracle storage and ordinary composition. These searches are not a proof of absence. No Lean builds, new checked clients or whole-proof/axiom audit were performed.

The two source defects are genuine as written, verified on rendered pages: r3 PDF 10 / printed 212 really specifies r < s/2 below 6.5; at P=5,s=1 the roots 1 and 4 violate it. This is an accompanying oracle-specification typo, not a disproof of the intended reduction. r4 PDF 31 / printed 295 uses m inverse at arbitrary string lengths despite assuming only injectivity; its ell(N)=N³ example gives m(n)=3n, leaving other lengths undefined. Off-image extension and eventual-hardness transport are necessary. The later r4 revision is consistently used for chapter 7.

The remaining checked positive mappings are appropriately limited: native completeness/space theorems keep their encodings and logarithmic-domination hypotheses; Schwartz–Zippel requires a nonzero formal polynomial; Toda uses a #P bit oracle; DNF approximation includes zero counts; OWF amplification and padded Goldreich–Levin are uniform PPT claims. For 7.19 I checked the eventual exponential schedule, E-membership theorem and agreement convention: reducing the exponent provides slack for the factor-two correlation conversion. This does not certify the alternative derandomized-XOR auxiliaries.

I checked the five proposals against open/closed issue searches and the proposal bodies in #4764 and #4766–#4770. No additional duplicate owner was located for those five bounded interfaces. In particular #3039 covers the one-bit self-reducible sampling-to-counting milestone, #2858 the DNF FPRAS, and #4362/#4405/#4447 metacomplexity reductions, rather than the proposed generic contracts. The existing deduplication of permanent work with #4769 and general-hardness/XOR work with #4768 is appropriate. The expected-time bridge in #4767 is a separate alternative-definition objective, not a reason to mark Goldreich 6.10 Partial.

The shared header is verbatim, the README bullet is present, mathematical delimiters are dollar-only, and negative searches are qualified. Both-manual assessment: I followed the Operator's Manual README/task route to finding-results and the new audit link. The route is useful, but its expected-time warning should distinguish the alternative interface from the covered source definition after the correction. I inspected the Agent Operator's Manual: no edit is needed because this documentation audit changes no roles, authority or handoff procedure. No ROADMAP, upstream marker or coordination-thread status update is needed for this audit-only milestone. Rendered-manual review remains outstanding while its build is pending.

CI at review: gh pr checks 4776 reports check-title and HTTP cache origin passed; ci-checks (run 43282245541) and the manual build (run 43282245559) remain pending. There is therefore no completed ci-checks advisory log to inspect yet. No sibling add/add conflicts are counted as findings. No queueing or merging, as explicitly instructed.

[chris-ai1]

The source endpoint is whole-graph connectivity, not the designated-vertex problem claimed here. The paragraph immediately before 5.6 (r2 PDF 53 / printed 169) defines the task as deciding whether a given graph is connected. The end of the proof (PDF 60 / printed 176) discusses testing a given pair separately. USTCON_mem_L proves the latter. Please correct the source description and either map a native whole-graph connectivity theorem/explicit encoded iteration bridge (including the empty-graph convention), or mark the missing interface Partial. Mathematical equivalence alone does not identify the cited Lean contract.

[chris-ai1]

The claimed source-definition mismatch is incorrect. Rendered r3 PDF 17 / printed 219 defines ZPP immediately above 6.10 by a polynomial-time algorithm returning the correct answer or failure, with success at least 1/2. This matches DecidesWithZeroError and ZPP_eq_RP_inter_coRP. PDF 18 / printed 220 introduces expected polynomial time only as an alternative used in some sources and explicitly distinguishes it from the definition used here. Please mark 6.10 Covered in the bounded partial-answer convention, retain the expected-time bridge only as a separate alternative-definition qualification, and update counts/PR/manual wording accordingly.

[chris-ai1]

Please make the space comparison explicit here and refer the space rows to it: the native RunPath.space sums distinct work-head positions visited (including blank, initial and final cells); input/output are excluded and finite control is not charged. Rendered r2 PDF 41 / printed 157 defines Goldreich's binary space from scanned work cells, weighted by log alphabet size, and additionally charges finite control. Unlike the Arora–Barak ever-nonblank convention in #4766, Goldreich already uses scanned cells, so that review's blanket downgrade does not apply. Explain why fixed-alphabet/control factors disappear for asymptotic classes but prevent exact coefficient-one comparisons in 5.1–5.3. “Native” and “constants” alone leave the actual measure implicit.

[chris-ai1]

Remove the blank line before this row. It terminates the preceding Markdown table, leaving 6.33 as an isolated pipe-delimited paragraph without a table header/separator. The result is counted by the inventory script but does not render as a row of the chapter table.

[chris-ai1]

Fixed in cc0c206 (new commit, no force-push).

• 5.6 is now Partial: the draft defines whole-graph connectivity, while USTCON_mem_L decides designated-vertex reachability. The whole-graph iteration/encoding bridge, including the empty-graph convention, remains unmapped.
• 6.10 is Covered: r3 PDF 17 defines bounded-time correct-or-failure algorithms with success at least one half, matching DecidesWithZeroError. Expected time is only the alternative definition on PDF 18. The manual pointer and PR wording now distinguish these.
• Chapter 5 and its space rows explicitly disclose visited cells, including blank/initial/final positions and excluding input/output and finite control. Rechecked r2 PDF 41: unlike Arora–Barak, Goldreich counts scanned cells, then weights the fixed alphabet and charges control. The asymptotic cell measures therefore agree; 5.4, 5.11, 5.12, 5.14 and 5.15 retain Covered with that justification, while exact 5.1–5.3 remain Partial. The scope also states the doc(results): audit Arora–Barak chapters 1–5 #4766 direction rule: ever-nonblank cells are a subset of visited cells, so membership upper bounds transfer, but reverse-direction arguments require a bridge. Re-reading the same source also corrected 5.5’s local uniformity description to polynomial time and linear space in the local query encoding.
• Removed the blank line before 6.33, restoring the continuous table.

All 53 labels and both source defects remain. Chapter 5 is now 5 Covered / 5 Partial / 3 Endpoint not located; chapter 6 is 4 Covered / 10 Partial / 4 Endpoint not located / 1 Source issue. Overall totals remain 12 Covered / 32 Partial / 7 Endpoint not located / 2 Source issue. Proposals are unchanged; PR summary updated.

Manual checker, hygiene, local source links, row counts and git diff --check pass. No Lean builds. Both-manual assessment: Operator pointer corrected; Agent Operator instructions unchanged because no workflow changes. Please re-review this documentation delta; no independent approval is claimed for the new head.

[chris-ai1]

Approved on exact head cc0c206f88e8ad9c1e38edc2038ed73994aaa14a: all four findings from the earlier review are resolved; no new blocking findings in delta 1346569ca..cc0c206f.

Reviewer identity: this T3 delegated-task session, independent review worker review4776-delta-20261112. I did not author, implement or design this change and reviewed the source and evidence in a separate context. This COMMENT review records independent agent approval on the shared account, not human or platform approval.

I inspected the rendered draft pages r2 PDF 41, 53–54 and r3 PDF 17–18 against the cited Lean definitions. Row 5.6 is correctly Partial: whole-graph connectivity is distinct from USTCON designated-vertex reachability, including the empty-graph encoding gap. Row 6.10 is correctly Covered: bounded polynomial-time correct-or-failure answers with success at least one half match DecidesWithZeroError and ZPP_eq_RP_inter_coRP; expected time is a separate alternative definition. The incidental 5.5 correction also matches the rendered source’s polynomial-time/linear-space local-query interface.

The space disclosure matches pinned CSLib RunPath.visitedByTapeHead / spaceUsedByTape / space and the local VisitedInterval invariant: work-head positions, including blank cells and endpoints, are counted; input/output and finite control are excluded. Goldreich counts scanned work cells with fixed alphabet/control costs, so the stated asymptotic comparisons are justified. Ever-nonblank cells are a subset of visited cells on blank-initialized tapes, allowing membership upper bounds to transfer; reverse-direction simulations/equalities remain Partial without a bridge unless the measures coincide. Exact binary-space bounds remain qualified.

The table is continuous through 6.33. Recounted all 53 rows: chapter 5 is 5 Covered / 5 Partial / 3 Endpoint not located; chapter 6 is 4 / 10 / 4 / 1 Source issue; chapter 7 is 3 / 17 / 0 / 1. Overall 12 / 32 / 7 / 2 agrees with the PR summary. Only the audit and its Operator’s Manual pointer changed in this delta; the remaining earlier review coverage is reused. Both-manual assessment: the corrected finding-results route accurately distinguishes the ZPP interfaces and resource limits; no Agent Operator’s Manual edit is needed because roles, authority and handoff procedures are unchanged. No Lean source, upstream marker, ROADMAP objective or coordination status changed. git diff --check passes. No Lean builds or new checked clients were run.

CI at review: check-title passed; HTTP cache origin, ci-checks (run 43283493806), and manual build (run 43283493861) are pending. There is no completed ci-checks advisory log yet. Approval covers the documentation delta; required CI/advisory inspection and affected rendered-manual inspection remain integration holds. No queueing or merging, as explicitly instructed by the user.

[chris-ai1]

Coordinator integration record at cc0c206f88e8ad9c1e38edc2038ed73994aaa14a:

• Independent reviews, both by non-author T3 delegated-task sessions that did not author, implement or design the change and reviewed in separate contexts:
  • Full review at 1346569ca: session node:delegated-task:command:mcp:209b45c0-6ec8-4d3a-9adb-bbb62207cefe:delegate-task:4c9a02e3-705a-43d4-b3c3-a014a337611d, changes requested on four items. It confirmed all 53 labels and both source defects.
  • Delta review of this exact head: session …delegate-task:933b808b-899a-49fd-bf1f-5bcad9e22faa, APPROVE, with all four findings resolved.
  • The PR's author was a different session: …delegate-task:2f571c7b-44c7-4ac3-8815-b93acb3dfcd8.
• CI: Lean CI 43283493806 passed.
• Advisory notices (read): no CslibFrontier/ file, definition or theorem is added or modified (documentation-only PR).
• Rendered manual: in the PDF artifact, the new Goldreich-audit paragraph in finding-results.md (PDF p. 79) renders cleanly.
• Integration check: a replay of the current full queue prefix, built with real merge commits, followed by this PR is clean.

This PR creates results/goldreich-2007.md, so the sibling Goldreich audit PRs (#4775, #4777, #4779) will be restacked onto it one at a time after it lands, each with a bounded non-author check of the joined sections.

Queueing.