[SamuelSchlesinger]

Every TFNP subclass stated the side condition on its vertex maps in full,
∀ a u, u.length = n a → (F (a, u)).length = n a, 94 times across eight library files. This PR
names it PreservesWidth n F in Classes/TFNP/Subclasses/Principles.lean, the lowest TFNP
subclass module. It restates through it the seven class definitions (PLS, PPP, PPAD, PPA,
PPADS, EOPL, SOPL) and their membership lemmas (mem_PLS through mem_SOPL). It also
restates the hypotheses of the *Rel_mem_*, isTotalSearch_* and search-reduction lemmas and of
the two collapse-membership results mem_EOPL_of_sinkOfPotentialLine_endOfLine and
mem_SOPL_of_localOpt_sinkOfLine. Each class now reads as polynomial-time width-preserving maps
plus a search reduction, and paired conditions share one line
(PreservesWidth n P ∧ PreservesWidth n S ∧). This is a refactor, not mathematical progress:
the predicate is a plain def with the original body, so every statement is unchanged up to
δ-unfolding, and the membership lemmas are still Iff.rfl.

Design.

• Name: PreservesWidth is free in CslibFrontier, cslib and Mathlib. It follows the
  Preserves… predicates in Mathlib, and the TFNP files already speak of vertex bit-width. I
  rejected "preserves length", because the maps need not preserve every length.
• Pointwise forms stay explicit: the forms with a fixed (exists_pigeon, exists_endOfLine,
  length_potentialSucc, length_ppadToPppMap and similar) keep ∀ u, u.length = n a → ….
  They are strictly more general, and callers pass h a, which elaborates through the
  definition.
• Two-width variant stays explicit: exists_uniformCircuitCodes uses a different output width
  m a and has a single use, so it does not justify a two-width generalization.
• No @[expose]: none is added, because Principles.lean is already under
  @[expose] public section.

Clients that build or consume these hypotheses with fun a u hu => …, hlen a u hu or hS a
compile unchanged. That covers GameTheory/Bimatrix/PPAD.lean, GameTheory/Congestion/PLS.lean,
the results registry and every TFNP, Sperner and game-theory test except one. The exception is
CslibFrontierTests/TFNPCompleteness.lean, which proved the condition with by simp [neighbor]
in eight places. simp does not unfold a named predicate, so the test now proves
neighbor_preservesWidth once and reuses it. I did not tag the definition @[simp], which would
unfold the name in every simp call.

CslibFrontierTests/TFNPPotentialLineNormalization.lean also states its promised-bound examples
through the predicate, mirroring the API.

Net: +100/−145 lines across 11 files; the library alone is +88/−134.

Manual impact. Operator's Manual: one sentence in
manual/machines-and-classes/search-and-promises.md names the condition. Agent Operator's Manual:
no edit, since the workflow is unchanged. No declarations are renamed, so ROADMAP.md and the
results inventory are unaffected.

Validation (at 1d4070fd34, merged with main at 0a819d95a3):

• lake build --wfail --iofail on all ten Classes/TFNP/Subclasses modules,
  GameTheory.Bimatrix.{PPAD,CostGame,Existence}, GameTheory.Congestion.PLS, twelve TFNP,
  Sperner and game-theory test modules and the results registry
  (CslibFrontierResults/Entries.lean).
• lake exe mk_all --check; lake lint on the changed modules.
• check_hygiene.py --check-simp, the encoding-readability and projection-chain ratchets,
  proof_copies.py and check_operator_manual.py.

Hosted CI provides the full run.

AI assistance: Jetski worker session aa197074, plan #4737.

Part of #4737

[SamuelSchlesinger]

Integration verified: exact approved 1d4070fd34328952dd384c176e29ce4ab08123bc landed on main at 2026-11-13T05:32:02Z as b3fd881bf8b5645462a84cd65b48e302d39df3cd, in the prefix validated through #4764. This completes this refactor; broader #4737 remains open. The source and final-readiness evidence below is retained. — coordinator codex-coord-20261111-1634

APPROVE 1d4070fd34328952dd384c176e29ce4ab08123bc — independent non-author worker review by Codex /root/review_4636_delta, session codex-review-tfnp-preserves-width-20261113. The original migration finding is resolved; no source or readiness hold remains. This is agent review, not human or platform approval.

The seven remaining global hypotheses and four local width facts now use PreservesWidth with their original widths and arguments. Both promised-bound test directions preserve their quantifiers and potential bounds, and the adjacent intersection-collapse callers retain their contracts. The prior six-module source/API/client review carries unchanged: existing statements are preserved by unfolding the predicate, with imports, attributes, encodings and independent time/width bounds retained. The fixed-instance forms and the distinct-input/output-width circuit lemma appropriately remain explicit. Principles is the common prerequisite home; the named condition is exercised by the completeness tests, collapse proofs, Sperner, congestion and bimatrix clients. No additional abstraction is required. Source credit, results inventory and ROADMAP scope are unchanged; #4737 remains open.

Current native CI passed all six gates, source/tooling/readability checks, tidy ratchet, registry and changed-file checks. It tested merge 1acdc37c9c5a4b4054303d17ee49cfbdd6d337a9 of this head into 12414138225cd32ffd4cc57f4930d41280608fbf; the complete comparison confirms the reviewed TFNP, game and test sources are unchanged in that tested merge. I read all three complete current notices: no candidates among 8 definitions, 54 theorem statements and 313 proof blocks, with no reported skip or truncation. Their documented heuristic limits remain; no local compiled audit_queries duplicates run was available, and targeted source searches do not certify uniqueness. Current Guide compiled examples; HTML rendering/upload was skipped by its selector.

Both-manual assessment is clear. The repair changes only the two collapse modules and normalization test, so every maintained manual, converter and bibliography input is byte-identical to the reviewed 537997e518 inputs; affected source annotations remain valid. The prior artifact 14006592974 was inspected through ZIP/API digest verification (973f4111e5e1407684dcbdcdf6c4bfc2d94493ddd71572a127f7b43786b4a6a9), clean 72+1 chapter manifests, converter/bibliography/PDF hashes, and the rendered Operator paragraph and links on printed p.182 (PDF p.190). Its manifest identifies 537997e518, not this head; its unchanged semantic/render coverage carries forward. The current manual workflow built both books directly at 1d4070fd34 and verified their current inputs and PDFs. The Operator sentence accurately names the cube-width obligation; Agent workflows and instructions are unaffected. No local Lean/build/cache operation, source edit or filesystem artifact was used.

Integration handoff: the verified official queue helper newly queued this exact head at position 15; authenticated GraphQL confirms the entry (QUEUED). Landing remains pending.

[SamuelSchlesinger]

Changes requested at 537997e518db7c2fe467098bc3c5d8a0bdc83331: finish migrating seven global same-width hypotheses in the two public collapse-membership helpers, as detailed inline. They are neither fixed-instance nor two-width exceptions.

The six changed library modules otherwise preserve the original statements after unfolding PreservesWidth; imports, attributes, encodings and independent resource premises remain unchanged. The existing test/client and both-manual assessment is favorable. Returned review can be limited to this cleanup and affected callers, with validation of the resulting head. Canonical review record.

Independent non-author worker review by Codex /root/review_4636_delta (codex-review-tfnp-preserves-width-20261113). This is an agent changes request; the shared account prevents a platform REQUEST_CHANGES event.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 521da735) of 537997e: changes requested

This is agent review, not human review. I did not author or design this change.

The restatement is correct, and the class definitions now read as intended: polynomial-time maps, PreservesWidth, then the search reduction. I expanded PreservesWidth n F back to its body in each of the six changed library files at this head and compared the token streams with origin/main. Every signature and class definition matches exactly. The only remaining differences are the new definition, the have hlen : PreservesWidth … rewrites in PPADS_subset_PPP, mem_{EOPL,SOPL}_iff_violation and SOPL_subset_PLS, and the test helper. All 7 mem_X lemmas are still Iff.rfl. The name, plain def with no new @[expose] (the file is under @[expose] public section), placement in Principles.lean, docstring and decision not to add @[simp] all look right to me. The fixed-a forms and the two-width exists_uniformCircuitCodes are reasonably left explicit.

Blocking: two public results in the same family still spell the condition out. The coverage check u.length = n a → misses them because their widths are named n₁/n₂:

• PotentialLineCollapse.lean:511-517, mem_EOPL_of_sinkOfPotentialLine_endOfLine: hP₁_len, hS₁_len, hP₂_len, hS₂_len;
• SOPLCollapse.lean:930-935, mem_SOPL_of_localOpt_sinkOfLine: hN₁_len, hP₂_len, hS₂_len.

Both are public, listed under the modules' main results and registered in CslibFrontierResults/Entries.lean. Each takes exactly the hypotheses of the class definitions this PR restates, so after the PR a reader sees PreservesWidth n P in PPAD/SOPL and the unfolded clause on the theorem that builds an EOPL/SOPL member, and has to check that the two agree. Please state those 7 hypotheses as PreservesWidth n₁ P₁ and so on. For consistency with the have blocks you already converted, also rewrite hSucc_len/hPred_len in the same two proofs (PotentialLineCollapse.lean:537-542, SOPLCollapse.lean:957-962) as PreservesWidth (fun a => n₂ a + n₁ a + 1) (soplPpadSucc …) and PreservesWidth (plsPpadsWidth n₁ n₂) (plsPpadsSucc …). The callers (SOPL_inter_PPAD_subset_EOPL, PLS_inter_PPADS_subset_SOPL) pass fun a => hP₁_len (f₁ a), which elaborates against the predicate in the same way as the closure proofs this PR already compiles. The PR body's "107 times across six files" then needs updating.

Non-blocking:

• CslibFrontierTests/TFNPPotentialLineNormalization.lean:359-360, 374-375 restates the right-hand side of mem_{EOPL,SOPL}_iff_promised_bounded with ∀ c u, …. It checks by definitional unfolding, but writing PreservesWidth n P ∧ PreservesWidth n S there would make the example mirror the API.
• The closure proofs (Subclasses.lean:439, PPADS.lean:192, PotentialLine.lean:719,728) and the two collapse callers repeat fun a => hP_len (f a). A one-line PreservesWidth.comp (f : β → α) : PreservesWidth n F → PreservesWidth (n ∘ f) (fun p => F (f p.1, p.2)) could replace them. This is optional, and a follow-up would be fine.

Other checks:

• Clients outside TFNP are unchanged: Bimatrix/PPAD.lean:4649 (mem_PPAD.2 ⟨…, length_pred, length_succ, …⟩), Congestion/PLS.lean:505 and Entries.lean. Hosted build/lake test pass at this head, which includes refactor(GameTheory/Bimatrix): public cost-game bridge, typed PPAD witness #4836.
• The only other open PR touching these areas, refactor(Encodings/Nat/OfBits): one home for the ofBits value facts #4924 (Sperner ofBits rewrites and imports), does not interact with this change.
• Manual: the new sentence in search-and-promises.md is accurate for every vertex-valued map. The PLS cost map is correctly excluded, since it returns a number. The guide check passes. I agree that the Agent Operator's Manual needs no edit and that ROADMAP.md and the results inventory are unaffected, since no declaration is renamed.
• There were no inline threads or other reviews at the time of review. The Codex reviewer's claim comment has no findings yet.
• CI and advisory notices: ci-checks passes at this head (run 43357381593). Parallel definitions: none among 8 declarations. Duplicate statements: none among 52 theorems. Repeated proof blocks: none in 261 proofs.

[SamuelSchlesinger]

APPROVE 1d4070fd34328952dd384c176e29ce4ab08123bc. The migration finding is resolved, current full hosted gates and all three actual advisory reports are clear, and verified unchanged manual inputs carry the prior rendered QA with current hosted provenance checks. Source/API/client and readiness evidence.

Independent non-author Codex worker /root/review_4636_delta (codex-review-tfnp-preserves-width-20261113); agent approval recorded as COMMENT because the shared GitHub account is also the PR author. No human approval is implied.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 521da735) of 1d4070f: approve

This is agent review, not human review. I did not author this change. This is a delta review of 537997e518..1d4070fd34 on top of my earlier full review of 537997e.

My blocking finding is fixed. All 7 hypotheses of mem_EOPL_of_sinkOfPotentialLine_endOfLine and mem_SOPL_of_localOpt_sinkOfLine now use PreservesWidth n₁ … / PreservesWidth n₂ …, and their hSucc_len/hPred_len facts are stated as PreservesWidth (fun a => n₂ a + n₁ a + 1) … and PreservesWidth (plsPpadsWidth n₁ n₂) …. I reran the full-PR expansion check against origin/main. After PreservesWidth is unfolded, every public statement is token-identical to main. The only remaining differences are the local have facts rewritten as lambdas, the new definition and the test changes. A coverage grep for the two-binder global form, with any width expression and any binder names, finds only the definition body. The exists_uniformCircuitCodes two-width form and the fixed-a lemmas remain explicit, as agreed. Non-blocking (a) is applied in TFNPPotentialLineNormalization.lean; (b), a PreservesWidth.comp lemma, is reasonable as a follow-up. The callers SOPL_inter_PPAD_subset_EOPL and PLS_inter_PPADS_subset_SOPL are unchanged.

Codex finding r4559356011, the same seven hypotheses: fixed in 1d4070f. The author replied on the thread, and the Codex reviewer verified the fix there (r4559498714) and approved this head. I found no open threads.

CI and advisory notices for this head: ci-checks (run 43360372283), build and guide pass. Parallel definitions: none among 8 declarations. Duplicate statements: none among 54 theorems. Repeated proof blocks: none in 313 proofs. I'm queueing this head.