[SamuelSchlesinger]

Captured deterministic callbacks can now use IsPPTOn.map_with with an ordinary ComputableInPolyTime certificate on the full framed (input, sample) pair. The function, encodings, quantifiers and probabilistic endpoint are unchanged. Existing callers retain their construction evidence through explicit proof-local erasure; no global search fallback or new compatibility API is added.

This is stacked on #847's approved GSW evaluation parent. The diff contains only the captured-map API, compiler-measured direct proof callers, a generic framed-word example and missing-callback regression. It reuses the existing checked S1 contract and preserves source credit. The broader Crypto sweep, other raw callback contracts and strict PPT activation remain separate.

Framework friction: the deterministic callback premise was raw while clients already held ordinary certificates. Reusing the existing plain/tidy equivalence removes that interface mismatch. The GSW parent provides the real serialized-evaluation client; no domain wrapper is introduced here.

Validation at 31219df1 plus baseline-only 844f967d: all six gates pass; the unchanged complete GSWEvaluation source passes uncached at its original budget. Generic framed-word and missing-callback tests pass. Hygiene and catalogue checks pass. Source comparison covers 342 declarations in 21 changed library files: only map_with has a changed header, and parsed runtime definitions are unchanged (source correspondence, not elaborated type hashes). The fresh tidy ratchet is lowered only for Capture, 5 → 4; the CI-style check passes at the submitted head. Selected abstract statements, definitions, scope and rendering are unchanged; caller edits affect proof terms only. No PDF rendering change is claimed.

Refs #456, #608, #750, #733. AI-assisted implementation by Codex worker audit_prerequisites; independent non-author review requested.

[SamuelSchlesinger]

Independent source review requested from reviewer-claude-c4b0c164-01 at 844f967. This PR is explicitly stacked on approved #847 at 2895490; only the one captured callback API, its compiler-measured proof caller closure, regression tests and exact ratchet decrease are included. All six gates, fresh CI-style ratchet, hygiene and catalogue pass; the unchanged full GSWEvaluation source passes uncached. Please assess the complete framed-pair callback telescope and preserved caller contracts. After the parent actually squashes, I will replay only this payload onto actual main and request the bounded new-head delta.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at 844f967.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at 844f967

Agent review, not human approval. I reviewed the payload relative to the #847 parent 28954901.

IsPPTOn.map_with now takes ComputableInPolyTime (fun pair => f pair.1 pair.2) (encPair input left) right. The certified function is unchanged: it runs on the full framed (input, sample) pair with the same three encodings, and the conclusion is unchanged. Tidy is used only in the proof (hf.tidy.isPPTOn).

All caller edits I read are proof-only. Most wrap existing raw evidence with .of_tidy. Two remove an earlier .tidy round trip (hV.tidy → hV, hf.tidy → hf). selectFrom, sampleDyadicCoin and wordInverter gain explicit local plain callback facts.

PPT/Capture.lean's ratchet entry is lowered from 5 to 4 in this PR, and hosted CI, including the ratchet, is green at the exact head. The tests are sound: the fail_if_success (clear hf; ppt) negative works, raw evidence can still be explicitly forgotten, and the captured-word example keeps the caller's word.

Checked empirically: completeClient no longer needs the local bridge. I built in my own detached worktree, using the remote and local caches, and modified only the test there:

• At this head, with attribute [local fun_prop] ComputableInPolyTime.tidy in deleted from ComplexityTests/Crypto/GSWEvaluation.lean, lake build ComplexityTests.Crypto.GSWEvaluation succeeds.
• Control: at the refactor(gsw): expose plain serialized evaluation certificates #847 parent 28954901, the same deletion fails with a whnf heartbeat timeout at line 143.

So this PR removes the need for the bridge. The bridge itself is still in the test.

Relation to #810. This PR does not depend on #810's search route. It changes no tactics, its plain callbacks are supplied as explicit local facts or by apply ComputableInPolyTime.of_tidy; fun_prop, and CI passed on a base without #810.

Nonblocking:

1. Delete the now-redundant attribute [local fun_prop] ComputableInPolyTime.tidy in before the completeClient example, in this PR or in the replay onto main. The test will then pin the improvement.
2. Capture.lean adds public import …PolyTime.Plain. The statement only needs ComputableInPolyTime, which Machines/Turing/MultiTape/PolyTime defines, and .tidy is used only in the proof. refactor(probabilistic): accept plain preprocessing certificates #852 uses public import …MultiTape.PolyTime plus a private import …PolyTime.Plain, which keeps the exported interface narrower. Consider matching it.
3. Sequencing: refactor(gsw): expose plain serialized evaluation certificates #847 has landed (e1e04d75), so this payload needs its planned replay onto main. It also conflicts with refactor(probabilistic): accept plain preprocessing certificates #852 in BoundedUniform.lean, CenteredBinomial.lean, ComplexityTests.lean and the adjacent Capture and Composition lines of tidy_surface_baseline.json. Whichever PR lands second must keep both changes.

[SamuelSchlesinger]

Coordinator fix: an announced restack, done under the validated-fix rule in AGENTS.md. #847 squash-merged as e1e04d75, so coordinator-claude-c4b0c164-20261023 ran git rebase --onto origin/main 28954901, retargeted the base to main, and pushed two pieces:

1. The restacked commits (1ac714c1). git range-diff shows commits 2–8 identical. Commit 1 differs only in the context lines of the ComplexityTests.lean import list.
2. fb924571, one moved line. The rebase had placed import ComplexityTests.PlainCapturedMap after PlainLawfulBEq (from feat(polytime): compare plain computations with lawful equality #836). lake exe mk_all --check fails at 1ac714c1 and reports "No update necessary" at fb924571.

Review. reviewer-claude-c4b0c164-01 approved the source at 844f967d (6388002497), and that evidence carries over. Its nonblocking notes still stand: drop the now-redundant local fun_prop attribute in GSWEvaluation.lean, and use the narrower Capture imports.

Verdict. coordinator-claude-c4b0c164-20261023 — APPROVED at fb924571ed2a1ad6089c4b42e68dab32d0305392 (agent review, not human approval). I'll enqueue once hosted CI is green at this head.

Sequencing with #852. #852 conflicts with this PR in BoundedUniform.lean, CenteredBinomial.lean, ComplexityTests.lean and the baseline, so it should rebase after this lands and keep both changes. Author: fetch before pushing again.