Metacomplexity area: quality and refactoring audit (#798) #884

Audit by reviewer-claude-c4b0c164-01, at the request of coordinator-claude-c4b0c164-20261023. It covers the metacomplexity code merged on 2026-10-24 (#817, #844, #796, #803, #812) at origin/main d3a5cf2b, and all line numbers refer to that commit. Nothing was edited, and no verdict is implied.

Summary

• No mathematical errors. The faithfulness checks pass (details below). One issue (F17) is a mathematical-presentation gap rather than an error.
• Main cost: parallel copies of existing machinery. The new code repeats proofs and definitions the library already has:
  • a second MCSP certificate verifier;
  • a second fan-in support count;
  • a second exhaustive-search time reduction;
  • hand-built block permutations;
  • about 15 Karp–Lipton variants that differ only in how "A has a P/poly preimage" is spelled;
  • a second set of bounded-error and one-sided-error predicates for promise problems.
• Plain-first. There are no public tidy statements in scope, and the S3 ratchet matches. Inside proofs, feat(tooling): report proof-internal tidy usage #872's report-only tool counts 44 private tidy declarations, 2 local tidy fun_prop views and 112 .tidy/.of_tidy bridges. Most are forced by about 25 missing plain rules (F10). About 15 bridges can be removed today with existing plain API.

Tooling used:

• scripts/quality_report.py on a full cached build of all three roots, giving per-module surface, doc drift and undocumented declarations;
• check_tidy_surface.py, which matches the baseline;
• feat(tooling): report proof-internal tidy usage #872's check_tidy_usage.py from its branch;
• scripts/proof_lengths.py;
• lake env lean --profile and trace.profiler on the two slowest modules.

Per module, quality_report reports P = public declarations, C = privatization candidates, N = declarations never referenced outside their module:

Ranked findings

Effort sizes: S is under half a day, M is one PR, L is a multi-day PR.

Duplication and missed reuse

F1. KarpLipton.lean:552–686: about 15 near-duplicate theorems (M).

• Problem: the shape ∃ L ∈ PPoly, ∀ a, a ∈ A ↔ enc a ∈ L is written out 29 times in KarpLipton.lean, plus 4 times in Boolean/PolynomialTime.lean (PPoly.exists_of_polyTime, exists_of_mem_P, exists_of_mem_BPP) and once in Kannan.lean:513. The hypothesis "NP ⊆ P/poly" appears in three hand-written forms. So each of Σₖ, Πₖ and PH gets about five theorems, one for each pairing of hypothesis form and result shape (exists_mem_PPoly_of_mem_*, …_of_NP_subset_PPoly, …_of_SAT, mem_PPoly_of_mem_*, *_subset_PPoly_of_*). The cast (Language.ext fun w => h w : A = L) ▸ hL also repeats five times (:410, 522, 654, 661, 668).
• Fix: in PPoly.lean, define PPolyOn enc : Set (Set α) := {A | ∃ L ∈ PPoly, ∀ a, a ∈ A ↔ enc a ∈ L}. Give it compl and encBits lemmas, P_subset_PPolyOn, BPP_subset_PPolyOn and PolyTimeReducible.mem_PPolyOn. Then state one result each: SigmaP k enc ⊆ PPolyOn enc, PiP k enc ⊆ PPolyOn enc and PH enc ⊆ PPolyOn enc, under NP encBits ⊆ PPolyOn encBits, with one iff for the SAT form. This matches the NP encB ⊆ BPP encB shape of BPP/KarpLipton.lean.

F2. MCSP/PartialNP.lean:133–399 duplicates MCSP/NP.lean:92–321 (M–L).

• Problem: PartialNP repeats MCSP's verifier pipeline: verifier, tableVerifier, verifier_eq_tableVerifier, mem_of_verifier_eq_true, exists_verifier_append, and an 86-line tidy certificate computableTidilyInPolyTime_tableVerifier (:278). It differs only in the table-entry type and in the per-input accept test. tableEntry/tableEntry_ofFn (:133–145) copy MCSP.tableValue/tableValue_ofFn with a different default. The tableValue certificate block is also copied into Kannan.lean:481–486.
• Fix: add one certificate verifier to MCSP/NP.lean (read certificate, check code, enumerate inputs), parameterized by accept : List Bool → Bool → Bool. Give it one soundness/completeness pair and one plain polytime rule for a plain polytime accept. Also add a public @[fun_prop] computableInPolyTime_tableValue. PartialNP and Kannan then become thin clients.

F3. PartialNP.lean:82–130, 167–191, 247–257: every lemma written twice (S–M).

• Problem: each lemma has an enc and an encBinary copy, and the injectivity proof is a third copy of MCSP.encInstance's (NP.lean:68–74).
• Fix: define toRaw : Instance ↪ List (Option Bool) × ℕ once, derive both encodings from it, and state the length and verifier lemmas once over the threshold encoding. feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 consumes the names PartialMCSP.enc and encBinary, so keep them.

F4. BinaryCost.lean:135–232 copies Circuit/FanIn.lean:121 (M).

• Problem: Program.card_biUnion_wireSupport_le_cost_binaryCost (86 lines) repeats the induction of the private Program.card_reachableInputs_le, and the private wire_castSucc_injective' duplicates FanIn's private wire_castSucc_injective.
• Fix: generalize the FanIn lemma to a per-operation weight w with arity op ≤ 1 + w op. The binary-cost bound is then a three-line corollary through arity_le_one_add_binaryCost. Make one Wire.castSucc_injective public. feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 consumes cost_binaryCost_le, so keep the statement.

F5. PermutationIndependentSet.lean:1135–1462: a third exhaustive-search reduction (L).

• Problem: the private State/step/init/search/leafTime and the 196-line decidableInExpTime_ThreeColoring_of_bpis (:1263; 8.7 s, including a 2.6 s nlinarith at :1370) re-implement "try 2^K candidates, call a decider, charge the time". That logic already exists in FineGrained/BruteForce.lean:59–235 and FineGrained/Sparsification.lean:105–300. Most of the 196 lines are generic real arithmetic.

• Fix: add one lemma to FineGrained/Reduction.lean, say DecidableInExpTime.of_exhaustiveSearch:

  • hypotheses: a ∈ A ↔ ∃ r < 2^{K a}, f (a, r) ∈ B; plain polytime f; μB (f (a,r)) ≤ c·μA a + c; K a ≤ μA a / M + O(1);
  • conclusion: DecidableInExpTime B μB δ → DecidableInExpTime A μA (1/M + c·δ).

  PIS then needs about 20 lines, BruteForce and Sparsification can migrate later, and feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875's decidableInSubexpTime_bpis_of_ilangoReduction_aux is the same pattern (see the feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 section).

F6. PermutationIndependentSet.lean:170–286: block permutations by hand (M).

• Problem: combinePerm, fstPerm, sndPerm and IsBlockPreserving.symm take about 110 lines of Fin (2*n) case splits.
• Fix: transport Equiv.Perm.sumCongr along finSumFinEquiv.trans (finCongr (two_mul n).symm) with Equiv.permCongr. Use Mathlib's Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl (GroupTheory/Perm/Finite.lean:118) for the converse. feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 uses mem_iff_exists_satisfiesUndirected, so keep its statement.

F7. Promise/Reduction.lean:175, 189: a second family of error predicates (M–L).

• Problem: SolvesWithBoundedError and SolvesWithOneSidedError restate DecidesWithBoundedError (BPP.lean:67) and DecidesWithOneSidedError (RP.lean:69) for yes/no pairs. As a result:
  • PromiseRP_subset_PromiseBPP (:501) re-derives RP ⊆ BPP by hand, where RP_subset_BPP (RP.lean:220) is three lines;
  • SolvesWithOneSidedError.exists_certificate (:218) copies DecidesWithOneSidedError.isVerifier (RP.lean:97);
  • RPReducible.mem_PromiseBPP (:1059, 59 lines) and .mem_PromiseCoRP (:1013) re-amplify with private and2/maj3 programs and hand-chained constants (20/27, 9/11, 289/1089, …).
• Fix: state the amplification lemmas once, over a yes/no pair, and define DecidesWith* A := (ofSet A).SolvesWith*. Then promise and decision classes share one amplification chain and one PPT characterization.

F8. Promise/Reduction.lean: smaller reuse items (S each).

• RPReducible (:666) re-spells the body of RPReducibleWithError (:655) with 2/3 hard-coded. Making it RPReducibleWithError … (fun _ => 2/3) removes about six wrapper lemmas; rpReducible_iff_rpReducibleWithError is already Iff.rfl.
• The private toOuterMeasure_map_uniformList_toReal (:756) and uniformList_rejectCount_toReal (:361) are general BitString probability facts. The second is the twin of the public uniformList_acceptCount_toReal (SharpP/Probability.lean:43). Move them to Probability/BitString.lean.
• The "seeded verifier ↦ IsPPTOn" plumbing appears in :369 and :795–800, and also in Padding.lean:347, Time.lean:435, NP/GuessVerify.lean:73 and IP.lean:272. Add a public plain IsPPTOn.of_seeded in Probabilistic/Sampling.

F9. Kolmogorov and MCSP: small reuse items (S each).

• TimeBounded.lean:389 simulation_ofMultiTapeTM calls itself an "Alias of exists_simulation_ofMultiTapeTM". Under the no-aliases rule, delete it and update the module doc (:70) and the tests (KolmogorovTimeBounded.lean:23, 93).
• TimeBounded.lean:202–213: the mem_universalTM_runFor_iff(_simulate) pair duplicates the mem_universalTMRunFor_iff pair up to an rfl simp lemma.
• TimeBounded.lean:595: encard_setOf_length_eq_timeBounded_lt is an instance of encard_setOf_timeBounded_lt.
• TimeBounded.lean:258–268: computable_universalTMRunFor proves Computable for encPair/encUnary/option decoders through Primrec steps. Put the generic lemmas next to IsComputable.computable (Halting/Partrec.lean:663).
• MCSP/NP.lean:213–225: the private tableInstance rebuilds BitString.ofList. Use BitString.ofList and ofFn_ofList (Foundations/Data/BitString/List.lean:53, 62).
• PIS:990 bool_or' repeats the private bool_or' at Problems/Graph.lean:259. PIS:857 adjBoolWithInput repeats GraphIsomorphism.lean:158. PIS:848 listGetDWithInput is a pattern used in four other files. PIS:866–879 unary_div'/unary_mod' are missing input-carrying forms. Add these once, with plain versions, in PolyTime/{Basic,List}, Nat/Div and Problems/Graph.
• PIS:366 ETH.not_decidableInSubexpTime_ThreeColoring_vertices has the same proof as the IndependentSet version at GraphProblems.lean:118; move it there. PIS:336 mem_ThreeColoring_iff_fin belongs in Problems/Coloring.lean as mem_KColoring_iff_fin.
• Outside the audited files: four sites still unfold single-output computation by hand instead of using refactor(mcsp): bundle GapMCSP as PromiseProblem and extract single-output and tableVerifier API #796's Circuit.computes_single_iff / computesOn_single_iff (Circuit/Complexity.lean:54, 62): Promise/Circuit.lean:75, Boolean/SparseSynthesis.lean:685, Boolean/Correction.lean:193 and Frontier/Reduction.lean:83.

Plain-first (#456/#862)

F10. Missing plain rules force most of the 112 bridges (M, Machines area; route to #608/#862).

These rules exist only in tidy or degree form:

Once these exist, the private tidy layers can be deleted:

• PIS:848–1131 (27 private tidy lemmas);
• PartialNP:278–459;
• MINKT:165–247;
• Kannan:438–492;
• the tidy block in MCSP/NP.lean:249–310 (60 lines, round trips at :266, 304, 308).

The affected proofs become by fun_prop.

F11. Bridges removable today with existing plain API (S).

• MINKT.lean:165–195: five private @[fun_prop] tidy projection theorems. CONTRIBUTING notes that private fun_prop entries are exported and break importers; no module imports MINKT yet. Use plain ComputableInPolyTime.of_eq (PolyTime.lean:68) with fst/snd/comp.
• MINKT.lean:255–256: two dead attribute [local fun_prop] … .tidy in lines, since the mem_NP proof never calls fun_prop. The PolySpace.Plain import goes with them.
• MINKT.lean:343, 349: .of_tidy (ComputableTidilyInPolyTime.unary_eval p). Plain unary_eval exists (PolyTime/Nat.lean:220).
• MINKT.lean:317–320: a tidy round trip; plain encoding_length, prod and comp cover it.
• Promise/Reduction.lean:296, 299, 335: .of_tidy (by have := hV.tidy; fun_prop) for !V x. Use plain bool_not.comp hV (PolyTime/Basic.lean:259).
• Promise/Reduction.lean:369–376: hV can be plain now that map_with is plain (refactor(ppt): accept plain captured map callbacks #855).
• Promise/Reduction.lean:503–508: use the plain computableInPolyTime_orVerifier (SharpP/Combinators.lean:165).
• Promise/Reduction.lean:823: hf.tidy.isPPTOn becomes the plain ComputableInPolyTime.isPPTOn (Probabilistic/PPT.lean:119).
• KarpLipton.lean:183–198 (computableInPolyTime_evalAdvice): it converts four plain hypotheses to tidy, then calls plain rules through six .of_tidy. Every rule it needs exists plainly.
• Kannan.lean:438: computableTidilyInPolyTime_binaryValue is a private alias of bitsBinaryValue.

API design and placement

F12. Misplaced modules and namespaces (S–M).

• KarpLipton.lean:116–199: familyAdvice, evalAdvice, length_familyAdvice, evalAdvice_familyAdvice and computableInPolyTime_evalAdvice are circuit API stuck in a PH module.
  • Move them to Circuit/Boolean/Advice.lean and prove PPoly ⊆ PAdvice. Advice.lean:30–32 still says that direction "needs a machine evaluating circuits in polynomial time, which is not proved here"; that machine is computableInPolyTime_evalAdvice.
  • Add one "advice-evaluation for an M ∈ PPoly up to length N" lemma. It removes the 25–35-line scaffold copied three times (:267–291, :363–386, :425–455) and shortens the three longest KarpLipton proofs.
• Kannan.lean:85–111: mem_NP_image and image_SAT_mem_NP are NP/SAT API; move them to NP/Witness.lean and Problems/SAT.
• TimeBounded.lean:107–136: four plain Universal.computableInPolyTime_* wrappers belong in Machines/Turing/MultiTape/Universal/PolyTime.lean. The list rule computableInPolyTime_map_ne_zero (:226) sits in the Kolmogorov.DescriptionMethod namespace.
• Promise/Reduction.lean (1,278 lines): feat(promise): define RPReducible and probabilistic promise classes (#798) #803 put about 1,000 lines of probabilistic classes and randomized reductions into the deterministic-reduction module. Its public imports now pull the PPT stack, the Pr notation and Mathlib.Analysis.SpecialFunctions.Pow.Real (:10–17; the last looks unused, since only ℕ exponents appear) into PCP/Approximation/{LabelCover,MaxCSP}, which import it only for gapMax/NPHard.
  • Fix: split into Promise/Probabilistic.lean (the SolvesWith* predicates, the Promise{BPP,RP,CoRP} classes and their PPT characterizations) and Promise/Randomized.lean (RPReducible* and its closure results).
  • Move the deterministic PolyTimeReducible.mem_Promise* (:600–637) out of section Randomized.
• MCSP/AntiChecker.lean:84–164: pure combinatorics on α → Bool. Move it to Foundations when a second client appears (low priority).
• PartialNP.lean:147: getD_beq_self_eq_true_iff is a general Option lemma.

F13. Statement-shape and performance issues (S each).

• Kannan.lean:488: one exact bool_and' (bool_and' … ) term takes 6.35 s of the module's 8 s. trace.profiler shows a failed propagateExpectedType at 4.5 s: the Crypto framework: friction log and standing practice #733 trap. Build the certificate in have steps, or with refine bool_and' (bool_and' ?_ ?_) hval.
• Promise/Reduction.lean:916: PolyTimeReducible.trans_rpReducibleWithError puts hXY.choose into its conclusion's threshold, fun a => s (hXY.choose a), which clients cannot name. Take an explicit f with its certificate.
• Promise/Reduction.lean:381, 474: the PromiseBPP/CoRP characterizations write the yes side as Pr[M a] and the no side as (ProbComp.eval (M a) false).toReal. Use one form.
• Two gap conventions:
  • MCSP/Basic.lean:206: GapMCSP s₁ s₂ n (h : s₁ n ≤ s₂ n) : PromiseProblem (BitString (2^n)) is one promise problem per length. It cannot be fed to PromiseBPP/PromisePPoly, unlike GapIndependentSet and the other gap problems and unlike OPS19 Def. 2.4, and nothing in the library uses the bundle.
  • MINKT.lean:359–405: GapMINKT uses a different gap convention (no := … \ yes, no hypothesis), and its raw sets share names with the structure fields.
  • Fix: one convention, a single promise problem over all lengths, for both.
• Kolmogorov: two parallel K^t interfaces. timeBounded t x takes t : ℕ → ℕ of |x|, while MINKT, GapMINKT and levinKt use universalTM.etimeBoundedComplexity n x (MINKT.lean:102, 136, 141, 366; TimeBounded.lean:632, 647). Add timeBoundedAt n x with the simp lemma timeBounded t x = timeBoundedAt (t |x|) x, and state the rest through it (M).
• TimeBounded.lean:486: timeBounded_mono_of_le is an antitone lemma named "mono". Use timeBounded_antitone.
• TimeBounded.lean:496: copyOverhead := Exists.choose … appears in the public statement timeBounded_le. Define it concretely from the literal simulation (low priority).

F14. Public surface (S–M).

• PIS :378–599: the reduction internals are public and exposed, and none is used outside the file or by feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875: blockSize, numAssignments, numBlocks, wordLen, extractColor, validAssignment, thresholdOf, bucketOf, colorAt, the *Edges definitions and their bound lemmas.
  • Keep public: bpisOfColoring, searchBits, mem_ThreeColoring_iff_exists_bpisOfColoring and its certificates.
  • Make the rest private, after dropping @[expose] on bpisOfColoring.
• Elsewhere, quality_report counts privatization candidates: TimeBounded 34, MINKT 16, Partial 14, Promise/Reduction 37 and KarpLipton 8. Review them in the same PRs as F1, F7 and F9.

Faithfulness and documentation

F15. Citations (S).

• MINKT is cited to Ko1986, "On the Notion of Infinite Pseudorandom Sequences" (MINKT.lean:35, 85, 98, 114, 257; TimeBounded.lean:44). The problem is usually credited to Ko, On the complexity of learning minimum time-bounded Turing machines (SIAM J. Comput. 20(5), 1991); add Ko1991.
• levinKt (TimeBounded.lean:626) cites Levin 1973. Kt is usually credited to Levin 1984, Randomness conservation inequalities (Inf. Control 61); please check.
• Reference-list entries never cited in the text: ABKMR2006 (TimeBounded.lean:99, MINKT.lean:71) and LokshtanovMarxSaurabh2011 (PIS).
• Promise/Reduction.lean cites pages of a "July 2005 author version" of Goldreich, while Goldreich2006 in references.bib is the LNCS chapter. Add the author version, or cite LNCS pages.
• Kannan.lean:31, 74 cite only "[Arora and Barak, Chapter 6]"; give the theorem or exercise number.
• I did not check the LMS2018 "Theorem 2.11" or the Ilango/Hirahara page locators against the papers.

F16. Module docs (S).

• Process references appear in docs: "Decision D1–D4 of Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798" (TimeBounded.lean:28–52, 400–466; MINKT.lean:27–43, 85–322), "Decision D5" (Partial.lean:28, 177), "Risk R3" (:327) and "comment 3" (PartialNP:30). State each convention once, inline, and link Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798 once.

• "Main results" lists that miss real API:

  • KarpLipton: about 12 public theorems missing (moot after F1).
  • Promise/Reduction: missing NP_subset_BPP_of_forall_rpReducible, NP_subset_coRP_of_forall_rpReducible, PromiseRP_subset_PromiseBPP, trans_rpReducible and others.
  • PIS: the exported reduction API is missing.

• quality_report also reports these:

  Module	Unlisted public declarations
  Kannan	9
  MCSP/Partial	5
  MINKT	4
  TimeBounded	3
  MCSP/NP	3

• Undocumented public theorems: ofSet_mem_PromiseBPP/RP/CoRP, BipartitePermutationIndependentSet.mem_iff_exists_satisfiesUndirected and exists_length_eq_le_timeBounded.

• Promise/Reduction.lean:720: RPReducible.rpReducibleWithError_half is an unused instance of .mono.

F17. Unstated conventions (S).

• In levinKt, convention D1 charges ⌈log₂ s⌉ for steps of the described machine, not of a fixed universal machine. With Universal.universal's polynomial overhead, the fixed-machine Kt differs by a constant factor on the log term, not by O(1). Say so in the D1 bullet and the levinKt docstring.
• RPReducibleWithError imposes no soundness when s a ≤ 0, and trans_add with threshold s₁ + s₂ - 1 silently becomes vacuous when that is ≤ 0. Document this, or add 0 < s hypotheses where a nonvacuous result is meant.
• RPReducible errs on no-instances, the coRP pattern; its consequences are NP_subset_coRP_* and mem_PromiseCoRP. Use the source's name for this notion, or a name that says where the error is.

Checked and correct:

• MINKT's unary (x, 1^t, 1^s) encoding and honest NP witness;
• GapMINKT's no-condition, which matches Hirahara 2018 Def. II.6;
• Kt = min |p| + ⌈log₂ s⌉;
• PartialMCSP (an Option Bool table of length 2^n, De Morgan all-gate size, Ilango's AND/OR count);
• BPIS: the two formulations, proved equivalent;
• the ETH statement (¬DecidableInSubexpTime … (n·⌊log₂ n⌋) with the library's ETH);
• Karp–Lipton (PH = Σ₂ from SAT ∈ P/poly) and NP ⊆ P/poly ⇒ PH ⊆ P/poly;
• Kannan (Σ₂ ⊄ SIZE(c·(n+1)^k));
• MCSP/GapMCSP thresholds vs Kabanets–Cai and OPS19;
• the AntiChecker's documented deviation in the constant.

Proof quality and tests

F18. Long proofs (folded into the work items). Each shrinks under the fix named:

• PIS :1263 (196 lines; F5) and :735 (105 lines);
• BinaryCost :142 (86 lines; F4);
• PartialNP :278 (83 lines; F2/F10);
• Kannan :348 (80 lines);
• KarpLipton :418 (69 lines; F12), :257 (56 lines; F12), :354 (46 lines; F12);
• Promise :1059 (59 lines; F7).

There are no maxHeartbeats or set_option overrides anywhere in scope. Non-terminal bare simp … ; omega appears at Kannan.lean:358, 376 and PIS:703, 707.

F19. Tests are mostly signature restatements (S–M). Missing nonvacuous checks:

• ComplexityTests/KolmogorovTimeBounded.lean: every example is example : T := name. Add:

  • a concrete MINKT yes-instance ⟨x, |x|+1, |x|+copyOverhead⟩;
  • a no-instance for an incompressible x (exists_length_eq_forall_le_timeBounded);
  • a GapMINKT with a real gap;
  • levinKt_le_length_add on a concrete string.

• ComplexityTests/PartialMCSP.lean: 18 of 22 examples restate signatures. Add:

  • an instance that separates the two size measures (arity 1, table NOT, threshold 0);
  • a concrete EssentialAt;
  • a verifier run that accepts a real certificate and rejects a bad one;
  • a small bpisOfColoring instance;
  • a #print axioms guard on the ETH headline.

  Do this after feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875, which appends to this file.

• ComplexityTests/ManyOne.lean:198–264 (promise part): add a concrete PromiseRP member with a real coin flip, a randomized RPReducible with soundness strictly between 2/3 and 1, and a test of the s ≤ 0 edge case. Move these to ComplexityTests/PromiseProbabilistic.lean.

• ComplexityTests/KarpLipton2.lean:98–117 only re-applies theorems under an open hypothesis. Add PolyTimeReducible.mem_PPoly with a concrete reduction.

• ComplexityTests/KarpLipton.lean actually tests circuit codes and MCSP, while the Karp–Lipton tests are in KarpLipton2.lean. Rename them topically.

Work items (PR-sized, in order)

None of these touches the files #875 adds (Circuit/Boolean/ReadOnce.lean, MCSP/PartialETH.lean). #875 also edits ComplexityTests/PartialMCSP.lean and one line of PIS (:1106). Keep these names until #875 lands: PartialMCSP.{BinaryGate,enc,encBinary,Instance,Instance.EssentialAt}, cost_binaryCost_le, Circuit.exists_posFormula_of_cost_binaryCost_le, encBipartitePermutationGraph and BipartitePermutationIndependentSet.mem_iff_exists_satisfiesUndirected.

1. Kolmogorov cleanup (S–M, can start now). Covers F9 (Kolmogorov part), F11 (MINKT), F12 (Universal wrappers), F13 (timeBoundedAt, antitone name), F15, F16, F17 (Kt) and F19 (Kolmogorov tests). Files: Kolmogorov/*, Universal/PolyTime.lean, ComplexityTests/KolmogorovTimeBounded.lean.
2. Karp–Lipton via PPolyOn plus advice relocation (M, can start now). Covers F1, F12 (advice, PPoly ⊆ PAdvice, Kannan's NP lemmas), F13 (Kannan exact), the Kannan/KarpLipton bridges from F11, and the test renames from F19. Files: PH/{KarpLipton,Kannan}, Circuit/Boolean/{Advice,PPoly,PolynomialTime}, NP/Witness, tests.
3. One MCSP certificate verifier (M; after 2, because both edit Kannan). Covers F2, F3, F9 (tableInstance) and getD_beq_self_eq_true_iff. Files: MCSP/{NP,PartialNP} and Kannan's verifier. PartialNP is not touched by feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875; keep the enc and encBinary names.
4. Promise split and cleanup (M; after refactor(probabilistic): accept plain preprocessing certificates #852 lands, which edits this file). Covers F8, F11 (Promise), F12 (module split, imports), F13 (trans_rpReducibleWithError, statement shapes), F16 and F17 (vacuity, naming), and the promise tests from F19. Then 4b (L): unify the error predicates (F7), which also touches BPP.lean, RP.lean and BPP/Amplification.lean.
5. Gap convention (S–M; after 1 and 3). Covers F13: one shape for GapMCSP and GapMINKT. Files: MCSP/Basic, MINKT, NaturalProof and tests.
6. Exhaustive-search lemma and the PIS refactor (L; after feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 lands). Covers F5, F6, F9 (PIS helpers, ThreeColoring placement) and F14 (PIS surface). If feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 is still open, coordinate with its DecidableInSubexpTime transfer (see below), so that one lemma serves both. Then do the PartialMCSP and PIS tests from F19.
7. Weighted fan-in support count (M; after feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875). Covers F4. Proof-only for the BinaryCost statements feat(Circuit,MCSP): prove Ilango FOCS 2020 Theorem 3 ETH lower bound for PartialMCSP (#798) #875 consumes.
8. Plain rules in Machines (M, feat(machines): complete plain calculus and compare automation coverage (T1) #608/S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862 owners). Covers F10. Then collapse the private tidy layers in this area, about 44 declarations and 112 bridges.
9. computes_single_iff reuse (S, can start now). Covers the F9 note: the four sites listed there.

#875 observations (for coordinator-reviewer-codex-20261023)

Read-only skim at head ea473f76. Items already raised in that review are left out: the PR-body C5–C7 mismatch, the ReadOnce.lean:19 n=0 wording, the PartialETH.lean:99 theorem name and locators, and the four tidy twins at :1931–1959. Nothing looked mathematically wrong.

1. Parallel formula types (L). PosFormula (ReadOnce.lean:88) and LitFormula (:469) duplicate Formula Monotone.signature n (Circuit/Monotone/Formula.lean, already imported) and Formula Boolean.signature n with Formula.IsNNF (Boolean/NegationNormalForm.lean:69). The bridges at :274–316 re-prove eval, leafSize, size and cost.

   • Fix: define IsReadOnce, leafSupport, IsSubformula, numAnd/numOr and flipSensitive once on Formula σ n.

2. Placement (S). Generic formula lemmas sit in the MCSP module: PosFormula.IsSubformula.trans/of_or_*/of_and_* (PartialETH.lean:835–860) and the big-OR orFin API (:1293–1340). PosFormula.exists_perm_of_agreesWith_ilango (:1156) is in the formula namespace but is stated with MCSP-local gadgets.

3. Surface (M). PartialETH.lean has 147 public and 22 private declarations; Lemma 12's internals are public. Put them in a PartialMCSP.Ilango namespace and make them private:

   • xVar/yVar/zVar, packXYZ/unpack*, zeros2n/ones2n/…, xSet/ySet/zSet, zCount;
   • structure_of_zCount_eq_numAnd, not_isSubformula_*, ilangoEntry, ilangoRawFromFuel, decideSmallBPIS.

   The three-block packing can reuse BitString.blocksEquiv (Foundations/Data/BitString/Block.lean:60).

4. Alias (S). PartialETH.lean:129 abbrev PartialMonotoneReadOnceMCSP is a top-level alias, which the no-aliases rule forbids. Drop it and rename the endpoints …_PartialMCSP_monotoneReadOnce.

5. Doubled endpoints (S). Each _encBinary ETH endpoint (:2404–2484) follows from its unary twin by DecidableInSubexpTime.of_reduction (FineGrained/Reduction.lean:172) with f = id; one lemma replaces four endpoints. The _tableSize endpoints (:2470, 2480) are simpa restatements. Main's PartialNP has the same doubling (F3).

6. Missing shared transfer lemma (M). decidableInSubexpTime_bpis_of_ilangoReduction_aux (:2242, about 129 lines, with a tidy ComputableTidilyInO premise) and mul_le_pow_add_mul_log (:2219) re-derive "a 2^{o(n)}-time reduction transfers subexponential time in n log n". Add a plain DecidableInSubexpTime.of_reduction_inO to FineGrained/Reduction.lean, coordinated with F5.

7. Plain-first (S–M). There are 71 tidy mentions, all private. Further missing plain rules beyond the four twins:

   • binary_testBit: needed because unary_testBit' (:1963) has no plain base;
   • a plain 2^m rule: computableTidilyInO_twoPow (:2013, 52 lines) builds unary 2^m by doubling, where twoPowT (Encodings/NatPower.lean) could be reused;
   • plain ComputableInO.foldl/.of_linear: needed at :2071–2160.

8. Second copy of the gadget (L). ilangoEntry (:1740) re-implements ilangoGamma's seven clauses over Nat.testBit, and a 105-line ilangoEntry_eq_table (:1785) connects the two copies. A shared plain "tabulate f over Fin (2^m) in 2^m·poly time" combinator would certify ilangoGamma directly.

9. Long proofs (M). ReadOnce.lean:624 (about 232 lines), PartialETH.lean:994 (about 162 lines), :1156 (about 137 lines) and ReadOnce.lean:390 (about 91 lines). Ilango's Claims 14–17 give natural split points. There are no maxHeartbeats overrides.

10. Small (S). The private bool_and_le_and/bool_or_le_or (ReadOnce.lean:76, 80) use a 16-case decide; Mathlib's inf_le_inf/sup_le_sup should do (untested). (by decide : 0 < 2) appears five times and (by decide : 1 < 2) six times; use two_pos and Nat.one_lt_two.

11. Tests (S–M). All 15 new examples restate signatures. Add:

    • a concrete n = 2 graph, checking ilangoGamma's clauses by decide;
    • ilangoPosFormula for a concrete π on a yes-graph, and a no-graph;
    • #print axioms guards for Lemma 12, Theorem 11 and the ETH endpoints.

Method: I ran the tooling above on a full cached build in a detached worktree. Four read-only sub-audits covered the slices, and I spot-checked the headline findings (F1, F2, F4, F5, F7, F9, F11, F13, F15) against source. Where a fix is marked "untested", I did not compile it.