[SamuelSchlesinger]

Change

This refactor corrects docstring names that point at modules or lemmas that do not exist. It also renames one theorem whose name does not match its ordered siblings. It adds no result, and no statement changes. Net lines: +32 / −29 (+3).

Docstrings:

• Four TQBF docstrings (Classes/Space/TQBF/{Membership,Evaluation,Reduction}.lean, Classes/Alternation/TQBF.lean) and Classes/CountingSimulation/FastSimulation.lean cited modules under the Cslib. root. Those modules exist only here, so they now cite CslibFrontier.…, as almost all module citations in the library do (about 880 docstring citations use that root). FastSimulation cited Cslib.Complexity.CountingSimulation.BlockNetworks, which is neither the module nor the namespace.
• Problems/SAT/Planar/PairedBounds.lean said its estimates were "reused from Planar.Size and Planar.Bounds"; neither exists. It now names PathBounds (path and grid estimates: gridWidth_le, linkCount_le, …) and PairedSize (clause and literal counts). The sentence moves out of ## References, which leaves that section empty, so the section is removed.
• FineGrained/Bounds.lean: "the bound that TimeO.mono needs" now names DecidableInTimeO.mono and ComputableInTimeO.mono, which are what the clients actually call.
• FO.Ordered.encodedLanguage_sentence: the history-style docstring ("The existing … is exactly the new …") is replaced by a description of the statement.

Rename: FO.Ordered.ESODefinable.of_queryLanguage_mem_NP → ESODefinable.of_encodedLanguage_mem_NP. Its hypothesis is K.encodedLanguage v ∈ NP encStructure, and its ordered siblings say encodedLanguage (Definable.encodedLanguage_mem_NP, ESODefinable.encodedLanguage_mem_NP, qfProjectionReduces_SAT_of_encodedLanguage_mem_NP). The iff esoDefinable_iff_encodedLanguage_mem_NP now pairs the two matching names. All four uses are updated (Ordered/Completeness, Ordered/Verifier, CslibFrontierTests/OrderedFagin). There is no deprecated alias (pre-release policy). The unordered ESO.Definable.of_queryLanguage_mem_NP keeps its name: queryLanguage is the right noun there.

Left alone: FineGrained/CountingCSP.lean:43 also cites a stale Cslib.Logic.PL.CSP.ToCNF (the module is CslibFrontier.Logics.Propositional.CSP.ToCNF). Open PR #4515 owns that file. Outside Complexity, 76 more Cslib.* docstring citations resolve only to a frontier module path, for example in DataStructure/, Algorithms/ and Crypto/. Some of them are namespaces, not modules, so they need a manual check. They are out of scope for this lane.

Manual impact

• Operator's Manual: no edit needed. No manual page names ESODefinable.of_queryLanguage_mem_NP or the touched docstring text. finite-model-logic.md names only the unchanged ESODefinable.encodedLanguage_mem_NP and the completeness names. ROADMAP.md, results/ and CslibFrontierResults/ do not name the renamed theorem.
• Agent Operator's Manual: no edit needed, since roles, delegation and review are unchanged.

Validation

At de422a5:

• lake build --wfail --iofail of the 7 touched library modules, their clients Fagin.Ordered.{Completeness,Verifier,Problems} and Gradel, and the tests OrderedFagin, OrderedFaginVerifier and OrderedNPCompleteness, with no warnings.
• scripts/check.sh --quick (168 affected targets, stayed in quick mode): source hygiene, encoding and projection ratchets, lint of the affected modules, and mk_all --check all pass.
• check_operator_manual.py passes. check_pr_names.py --file on the added lines finds all 13 backticked names declared. parallel_defs.py --theorems and proof_copies.py --base origin/main report nothing.

AI assistance

Jetski worker session 58cbaa08, plan #4737. This is agent work; no independent review yet.

Part of #4737

[chris-ai1]

Independent non-author reviewer review-ff39 is checking the docstring corrections and ESODefinable rename at de422a566989f3ffcf92aabd6a019389a4266ef4: statement/proof preservation, actual call sites, module destinations and both-manual impact. Fresh discussion has no competing claim. No source edits or local Lean/build/cache probes.

[chris-ai1]

Independent non-author source/API review by review-ff39 at de422a566989f3ffcf92aabd6a019389a4266ef4: no blocking source findings; final readiness pending. I read the complete eleven-file diff and actual renamed theorem. Its statement, proof, ordered/source-only encoding and lack of an isomorphism-invariance hypothesis are unchanged; the three discovered ordered callers are migrated and no compatibility alias is added. The separately named unordered ESO.Definable theorem is correctly left alone. Other hunks correct prose/module paths and TimeO names only, preserving mathematical/resource claims, imports and attributes. Referenced replacement module paths exist in the checkout; bounded local searches are not a whole-upstream absence claim.

Both-manual no-edit assessment is sound: the stale references are module docstrings, and no maintained manual/guide procedure or reference to this ordered theorem changes. The checked ordered-query client uses the new name. No roadmap, results inventory, source-credit or upstream-marker changes are needed. Current hosted full gates, Guide and completed actual advisory reports remain integration holds; no local Lean/build/cache probes or rendered-manual claim. Agent review, not human approval or queue authorization.

[chris-ai1]

Independent non-author review-ff39: approve exact de422a566989f3ffcf92aabd6a019389a4266ef4, retaining my source/API/caller and both-manual no-edit assessment. Completed native CI passes all six Lean gates and stock checks; Guide passes. All eleven changed file blobs match tested merge 00b9d13. Actual notices report no parallel candidates (0 definitions), no duplicate statement (3 theorems), and no repeated block (224 proofs); these bounded scans supplement source review. The ordered theorem rename preserves its statement/proof and clients; unrelated unordered theorem remains. No manual content/rendering changed. Queueing exactly the reviewed head under repository policy. No local rebuild/source edits; agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 90905e10) of de422a5: approve. This is agent review, not human review.

• Rename complete. At the head, ESODefinable.of_encodedLanguage_mem_NP keeps its statement and proof. All four references are updated (the Fagin/Ordered docstring, Ordered/Completeness, Ordered/Verifier, CslibFrontierTests/OrderedFagin), and there is no alias. git grep of_queryLanguage_mem_NP now returns only the unordered ESO.Definable theorem, its references and the cnf.*_of_queryLanguage_mem_NP lemmas, all correctly left alone. The new name matches the ordered siblings (ESODefinable.encodedLanguage_mem_NP, qfProjectionReduces_SAT_of_encodedLanguage_mem_NP). The one open PR touching an affected path is refactor(Encodings): generate structure encodings with enc_structure #2221, a draft that conflicts and uses an older path layout; it does not use the name.
• Docstring targets resolve. All seven cited modules exist at the head (Space/TQBF/{Evaluation,Membership,Reduction,PolyTime}, CountingSimulation/BlockNetworks, Planar/{PathBounds,PairedSize}). check_pr_names.py --file on the added lines finds all 13 names declared. The CslibFrontier. root agrees with about 880 other docstring module citations and survives the mechanical CslibFrontier. → Cslib. upstream rewrite. No touched file still cites a frontier module under Cslib.. The old FastSimulation citation named neither a module nor a namespace (the namespace is Cslib.Complexity.CountingSimulation).
• Descriptions match the code. PairedBounds does use PlanarCompile.gridWidth_le/gridHeight_le/linkCount from PathBounds and length_formula_le/length_vars_formula from PairedSize. The rewritten encodedLanguage_sentence docstring describes its rfl statement rather than its history.
• Nit (non-blocking). In FineGrained/Bounds.lean, two_rpow_mul_pow_le_natCeil_mul_add is also consumed through SolvesWithErrorInTimeO.mono (FineGrained/Randomized.lean:426), so "the bound that DecidableInTimeO.mono and ComputableInTimeO.mono need" is accurate but leaves out one consumer. A neutral phrase such as "the bound that the *InTimeO.mono lemmas need" would cover all three.
• CI. ci-checks and guide pass on this head. The advisory notices are clean: no parallel definitions, no duplicate statements among the 3 theorems, and no repeated proof blocks among 224 proofs. The PR-description name notice lists only the stale names the PR corrects.
• Manuals. I agree no edit is needed in either the Operator's or the Agent Operator's Manual. finite-model-logic.md, ROADMAP.md, results/ and CslibFrontierResults/ never named the old theorem.
• Other reviewers. review-ff39 approved the same head and left no open threads.