[SamuelSchlesinger]

Restate the four existing GSW serialized evaluation certificates—decryptResidue, decryptSerialized, nandEntry and nandSerialized—with canonical plain polynomial-time premises and results. Full input telescopes, unary dimensions/indices, binary arithmetic, complete-word encodings and runtime algorithms are unchanged. The existing raw construction proofs are reused locally; there are no aliases or public-field changes. Refs #456, #608, #750.

Framework friction: captured PPT callbacks need plain deterministic certificates. This bounded domain parent supplies the actual decryption/NAND providers before the shared captured-map change. Corresponding fixtures and axiom-name guards use the canonical API; all runtime cases, ordinary tactics, allowed axioms and the completeClient program/budget are preserved. Its local proof transport supports main's current callback contract. The broader Crypto sweep remains open: the fresh inventory is 328, down from 332.

All six required gates, fresh strict report, hygiene and catalogue checks pass at 4db59e04. The complete GSWEvaluation source also passes uncached on actual-main base 5750a596. Source comparison checks all four full telescopes under only predicate/name substitution and confirms the completeClient definition is byte-identical. Selected abstract statements, definitions, scope and rendering are unaffected; no PDF update is needed.

AI assistance: Codex extracted the already-checked sweep slice and validated its API/consumers. Independent review is requested.

[SamuelSchlesinger]

Independent exact-head review requested from reviewer-claude-c4b0c164-01 at 4db59e041befea5839ba5c7779f9ae71e4fdcd92. Bounded four-rule GSW domain parent, two files; runtime algorithms and the completeClient definition/budget are unchanged, and the axiom guard sets are unchanged.

All six gates and the fresh strict report, hygiene and catalogue checks pass on actual-main base 5750a596; the full GSWEvaluation source also passes uncached. Please focus on the four complete type/encoding transports and preserved clients. The remaining Crypto sweep stays open.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at 4db59e0.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — CHANGES REQUESTED at 4db59e0

Agent review, not human approval.

The source change itself is right:

• Faithful restatements. All four certificates (decryptResidue, decryptSerialized, nandEntry, nandSerialized) are restated plainly with the same functions, the same full argument telescopes and the same encodings: encUnary dimensions and indices, encBits words, and encNat/encBool/encBits outputs.
• Tidy only inside proofs. Tidy now appears only inside proofs, through .tidy on the hypotheses and refine .of_tidy, and through attribute [local fun_prop] ComputableInPolyTime.tidy in on nandSerialized.
• No stale names. Nothing in the tree still refers to the old computableTidilyInPolyTime_* names. The module's "Main results", the two tests and the two axiom guards are renamed consistently, and completeClient is unchanged.

Blocking

1. The tidy-statement ratchet fails at this head. Hosted ci-checks run 40118175642 fails at the "Tidy statement ratchet" step:

   Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean: 0 (baseline 4)

   scripts/tidy_surface_baseline.json:345 still records 4 for this module, and an exact-count ratchet rejects a count below its entry. Please run python3 scripts/check_tidy_surface.py --update and commit the result, which deletes the entry. lake build, lake test and lake lint pass. mk_all --check, lint-style and checkInitImports were skipped after the failure, so they need the rerun.

Nonblocking

• In computableInPolyTime_decryptSerialized, the four hypotheses are shadowed by their tidy versions, then converted back with .of_tidy to call the plain decryptResidue rule, then converted to tidy again. Taking hvalue := (computableInPolyTime_decryptResidue hn hw hsecret hciphertext).tidy before the shadowing would avoid the round trip.
• In ComplexityTests/Crypto/GSWEvaluation.lean, the completeClient IsPPTOn example now needs attribute [local fun_prop] ComputableInPolyTime.tidy in, because the captured-callback contract is still raw. That is acceptable as a transitional measure, which the PR's friction note acknowledges. Please make sure the shared captured-map change (Review findings: certificate registration, degree domain, and reuse fixes #750/refactor(computability): use plain resource and Crypto interfaces #810) removes this local bridge, so it does not become the standard client pattern.

[SamuelSchlesinger]

Coordinator fix, applied under the validated-fix rule (Samuel's decision of 2026-10-24, being recorded in #832). coordinator-claude-c4b0c164-20261023 pushed 28954901 on top of 4db59e04. It's one commit, and it changes only scripts/tidy_surface_baseline.json.

• The fix. The commit removes the GSW/Serialized/Evaluation/PolyTime.lean entry (4 → 0), the only mismatch hosted CI reported (run 40118175642). The resulting file is byte-identical to what check_tidy_surface.py --update writes for those counts: 401 entries, 1,890 statements.
• Review. reviewer-claude-c4b0c164-01 approved the source in its exact-head review (6387684320); its only blocker was this baseline. Its nonblocking notes (the tidy → plain → tidy round trip and the local fun_prop attribute in the completeClient test) are left to the author.
• Verdict. coordinator-claude-c4b0c164-20261023 — APPROVED at 289549019e8e4ff0866aa5bf99f915d9893fd670. Agent review, not human approval. I'll enqueue once hosted CI is green at this head, including the mk_all, lint-style and checkInitImports steps that were skipped after the failure.

Author: please fetch before pushing again.