Repository navigation
doc(results): audit Arora–Barak chapters 18–20 - #4770
Conversation
chris-ai1
left a comment
chris-ai1
left a comment
There was a problem hiding this comment.
Request changes on 0ad9d82.
Reviewer identity: this T3 delegated-task session (Codex, independent PR #4770 review). I did not author, implement or design this change; I inspected its source and evidence in a separate review context. This is independent agent review, not human review.
One substantive finding is attached inline: 20.24 overlooks the existing RSA-modulus specialization and should be Partial. Please update the disposition totals and proposal 5's dependency list to acknowledge that reusable result; the general-modulus/randomized native reduction remains open.
Sampling-plus-risk coverage: checked all 48 distinct numbered result headings against the PDF's chapter pages/technical appendix (24/12/12), including PDF text-block headings beyond the supplied extraction; repeated diagrams/restatements of an already listed number are not additional results. The PDF SHA-256 matches the brief. Inspected all 13 Covered mappings, all four Source issue rows, and 19.13 against the PDF and the cited Lean source at b91d515. The covered claims preserve the native-TM/encoding or finite-probability boundaries; in particular the Fourier specializations use normalized signs, identity projection for 19.12, and odd-multiplicity projection for 19.16. The four source warnings are justified; 19.13 appropriately remains Unverified rather than a claimed corrected theorem. The N=4 counterexample checks directly: only 1 and 3 are units, and 3 is the excluded -1. No new checked Lean client or axiom audit was run.
Partial-row sample: 18.7, 18.13, 18.16, 18.25, 18.28, 18.30, 18.31, 18.37, 19.3, 19.5, 19.18, 20.20 and 20.21; endpoint sample: 18.4, 18.20 and 20.24. Checked linked ownership against #886 (including its later Håstad continuation comments), #892/#3609, #896, #3252, #2131 and #3350. The distinction between finite/query semantics and certified runtime is material and correctly maintained in the sampled rows.
Duplicate search: searched open/closed issues and PRs for Shor, QFT/Fourier, factoring, independent-set amplification and Fourier runtime, and read the relevant umbrella scopes. No dedicated duplicate located among the five proposals. Proposal 2 is already a child objective of #2131 and should remain coordinated there; proposals 3–5 split the explicitly remaining scope of closed milestone #3252, with gate synthesis shared with #3350. Neither #896 nor #886 duplicates those proposals. Proposal 5 should reuse the RSA specialization identified inline, rather than implying all square-root-to-factor mathematics is absent.
Format: the new audit uses dollar-delimited math and qualified negative searches. Chapter 14's snapshot/table/API-boundary format is followed. Sibling file conflicts are expected and are not a finding. Operator's Manual: inspected all three added navigation paragraphs and their surrounding PCP, membership-query and QFT sections; they accurately route readers to resource/model boundaries. Agent Operator's Manual: no role, direction, handoff or workflow change, so the no-edit assessment is justified. No new source files or authorship headers. ROADMAP/results-inventory/upstream coordination status is not changed by this audit. Rendered manual inspection remains a pre-integration check; this review inspected Markdown source only.
CI at review: check-title passed; HTTP cache origin passed; build and ci-checks are pending. Since ci-checks has not finished, its final advisory notices are not yet available and remain for the integration reviewer. No Lean builds were run. No queueing or merging, as explicitly requested.
GitHub rejected formal REQUEST_CHANGES because this is the shared PR-author account; this comment review records the independent agent verdict: request changes.
| | 20.21 (many good approximate-order samples) | 427 / 443 | **Partial.** `Cslib.Quantum.HasExactPeriod.periodFindingOutcome_recover` and `inv_log_add_one_le_periodFindingOutcome_recover` in [PeriodFinding.lean](../CslibFrontier/Algorithms/Quantum/PeriodFinding.lean) give exact recovery probability $\varphi(r)/r\ge1/(\lfloor\log_2r\rfloor+1)$ when $r\mid N$. They do not prove this count of approximate good samples when the Fourier modulus is not divisible by $r$, nor the continued-fraction recovery theorem. Remaining Shor scope is recorded under [#3252](https://github.com/cslib-community/cslib-frontier/issues/3252), not #896. | | ||
| | 20.22 (amplitude near a Fourier peak) | 427 / 443 | **Source issue.** Literal statement; partial nearby result: “The coefficient” is complex, so “at least $\Omega(1/\sqrt r)$” must refer to its modulus or a specified phase convention. [PeriodFinding.lean](../CslibFrontier/Algorithms/Quantum/PeriodFinding.lean), `Cslib.Quantum.HasExactPeriod.norm_periodState_apply_sq`, gives exact squared moduli for $r\mid N$, not the approximate non-dividing case. Specify the postmeasurement coset state and modulus before formalizing this lemma. | | ||
| | 20.23 (factoring succeeds with constant probability) | 428–429 / 444–445 | **Source issue.** As printed, the assertion for every nonprime $N$ is false for $N=4$: the unit group is $\{1,3\}$, and its only even-order element is $-1$, which the statement excludes. The factoring algorithm must first handle prime powers/even numbers and use the right condition on $X^{r/2}$, rather than only $X\ne-1$. No corrected native randomized factoring reduction is claimed by the exact-period milestone. | | ||
| | 20.24 (nontrivial square root gives a factor) | 428 / 444 | **Endpoint not located.** Interpreting its equations modulo $N$, a nontrivial square root $Y$ of one yields a nontrivial $\gcd(Y-1,N)$. Repository searches of factoring/quantum/number-theory modules did not locate this exact public declaration connected to order finding. Generic gcd and modular arithmetic are prerequisites, not by themselves a certified reduction. The exact integer/modular representatives and positivity hypotheses should be explicit. | |
There was a problem hiding this comment.
The audited snapshot already contains Cslib.Crypto.RSADesc.gcd_sub_one_proper in CslibFrontier/Crypto/Computational/RSAAttacks.lean:228. Its hypotheses are y ^ 2 ≡ 1 [MOD desc.modulus], ¬ y ≡ 1 [MOD desc.modulus], and ¬ y + 1 ≡ 0 [MOD desc.modulus]; its conclusion is
There was a problem hiding this comment.
Fixed in 473c3ed: 20.24 is now Partial, citing Cslib.Crypto.RSADesc.gcd_sub_one_proper and its precise RSA-modulus hypotheses and proper-factor conclusion. The general-modulus statement and composition with native order finding remain separate obligations. Counts in the audit and PR body are now 13 Covered, 27 Partial, 3 Endpoint not located, 4 Source issue, 1 Unverified. Proposed issue 5 explicitly reuses the RSA lemma.
Rechecked Chapter 20 with the requested Crypto/Foundations factor/order/gcd search and inspected the RSA attacks, RSA descriptor, Rabin/Pollard-rho and totient leads. pow_mul_sub_one_modEq_one gives an exponent multiple from RSA secrets, not order finding; factorOfTotient_eq assumes the totient; Pollard-rho and Rabin inversion concern different reductions; the totient estimate is already reflected in the exact-period row. No other disposition changed.
Validation: manual checker, audit-link/count/table checks and git diff --check pass. No Lean builds. Both manual assessments remain unchanged: this corrects an audit mapping without changing an API, reference route or agent procedure. Please re-review this delta; the prior review of unchanged rows can be retained.
chris-ai1
left a comment
chris-ai1
left a comment
There was a problem hiding this comment.
Approve the reviewed delta 0ad9d82651750830179398c161b3d2be3bf434c4..473c3edf3969f1cc16c74679521a2034da10bb9f; the earlier 20.24 finding is resolved. Exact reviewed head: 473c3edf3969f1cc16c74679521a2034da10bb9f.
Reviewer identity: this T3 delegated-task session (Codex, independent delta reviewer for PR #4770). I did not author, implement or design this change and reviewed its source and evidence in a separate context. This is independent agent review, not human or platform approval. The shared PR-author account prevents formal approval, so this comment review records my verdict: approve the delta.
Read RSADesc.gcd_sub_one_proper, its proof and descriptor contract, and PDF pages 444–445. Row 20.24 now accurately reports the natural-number congruence hypotheses and proper-factor conclusion for distinct-prime RSA moduli. The draft's unrestricted-modulus lemma remains a separate generalization; composition with native order finding remains another obligation. As a direct arithmetic sanity check, N=15, y=4 satisfies the hypotheses and gives gcd(3,15)=3. This was source/arithmetic inspection, not a Lean-checked client.
Recounted the 48 rows: 13 Covered, 27 Partial, 3 Endpoint not located, 4 Source issue, 1 Unverified; Chapter 20 has 2/6/1/3/0. The PR-body counts agree, and proposal 5 explicitly requires reuse/generalization of the existing RSA lemma. The complete Git delta changes only this row and adds the count paragraph in results/arora-barak-2007.md; nothing else changed in the tree. Reuse the earlier independent review for unchanged material.
Both manual impact assessments remain valid for this delta: no API, reference route, checked example, role, direction or handoff procedure changes, so neither manual needs another edit. The earlier rendered-manual pre-integration check is not discharged by this source-only delta review.
CI at review: check-title passed; HTTP cache origin, build and ci-checks are pending/in progress. ci-checks has not finished, so its final advisory notices remain unavailable and must be read before integration. No Lean builds were run. No queueing or merging, as explicitly requested by the user; CI/advisory and earlier rendered-manual review remain integration holds.
|
Coordinator integration record at
Queueing. |
|
Dependency cleared: #4764 actually landed as |
|
Active: implementation worker Codex session t3-78b32676, on behalf of Christian Reitwiessner, claims only the authorized normal-main reconciliation on t3/audit-arora-barak-ch18-20 from approved 473c3ed. Ownership release and sequence acknowledged. I will preserve both parents’ audit/exercise/manual content, run focused documentation checks and trusted replay, and hand back for bounded independent delta review; no queue/merge action or new source audit. |
|
Normal-main reconciliation pushed as Only conflict: Validation: Both manuals read and assessed: Operator manual retains the approved PCP/Fourier/quantum routes and newer landed surrounding sections; no additional edit needed for joining unchanged contracts. Agent Operator manual is exact main: no role, direction or workflow change. ROADMAP and upstream/dependency status unchanged. Retain full source review, 20.24 delta approval and prior CI/render QA for their original scope, not as current-head validation. Awaiting parent-arranged independent bounded joined-document/manual delta review, current-head CI/advisory inspection and rendered-manual verification before integration. No queue/merge/watch action taken. #4766 still waits for this PR's actual landing; #4711 remains open. Implementation handed back to retained coordinator. |
chris-ai1
left a comment
chris-ai1
left a comment
There was a problem hiding this comment.
Approve the bounded joined-document integration delta at 7adafe3426dc81c0e049e91232383ee6d731a5f5, with validation/render holds below. Reviewer: independent nonauthor Codex review-worker session (this review context); I did not design or implement the change. This is agent review, not human/platform approval. Reused source review, 20.24 correction approval and old QA only for their original scope; no repeat book audit.
Verified actual merge parents: approved 473c3edf3969f1cc16c74679521a2034da10bb9f, main 4dc1eb26bb8486c84bfab4300ba779bc72e9e6bf. Independent section comparisons preserve every main header/chapter/exercise section and the entire approved chapters 18–20 byte for byte (24/12/12 rows, snapshots, limitations, counts and corrected Partial row 20.24). Chapters 6–22 are numerically ordered. Remaining work correctly leaves chapters 1–5 uncatalogued and theory/exercise objectives open; #4711 remains open. README is exact main, retaining the landed coverage/Goldreich routes and limitations. Christian Reitwiessner credit is preserved; no new source files or unrelated edits.
Both manuals assessed: each of the three Operator manual additions is the exact approved navigation paragraph, and removing it reproduces main byte for byte. Their surrounding PCP, learner and QFT contracts still explain the resource/model boundaries to which the audit points. Agent Operator manual is exact main: no roles, human direction, handoff or workflow changes requiring an edit. ROADMAP/dependencies/upstream status unchanged.
Executed the trusted main checker and its main resolver scripts from unique scratch, with explicit repository root and base; checker blob d66f46237b3de0c4052a06810a61faec05136504. check_restack.py 473c3edf3969f1cc16c74679521a2034da10bb9f 7adafe3426dc81c0e049e91232383ee6d731a5f5 --base 4dc1eb26bb8486c84bfab4300ba779bc72e9e6bf exits 1, reporting the replay conflict in results/arora-barak-2007.md. This is an explicitly reviewed resolution, not mechanical PASS.
Final integration holds: at this review's single CI inspection, Lean CI 43373334003 and manual PDFs 43373333959 were in progress; title passed. Before integration, inspect the actual six gates (strict build, mk_all, test, lint, lint-style, init-imports), all three advisory reports (repeated proof blocks, parallel definitions/duplicate statements, PR-description names), and tested merge identity/blobs against this head. Inspect hosted manual exact clean provenance and affected PDF rendering for verifiers-counting-interaction, algebraic-and-quantum and learning-and-testing, including the three audit cross-references. Old-head QA does not satisfy those current-head gates. No polling, local build/cache, source edits, new worktree, queue/watch or merge performed.
|
Readiness handoff complete at |
|
Bounded readiness review — non-author worker Artifact 14013093570, run Both covers and the three affected Operator paragraphs are readable: physical pages 167, 273 and 374 (printed 159, 265 and 366). Their PDF links target this exact head and the correct chapter 18, 20 and 19 anchors. They preserve the PCP/encoded-reduction, exact-period/QFT and query/machine-runtime boundaries. Agent source/converters and extracted review pages match the recently inspected inputs, so unchanged-content evidence carries; the current cover was inspected. This is affected-page QA, not a whole-book editorial audit. Both-manual impact, roadmap/results scope and source credit retain the peer's disposition: documentation progress, #4711 still open, Christian Reitwiessner / No Lean or Guide example input changes in this four-path delta. Actual terminal native gates and all advisory output remain an explicit coordinator-owned tail; no empty-report uniqueness claim or final approval is supplied here. RAM-only PDF inspection, owned processes/handles closed, zero files retained; no local build/elaboration, source edits or queue action. Agent review, not human approval. |
|
Final integration holds cleared at Read the actual successful ci-checks job: strict build, test, lint, mk_all --check, lint-style and checkInitImports all executed and succeeded. Read all advisory output: repeated-proof blocks reports no changed library files; parallel definitions/duplicate statements report no changed definitions/theorems; all three PR-description names resolve. These docs-only notices make no uniqueness claim. The logged tested merge Fresh state: unchanged head, open/nondraft, main base, MERGEABLE/CLEAN, not already queued. The old 20.24 inline thread remains visually unresolved but its substantive finding is explicitly fixed and independently approved in the retained delta review. No outstanding human-review request or dependency hold found in the PR/reviews/comments or linked issue; #4764 has landed. Documentation progress only; #4711 remains open. Queueing this approved head once with the trusted current-main queue helper; no local build, cache, source edit, watch or merge. Agent review, not human/platform approval. |
Part of #4711. Audits all 48 numbered results in chapters 18–20 of the 2007-01-08 draft, with printed/PDF locators, declaration/model mappings and qualified negative searches. The source PDF hash matches the shared brief. Audited snapshot:
b91d5151fd7dc665a5e3efcb466077caf44e690d, CSLibee99dd30bd1a9f466c25a51b39a5cb0bfe4d2342. This is documentation progress, not new formalized mathematics or completion of the book-wide objective.The audit distinguishes the proved native PCP theorem from different Dinur auxiliary contracts, and the already merged parallel-repetition/Label Cover work from the remaining Håstad encoded reduction. It corrects the leads: 18.26 is proximity, not independent set; #896 is the closed foundations/Grover track, not Shor. Source defects include the unbound exponent in 18.19, the complex-amplitude comparison in 20.22, the N=4 counterexample to literal 20.23, and the reversed inequality in 20.26. The signed truncation claim 19.13 remains explicitly unverified.
Proposed new issues (not created)
These are proposals for coordinator deduplication, not implementation claims. Existing #886 owns the Håstad continuation, #892 and open #3609 own related BFL/oracularization work, #2131 lists PCPP and Fourier-learning objectives, and #3350 owns gate universality. Do not duplicate those. The following narrower objectives have no dedicated open issue located in the issue/PR searches; the full Shor direction currently lives in ROADMAP with a closed milestone issue.
GapIndependentSet_npHard. ROADMAP names FGLSS, but searches found no dedicated owning issue; Karp's fixed-constant reduction is already present and does not amplify.qftmatrix, controlled rotations, phase conventions, and Quantum gate-set universality: BQP with arbitrary elementary gates equals BQP over H, NOT, CNOT, Toffoli #3350 for the finite-gate transfer. Closed Shor's algorithm, milestone 1: quantum Fourier transform and exact period finding #3252/feat(quantum): quantum Fourier transform and exact period finding #3267 explicitly delivered only matrix semantics and exact period finding; Frontier track: quantum computation foundations, BQP ⊆ PP and the Grover/BBBV bounds #896 does not own Shor, and no open dedicated QFT-circuit continuation was located.HasExactPeriodresults do not supply it. No dedicated open continuation was located.Cslib.Crypto.RSADesc.gcd_sub_one_properin RSAAttacks.lean, which already proves the proper-factor conclusion for nontrivial square roots of one modulo RSA moduli; generalize its modulus contract where needed instead of re-proving that specialization. Existing Rabin factoring concerns a different reduction; neither the closed Shor milestone nor Frontier track: quantum computation foundations, BQP ⊆ PP and the Grover/BBBV bounds #896 supplies this general theorem. No dedicated open issue was located.The exact probabilistic-register BPP equivalence (20.7), packaged four-way unitarity characterization (20.11) and optional source-specific Dinur auxiliaries are recorded as remaining gaps, not silently promoted to completed endpoints or proposed as urgent duplicate implementations. NEXP PCP needs an explicit bridge coordinated with #892/#3609. A separate check/correction of 19.13 is needed before proposing its literal statement as development work.
Validation and manual impact
python3 -B scripts/check_operator_manual.py: pass (5,437 links, 11 excerpts; no Lean compilation).python3 -B scripts/test_operator_manual.py: 72 tests pass.python3 -B scripts/check_hygiene.py: pass. Its Lean/bibliography checks do not validate the audit table's mathematics.git diff --check: pass; all new local audit links resolve.Operator's Manual: added routes from the PCP, membership-query and quantum Fourier sections to the precise audit boundaries. Existing results inventory already links the growing audit. Agent Operator's Manual: inspected; no roles, human direction, handoff or workflow changes, so no edit needed. ROADMAP still accurately lists FGLSS, optimal Håstad hardness, Shor and gate universality as open; no status change is made there.
Please arrange coordinator review of source completeness, statement/model correspondences, both manual impact assessments and the proposed issues. The overall #4711 remains open. Prepared by Christian Reitwiessner with Codex assistance for PDF/source inspection and documentation; no independent agent or human review is claimed.