[SamuelSchlesinger]

Proves single-challenge IND-CPA for the actual serialized GSW key generator and encryption program, assuming decision LWE for their exact centered-binomial error distribution. The public-key marginal is identified with the LWE experiment, and one uniform strict-PPT reduction retains the adversary's complete saved state. Its bound is AdvCPA ≤ 2·AdvLWE + N·sqrt(2^N / 2^m), where N = (n+1)w.

The explicit family n = η = λ+1, w = 16+8⌈log₂(λ+1)⌉, and m = N+2λ supplies native parameter routines, negligible statistical error, and strict fresh/one-NAND correctness margins. The endpoint GSW.Parameters.indCPA therefore leaves only its specified LWE premise. Reusable additions cover public-key replacement, encoded LWE experiments, dyadic negligibility, and independent replicated sampling.

Closes #501 as a security milestone within #486. This does not establish LWE hardness, circular security, native decryption/evaluation, shallow decryption, or bootstrappability. The current parameter family is not claimed to support full FHE. The native honest algorithms come from merged #519.

Validation: all six repository gates passed on the final source: strict build, aggregate-import check, strict tests, lint, style lint, and initialization-import check. Regressions exercise adaptive message selection and saved public-key state, attain the reduction's factor-two loss, and check actual honest/reduction efficiency certificates. The checked abstract has 40 roots, 164 audited dependencies, no internal-definition allowlist, and headline axiom guards containing only the three permitted standard axioms.

Independent source/API/correctness review by /root/maintenance_audit approved published head a406f81f19d5cb9c7383cacc1ca37e3d82e60eae (tree d79a101d3483da59b6edbf0740152d288e4a828a); review record. /root/refactor_plan_review independently reviewed the abstract/bridge and all six rendered PDF pages. The final standalone PDF has SHA256 529a806df8e52120c9fcc98e58b052b4a5ae7390d9fcfb8b44930d650e270017; its statement links resolve to this head at native_algorithms and indCPA. Local PDF layout adjustments keep explanations with declarations and reserve footer space; the repository renderer is unchanged. Remote CI is separate from these completed local checks.

Documentation/index assessment: the roadmap records this result and its remaining gaps; the new supporting formal abstract is intentionally outside the curated headline catalogue while full FHE remains open. Catalogue and selected-headline documentation are unchanged.

Mathematical credit: Gentry, Sahai and Waters, GSW 2013, §§3.1–3.2; additional sources are cited in the modules and abstract. AI-assisted by OpenAI Codex: core/reduction integration by worker-codex-gsw-lwe-security-20261023, parameter subtask by worker-codex-gsw-parameters-20261023, and abstract by /root/library_map. The independent reviews above are agent reviews, not human or platform approval.

[SamuelSchlesinger]

Independent source/API/correctness review: APPROVE, no remaining findings.

Reviewer: /root/maintenance_audit. Reviewed head a406f81f19d5cb9c7383cacc1ca37e3d82e60eae, tree d79a101d3483da59b6edbf0740152d288e4a828a; refreshed the live PR head immediately before posting. All 14 remote file identities match the reviewed manifest c76e2b0df264458f306a6177858d65194fa3e76fe1090dea66bddac87ae894e1 and the clean, tested local tree.

Checked the exact generated-public-key LWE law, actual chosen-message game, one uniform native reduction retaining saved state, factor-two quantitative loss, negligibility argument, positive-noise parameter/correctness margins, regression clients, aggregate imports and roadmap scope. The endpoint is conditional on the specified decision-LWE hypothesis; it does not establish hardness, circular security or bootstrappability. The Abstract/Bridge source review was independently delegated to /root/refactor_plan_review, which confirmed the exact two hashes in this manifest without findings. That reviewer also performed the separate six-page PDF/source-link review recorded in the PR description.

I inspected the final author-run log: all six repository gates passed. I ran no duplicate Lean builds and made no edits. My independent scope is this PR's 14 new/changed paths; the merged #519 parent, which I helped author, is excluded. This is an agent review comment, not a platform or human approval. No merge performed.

[SamuelSchlesinger]

Coordinator verdict: approve a406f81f19d5cb9c7383cacc1ca37e3d82e60eae, with current-main integration validation still pending. I reuse the exact-head independent source/API and abstract/PDF reviews; their stated scope covers this delta and excludes the already-reviewed #519 parent.

I additionally checked the public-key marginal law, hidden-bit reduction and saved state, native runtime premises, explicit parameter inequalities, attained factor-two regression and roadmap against #501's acceptance criteria. No findings. The result is conditional single-challenge IND-CPA under its exact decision-LWE hypothesis, with fresh/one-NAND arithmetic margins; hardness, circular security and bootstrappability remain open. The supporting abstract remains outside the selected catalogue, as documented.

Reviewer coordinator-codex-20261023-1050-root; agent review, not human or platform approval.

[SamuelSchlesinger]

Code CI passed at the reviewed head. The separate PDF workflow exhausted its 30-minute job limit while downloading TeX/font dependencies, before running the renderer or generating an artifact. I recorded that infrastructure failure in #536; the locally generated supporting security abstract and its completed visual review remain unchanged.

[SamuelSchlesinger]

The PDF retry succeeded. Attempt 1 was cancelled after roughly 30 minutes during TeX/font downloads, before rendering; the workflow's 30-minute timeout was the likely cause. Only that cancelled build job was retried, with no source changes.

The successful checkout was 5cfc69ee, whose tree matches the reviewed main-plus-PR merge. It built the unchanged twelve-group curated catalogue; this is separate from the six-page supporting GSW abstract review already recorded above. Hosted Lean CI is also green. Corrected integration passed all six local gates and 89 Python/tooling checks, with prerequisite merge-tree checks still pending. Coordinator coordinator-codex-20261023-1050-root.