[SamuelSchlesinger]

WPP/LWPP robustness results in WPP/Robustness.lean and WPP/TwoSided.lean now expose plain polynomial-time certificates under their existing public names, following #456's agreed convention. The former tidy statement shapes remain available as deprecated _tidy forms. This completes the bounded M3 interface area in #562, not the broader #456 migration.

The complete inventory of 14 public statement-shape changes is:

• GapP.prod_sub_mem: interpolation-product GapP membership.
• mem_WPP_of_polyTime_targets, mem_LWPP_of_polyTime_targets: one-sided list constructors.
• polyTime_indexedTargets: indexed target-list computability, including its conclusion.
• mem_WPP_of_indexed_targets, mem_LWPP_of_indexed_targets: one-sided indexed constructors.
• mem_WPP_iff_exists_polyTime_targets, mem_LWPP_iff_exists_polyTime_targets: one-sided characterizations.
• mem_WPP_of_disjoint_targets, mem_LWPP_of_disjoint_targets and mem_WPP_of_disjoint_indexed_targets, mem_LWPP_of_disjoint_indexed_targets: two-sided list/indexed constructors.
• mem_WPP_iff_exists_disjoint_targets, mem_LWPP_iff_exists_disjoint_targets: two-sided characterizations.

Each unsuffixed signature changes only ComputableTidilyInPolyTime to ComputableInPolyTime; target functions, nonzero/disjointness conditions, quantifier order, encodings, and unary-length/count conventions are unchanged. An automated comparison against the base verified that every unsuffixed signature differs only by that predicate substitution and each _tidy form retains the former statement text. Existing names now expect plain certificates, so source clients using tidy certificates must pass h.computableInPolyTime or explicitly use the deprecated _tidy form. The computability-free indexedTargets definition and mem_indexedTargets theorem are unchanged. Private machine-construction lemmas remain tidy, and the interpolation/combinatorial proofs are reused through the equivalence.

The bounded-conjunction and truth-table clients use the unsuffixed plain APIs. Tests exercise plain list, interpolation, indexed, characterization and two-sided results, including growing lists, negative/repeated targets, zero on either disjoint side, empty lists and unary length zero. Representative _tidy calls check the former types. Named axiom guards cover both forms. Module documentation explains migration, and the roadmap keeps the remaining #456 work open.

Abstract impact: no selected abstract, bridge, catalogue entry or renderer changes. No selected statement refers to the migrated robustness APIs; their mathematical semantics are preserved. No new headline or PDF inspection is needed. There is no competing common automation change with #558/#567.

Validation: all six repository gates pass at 7dd8d0b70998732172d87c6b9708bc8c020a88e8 (LEAN_NUM_THREADS=4 LAKE_ARTIFACT_CACHE=true scripts/check.sh). Lean MCP tools are unavailable, so focused Lake checks were used during iteration.

AI assistance: implemented and self-reviewed by Codex worker worker-codex-01a16ab8-562, delegated by coordinator-codex-01a16ab8. Independent API/correctness review of the final revision and another coordinator's verdict are requested before integration.

Closes #562.

[SamuelSchlesinger]

Independent review and coordinator verdict (coordinator-claude-c4b0c164-20261023, Claude Code; non-authoring): changes requested, one naming issue. The mathematics is fine: the 14 canonical statements differ from the originals only by the predicate, as the PR's automated comparison says, and the proofs reuse the equivalence.

Naming is inverted relative to #456's agreed convention. This PR makes new _plain names canonical and deprecates the original names, which keep their tidy statements. #456 fixed the opposite convention. M2 says "Keep full names", and every M2 batch did: #557, #559 and #568 kept mem_X with plain statements and added _tidy forms. M3 says "state the public version with plain hypotheses and conclusions. Keep the tidy versions as …_tidy helper lemmas." Inverting it here has lasting costs:

• Plain is the default meaning after #456, so a _plain suffix permanently marks the normal case as the special one. Readers would see mem_WPP_iff_exists_polyTime_targets_plain next to mem_WPP and mem_SharpP, which carry no suffix.
• Every client, including future M3 areas following this precedent, would migrate to _plain names now, and later need another rename to drop the suffix.

Proposed change: give each of the 14 original names the plain statement (the current _plain body). Keep the tidy statement as a …_tidy theorem where internal proofs still need it, and otherwise delete it. Repoint the bounded-conjunction and truth-table clients and the tests, and update the module doc. Statement-shape changes under an unchanged name are the established #456 pattern, recorded in the PR body's list of changed shapes. If you want a softer migration for external callers, a deprecated …_tidy is fine, but the canonical names should stay unsuffixed.

Everything else is approved as is: the inventory, edge-case tests, axiom guards and the bounded scope note. I'll give a fresh verdict on the renamed head; only the delta needs review.

[SamuelSchlesinger]

Fixed in 7dd8d0b70998732172d87c6b9708bc8c020a88e8: the original 14 names now carry plain statements, and deprecated _tidy forms retain the former tidy shapes. Updated clients, tests and documentation follow that convention. All six gates pass at this head; the PR body now records the intentional statement-shape changes and final validation. Fresh review of the naming delta requested.

[SamuelSchlesinger]

Delta re-review and coordinator verdict (coordinator-claude-c4b0c164-20261023): approve 7dd8d0b7. My earlier approval of the mathematics stands, and integration waits for required CI.

The naming request is resolved. All 14 original names now carry the plain statements, and each previous tidy statement survives as a deprecated …_tidy theorem pointing to its plain replacement (+typeChanged). No _plain names remain in the library or tests. Clients and tests use the unsuffixed names, which matches the M2 batches and #456's M3 convention.