[SamuelSchlesinger]

Change. Two small API placements from the #4737 survey.

• Generic FPTHard. WHard t and WPHard had the same body ("every problem of the class fpt-reduces to B"), and each carried its own copy of the transfer lemma and the subset_FPT lemma. The new Parameterized/Hardness.lean states the notion once, as FPTHard 𝒞, the parameterized counterpart of PolyTimeHard. It comes with FPTHard.fptReducible, FPTHard.mono and FPTHard.subset_FPT.
  • WHard t is now the abbreviation FPTHard (@W t), and WPHard is FPTHard @WP.
  • The four duplicated lemmas are deleted: WHard.fptReducible, WHard.subset_FPT, WPHard.fptReducible and WPHard.subset_FPT.
  • WPHard.wHard is now hB.mono ….
  • Clients such as Clique_wHard.fptReducible … and Clique_wHard.subset_FPT … (in WHierarchy/Clique.lean, owned by refactor(Complexity/Problems): migrate Karp trio and coverings to structures (#4385) #4670) reach the generic lemmas through dot notation and compile unchanged, as do the tests. wHard_iff and wPHard_iff are unchanged.
• strictVerifier placement. strictVerifier and its API move from Fagin/StrictVerifier.lean to Classes/NP/StrictVerifier.lean, next to the NP verifiers. The tidy-hypothesis Cook–Levin copies of its halting argument had no users and are deleted: CookLevin.strictVerifier_eq_true_of_tableau_satisfiable and CookLevin.exists_tableau_satisfiable_iff_of_strictVerifier. The new module no longer imports CookLevin.Correctness or Tidy.Run.

Net: +188/−201 over 8 files. This is a refactor, not mathematical progress.

The survey also suggested bundling the OR-compression hypotheses into an IsORCompression structure. That item is dropped: compl_mem_NPPoly_of_orCompression needs (enc a).length = n, while the coNP and PH consequences need ≤ n, so a single structure would either weaken the first theorem or not fit the second.

Manual impact. Operator's Manual: parameterized-complexity.md now introduces FPTHard and names FPTHard.subset_FPT/FPTHard.fptReducible in place of the deleted WHard.* lemmas. Agent Operator's Manual: no edit needed; it names none of these declarations. ROADMAP.md, results/ and CslibFrontierResults/ don't reference them either.

Validation. At 777ca29109, based on b91d5151fd:

• lake build --wfail --iofail on the changed modules and every direct importer: Parameterized.{Hardness, WHierarchy, WHierarchy.XP, WHierarchy.Clique, WHierarchy.Clique.Graph, WHierarchy.IndependentSet}, Classes.NP.StrictVerifier, Fagin.{Converse, Ordered, SAT, Ordered.Verifier}, ImmermanVardi, NL ⊆ FO(TC) converse, CslibFrontierResults.Entries, and the tests Fagin, OrderedFaginVerifier, WHierarchy, WHierarchyClique and WHierarchyXP.
• lake exe mk_all --check.
• scripts/check_operator_manual.py.
• scripts/proof_copies.py --base origin/main.

Hosted CI runs the full validation. The PR is independent of #4757; the two touch adjacent but separate import lines of Fagin/Converse.lean.

AI assistance. Jetski worker session 1c3a6893, plan #4737.

Part of #4737

[SamuelSchlesinger]

Agent review (Jetski reviewer session b0a2721e-b109-4df0-b889-ff48fb783bb3) of 777ca29: approve. This is agent review, not human review.

FPTHard. The body of FPTHard is the same as the old WHard/WPHard bodies with the class abstracted out, so WHard t := FPTHard (@W t) and WPHard := FPTHard @WP keep their statements. wHard_iff/wPHard_iff still unfold it, which justifies exposing FPTHard. The three generic lemmas are exactly the four deleted ones with the class abstracted, and WPHard.wHard is now hB.mono. Dot notation resolves through the abbrevs: Clique_wHard.fptReducible, Clique_wHard.subset_FPT, WeightedCircuitSAT_wPHard.subset_FPT and the cross-module test hB.subset_FPT in CslibFrontierTests/WHierarchy.lean all build in hosted ci-checks. #4670's diff to WHierarchy/Clique.lean and the tests only changes the encoding and parameter arguments of WHard 1 …. Its call sites are the same dot-notation uses and merge without conflict with this PR, so they keep compiling. No open PR adds a use of the deleted names, Fagin.StrictVerifier, or the two CookLevin theorems (I grepped the added lines of every open PR's diff).

strictVerifier move. The old file is deleted with no shim. The only importer, Fagin/Converse, and the aggregate are updated. The moved declarations are unchanged. The two deleted CookLevin theorems had no users, and their hypotheses were stated in terms of tidy machines, a proof device. Converse already proves the same step for ordinary machines. Converse still gets CookLevin.tableau_satisfiable_iff through Fagin.Tableau.Defs. I also checked the merge with #4757: there is no conflict, and the merged Converse resolves runFrom_of_le and output_eq_of_halted through Run and Halting.Basic, not through the dropped transitive imports.

Manuals. The parameterized-complexity.md edits are accurate. I agree no Agent Operator's Manual edit is needed, and nothing in ROADMAP.md, results/ or CslibFrontierResults/ refers to the changed names. The advisory notices for this head (parallel-definition, duplicate-statement, repeated-proof-block) report no candidates.

Non-blocking, for one small follow-up after #4670 lands (it touches the Clique_wHard.fptReducible line that #4670 owns):

• Every sibling hardness notion names its transfer lemma .trans: PolyTimeHard, LogSpaceHard, NPHard, SearchHard, SharpPHard, LevinHard and HardUnder. Elsewhere in Parameterized/, .fptReducible names lemmas that produce an FPTReducible (e.g. IsKernelization.fptReducible). FPTHard.trans would match.
• The module docstring calls FPTHard "the parameterized counterpart of PolyTimeHard", but PolyTimeHard is a HardUnder instance and FPTHard is not. One sentence would say why: parameterized classes are indexed by a parameter as well as an encoding, so a HardUnder instance would need problems packaged as (parameter, set) pairs.