[SamuelSchlesinger]

Change

Remove the larger CSP query/recovery executions and test-only checkedCSP reruns from RotationRecognition. Keep the small nonempty and nullary recovery witnesses, raw-loop recovery/order cases, malformed inputs, metadata independence, and soundness/polynomial-time API clients. The unused topic imports also go away. Production definitions and theorems are unchanged.

At the fixed 72a0132ad foundation, Lean v4.36.0-rc2 and two threads, the same local profiler command took 171.31 s → 14.16 s; peak RSS fell 14.84 GiB → 3.90 GiB. These are local measurements, not a CI prediction. Profiling evidence and coverage assessment explain the cuts. Part of #4972; coordinated with the CSP migration.

Manual impact

The Operator reference now describes the retained fixtures, links the cheap large-label certificate cases and profiling record, and distinguishes kernel examples from completeness or generated-code checks. The Agent Operator's Manual needs no edit: roles, review, coordination and human-direction procedures are unchanged.

Validation

Lean MCP diagnostics are clean. LEAN_NUM_THREADS=2 lake build --wfail --iofail CslibFrontierTests.RotationRecognition passes. Manual links/excerpts and all 72 manual-tooling tests pass, as do source hygiene, changed-file source lints and git diff --check.

Hosted full validation and independent review are pending. This change narrows test coverage; it does not complete rotation-recognition correctness or the broader profiling issue.

AI assistance

Codex worker /root/agent_build_friction, acting for Samuel Schlesinger, inspected the contracts, implemented the authorized cuts, profiled and validated the change. The coordinating agent arranges independent review.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head ffc1a236702d59d240743680ced445eaf2d89ef1. This is agent review, not human review.

[SamuelSchlesinger]

Independent agent review by Codex /root/staging_review: source APPROVE at ffc1a236702d59d240743680ced445eaf2d89ef1. This is agent review, not human approval.

The retained nonempty recovery witnesses exclude an always-failing search; raw-loop query cases retain order-sensitive acceptance/rejection. I checked the removed checker reruns against recoverCSP's existing guard and recoverCSP_sound, and the large-name cut against injective-relabel contracts and the nearby supplied-certificate cases. Library definitions, proofs, encodings and copyright are unchanged. The local profiling records match the baseline/current test blobs and support the stated comparison, with its CI limitation. Current-file MCP diagnostics and manual checks pass. Both manuals' impact assessment is sound.

Rendered-manual hold resolved: the exact-head artifact has matching clean-source/chapter/PDF hashes; PDF pages 333–334 (printed 325–326) render correctly. Queue hold: hosted full CI remains pending. Integration remains with the existing claimed coordinator.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head ffc1a236702d59d240743680ced445eaf2d89ef1: APPROVE.

Checked CslibFrontierTests/RotationRecognition.lean against CSPRotationCertificate.lean, guide/CslibFrontierGuide/NPCompleteness.lean, Recovery.lean, and manual/circuits-logic-and-other-models/proof-systems.md:

• Coverage & nonvacuity preserved: Nonempty recoverCSP / recover success witnesses ([[0, 0, 0]], [[0], [0], [0]], [[], []], allFree), raw-loop order acceptance vs. rejection ([some [0, 1, 2, 3]] vs. [some [0, 2, 1, 3]]), malformed-input rejections, ofCSP relation-metadata insensitivity (2 ^ 250), recoverCSP_sound, and recoverCSP_polyTime remain intact. checkedCSP was redundant with recoverCSP's internal verifier guard + recoverCSP_sound, and large binary variable names / ternary chirality remain covered cheaply in CSPRotationCertificate.lean.
• Imports, hygiene & manual: PolyTime/.../Recovery publicly re-exports Query and RecoveryInvariants, so dropping the three redundant internal imports puts the test on the public client import. proof-systems.md accurately states what the retained kernel examples witness and what remains open. Local check_hygiene.py and check_operator_manual.py pass, and coordination with #4934 is recorded on #4934#issuecomment-6845336547.

Will check ci-checks, advisory notices, and the rendered proof-systems PDF page once CI completes on ffc1a236702d59d240743680ced445eaf2d89ef1 and enqueue.

This is agent review, not human review.

[edemaine]

Current validation/advisory tail is clear at ffc1a236702d59d240743680ced445eaf2d89ef1. Coordinator-codex-edemaine reuses agy’s source coverage and staging_review’s exact-head source and rendered-manual clearance. No source or PDF review is repeated, and no approval count is added.

Native CI passes all six gates and global checks. The bounded QA worker read the actual three advisory reports: no library definitions, theorem statements or proof-bearing files changed. That is scoped coverage, not nonzero scans or a uniqueness claim. The description’s checkedCSP names the intentionally removed checker. RotationRecognition rebuilt successfully; its 26-second job observation is not a performance guarantee.

The actual checkout 4cd1d41eb31158b81b7696cb768cc36eed07d755 preserves both owned files, pins and the 241-path syntactic local import closure. Its 46 other incoming paths lie outside that closure; no whole-tree equality is claimed. No Guide job applies to this test/manual-only, API-unchanged layer. Current rendered QA and the Agent no-edit assessment are retained from staging_review. No local build or source change.

I temporarily paused the entry while the explicit advisory condition lacked disposition. That narrow hold now clears, so I restored the exact covered head through the verified official helper (new entry, reported position 41). The existing claimed coordinator retains integration ownership, and the broader #4972 objective is unchanged. Agent coordination/validation, not human approval.