Repository navigation
refactor(problems): unify graph ordering and cover verifiers in Graph toolkit - #828
Merged
SamuelSchlesinger merged 1 commit intoOct 24, 2026
Merged
Conversation
… toolkit Complete the remaining Wave 2, Item 4 (`refactor(problems): one graph toolkit`) and Item 2 graph cleanups from #610: - Move `Graph.enumeratesBool`, `Graph.enumeratesBool_eq_true_iff`, `Graph.decodeVertexList`, `Graph.exists_decodeVertexList_eq`, `Graph.verifyOrdering`, `Graph.isVerifier_verifyOrdering`, `Graph.computableTidilyInPolyTime_decodeVertexList`, and `Graph.computableTidilyInPolyTime_verifyOrdering` (with a `private` `computableTidilyInPolyTime_enumeratesBool`) from `Problems/Hamiltonian.lean` into `Problems/Graph.lean`. - Build `GraphIsomorphism.verifier`, `GraphIsomorphism.isVerifier`, and `GraphIsomorphism.computableTidilyInPolyTime_verifier` in `Problems/GraphIsomorphism.lean` from `Graph.verifyOrdering`, moving the permutation-matrix row decoder `image` (and its `private` lemmas) into `Classes/ArthurMerlin/GraphNonIsomorphism.lean` (`PublicCoin`) and removing `GraphIsomorphism.pairTest`. - Move `VertexCover.isUncoveredEdge`, `VertexCover.uncoveredEdges`, `VertexCover.isCover`, `VertexCover.isUncoveredEdge_eq_true_iff`, `VertexCover.mem_uncoveredEdges_iff`, `VertexCover.isCover_eq_true_iff`, `VertexCover.computableTidilyInPolyTime_uncoveredEdges`, and `VertexCover.computableTidilyInPolyTime_isCover` (with a `private` `computableTidilyInPolyTime_isUncoveredEdge`) from `Parameterized/VertexCover.lean` into `Problems/VertexCover.lean`, and express `VertexCover.verifier` and `VertexCover.isVerifier` via `subsetVerifier` and `isCover`. - Switch all remaining `SimpleGraph.fromRel_adj` client unfoldings in `Problems/` and `Parameterized/VertexCover*` to `Graph.toSimpleGraph_adj`. - Remove the dead `VertexCover.Buss.computableTidilyInPolyTime_distinctVertices` (`BussKernel.lean`) and duplicate `HamCycle.cities` alias (`TSP.lean`). Part of #610
Collaborator
Author
|
Independent Review (
Scope Verified
|
26 of 75 tasks
Collaborator
Author
|
Coordinator review claimed by |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
Collaborator
Author
There was a problem hiding this comment.
Coordinator verdict — coordinator-jetski-e5ce255c (non-authoring), with scripted source review by review-828-jetski-e5ce255c: approve 9d141d21; ci-checks passes.
The moved verifyOrdering/isCover toolkit declarations keep their statements and proofs. Two fun_prop helpers became private with local fun_prop. Only dead or duplicate declarations were removed (pairTest, HamCycle.cities, Buss.computableTidilyInPolyTime_distinctVertices), and all clients are updated. The GraphIsomorphism and VertexCover verifiers are rebuilt, but their public isVerifier/mem_NP statements and the problem definitions are unchanged, so the NP results keep their meaning. The new GI test certificates decode correctly, including a vertex list with duplicates. The completion claim matches the #610 item 4 and item 2 checklists.
Record fixes, no new review needed:
- The tidy-surface reduction is −5 (39 → 34 across these files), not −3.
- Note that
Graph.toSimpleGraph_adjis deliberately not@[simp](per #689), although #610's checkbox asks for@[simp].
Nits, optional:
GraphIsomorphism.lean:164-204writes the characterising set twice (hmem/hset). It could be a publicmem_GraphIsomorphism_iff_exists_ordering.- The ~140 lines of ordering-verifier tooling in
Problems/Graph.leancould live inProblems/Graph/Ordering.lean, so that Coloring, Clique and the other problems that don't use it skip the rebuild. GraphNonIsomorphism.PublicCoin.imageis a very generic public name.
Enqueuing.
Merged
2 tasks done
This was referenced Oct 24, 2026
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 24, 2026
…le docs After regenerating the sweep on fresh main: `distinctVars` certificates come from `SAT` (#826), the graph non-isomorphism protocol keeps main's private `image` rule (#828), one long line is reflowed, the TreeEval and USTCON reader docs no longer call their now-plain certificates tidy, and the S3 baseline is lowered again (Classes: 590 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 24, 2026
…le docs After regenerating the sweep on fresh main: `distinctVars` certificates come from `SAT` (#826), the graph non-isomorphism protocol keeps main's private `image` rule (#828), one long line is reflowed, the TreeEval and USTCON reader docs no longer call their now-plain certificates tidy, and the S3 baseline is lowered again (Classes: 590 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Oct 24, 2026
…S2) (cslib-community#854) * refactor: state PCP verifier component efficiency plainly Manual-first Classes proposal for456. Only PCPVerifier.PolyTime changes: coins/queries/verdict predicates become ComputableInPolyTime with exactly the same encodings, including binary coins and addresses. Existing consumer statements and all algorithms/bounds are preserved, with proof-local ordinary bridges. Focused strict PCPNP/ClassClosure/PCPEncodedVerifier/PCPVerifierProbability clients and source modules pass6760jobs; hygiene/simp and preservation checks pass. This is not the Classes sweep or a public-boundary completion claim. (cherry picked from commit f4e2475) (cherry picked from commit 6829e280bb1313693a13ef7bcee96d5af1ce2987) * refactor: simplify PCP abstract bridge over plain verifier components Necessary seventh caller for the manual Classes field proposal. Every bridge/abstract definition and public theorem header is unchanged; remove six obsolete tidy conversions only. Actual strict three-root build passes13029jobs, PCP abstract audit is checked in that build, catalogue check14abstracts19headlines passes, rendering unit tests23 pass. Independent clean-main PCPAbstract rebuild6694jobs and new-source elaborated display/type dumps for all24 bridge/abstract declarations are byte-identical. No headline, catalogue or rendering-input change; no PDF visual-identity claim. (cherry picked from commit 440a91c) (cherry picked from commit d1693d2da94e5d670fefa9113a4ed28c3f3c8b6f) * refactor(classes): restate the Classes certificates plainly (tool output) Output of `scripts/tidy_sweep.py rewrite --area Classes --verify --rounds 8`, run through a wrapper that renames, instead of deferring, the references the tool cannot convert mechanically (partial applications, conclusions that are not bare predicates, tactic lemma lists, dot notation on tidy receivers), and lists them for hand fixes. 549 case-2 declarations: 16 deferred, 206 translated, 327 wrapped. This commit does not build on its own; the next commits complete it by hand. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): hand-complete the Classes restatement Hand fixes after the tool output: call sites that the rewrite could not convert (partial applications, non-bare conclusions, dot and field notation), translated proofs that need the tidy calculus, and tidy `fun_prop` proofs that used a restated composition rule. Those proofs get proof-local tidy certificates: explicit `have`s, or private `@[local fun_prop]` tidy views of the plain rules. The FPT family is plain (`ComputableInFPTTime.ite`/`.comp`, `ComputableInPolyTime.computableInFPTTime`, `ComputableInO.computableInFPTTime`, `mem_FPT_iff_computableInFPTTime`); the raw `ComputableTidilyInFPTTime`, its bridges and `isKernelization_iff_tidy` are removed. The three uncharged BigO endpoints are restated on `ComputableInBigO` with the same bounds. Tests state the restated API plainly. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): restate the remaining deferred Classes certificates TimeConstructible/SpaceConstructible.computableInO, DecidableInTimeO.exists_computableInO, ComputableInPolyTimeWithOracle.computableInPolyTime and .exists_computableInO, Interaction.computableInPolySpace_evaluate, SharpP/GapP.computableInPolySpace, ComputableInO.computableInPolyTime_take and ComputableInPolyTime.bitsEnumList_of_polyBounded: same functions, encodings and bounds, with the tidy machinery inside the proofs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): retire the class and reduction tidy bridges The 24 public bridges between plain and tidy class membership and reductions (`mem_X_iff_tidy` for twenty classes, `polyTimeReducible_iff_tidy`, `parsimoniousReducible_iff_tidy`, `polyTimeTruthTableReducible_iff_tidy`, `searchReducible_iff_tidy`) are removed: the classes and reductions are stated plainly and their `mem_X` lemmas are plain, so proofs that build tidy certificates convert them with `.of_tidy`, and proofs that destructure plain memberships take `.tidy` locally. Module docs no longer list the bridges, and name the plain twins of the remaining case-1 composition rules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): reflow, review docs and lower the tidy surface baseline Lines the restatement pushed past 100 characters are reflowed, docstrings of restated declarations no longer call their certificates tidy, the SAT to CircuitSAT reduction uses a plain certificate, axiom guards whose messages now fit one line are whitespace-lax, and the S3 baseline is lowered: the Classes area goes from 597 tidy statements in 179 modules to the 5 case-1 originals in 3 modules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): follow main's CNF and graph refactors, review module docs After regenerating the sweep on fresh main: `distinctVars` certificates come from `SAT` (cslib-community#826), the graph non-isomorphism protocol keeps main's private `image` rule (cslib-community#828), one long line is reflowed, the TreeEval and USTCON reader docs no longer call their now-plain certificates tidy, and the S3 baseline is lowered again (Classes: 590 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * test(classes): plain fun_prop over restated Classes certificates Client examples for automation parity: plain `fun_prop` composes the plain Buss-kernel, Sipser–Lautemann and Clique certificates with plain hypotheses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): follow the Wave 5 names and MINKT after regenerating After regenerating on main with cslib-community#835 and cslib-community#817: `MINKT.mem_NP` uses the plain `computableInPolyTime_check`, and lines that the Wave 5 names pushed past 100 characters are reflowed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): follow cslib-community#843, cslib-community#844 and cslib-community#848 after regenerating After regenerating on main with cslib-community#842, cslib-community#843, cslib-community#844, cslib-community#848, cslib-community#849 and cslib-community#850: `SharpPWithOracle.add_mem` (cslib-community#843) takes the plain all-false certificate through `ComputableInPolyTime.computableInPolyTimeWithOracle`; the ETH lower bounds of cslib-community#844 use the plain `SAT.toThreeColoring` and `toBinary` certificates and `DecidableInTimeO.exists_computableInO`; the TreeEval instantiation tests of cslib-community#848 instantiate the plain `ComputableInBigO` endpoints and state plain `ComputesInTimeAndSpace`; and the S3 baseline is lowered (Classes: 589 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Completes the remaining Wave 2, Item 4 (
refactor(problems): one graph toolkit) and Item 2 graph cleanups from #610 (refactoring only; no new mathematical endpoints):Problems/Graph.lean,Problems/Hamiltonian.lean): MoveGraph.enumeratesBool,Graph.enumeratesBool_eq_true_iff,Graph.decodeVertexList,Graph.exists_decodeVertexList_eq,Graph.verifyOrdering,Graph.isVerifier_verifyOrdering,Graph.computableTidilyInPolyTime_decodeVertexList, andGraph.computableTidilyInPolyTime_verifyOrdering(with aprivatecomputableTidilyInPolyTime_enumeratesBool) fromProblems/Hamiltonian.leanintoProblems/Graph.lean.Problems/GraphIsomorphism.lean,Classes/ArthurMerlin/GraphNonIsomorphism.lean,ComplexityTests/InteractiveProofs.lean): BuildGraphIsomorphism.verifier,GraphIsomorphism.isVerifier, andGraphIsomorphism.computableTidilyInPolyTime_verifierfromGraph.verifyOrdering(decoding an ordering of the second graph's declared vertices in unary blocks and checking length and adjacency preservation), move the permutation-matrix row decoderimage(and itsprivatehelper lemmas) intoGraphNonIsomorphism.PublicCoin, and removeGraphIsomorphism.pairTest.Problems/VertexCover.lean,Parameterized/VertexCover.lean): MoveVertexCover.isUncoveredEdge,VertexCover.uncoveredEdges,VertexCover.isCover,VertexCover.isUncoveredEdge_eq_true_iff,VertexCover.mem_uncoveredEdges_iff,VertexCover.isCover_eq_true_iff,VertexCover.computableTidilyInPolyTime_uncoveredEdges, andVertexCover.computableTidilyInPolyTime_isCover(with aprivatecomputableTidilyInPolyTime_isUncoveredEdge) fromParameterized/VertexCover.leanintoProblems/VertexCover.lean, and expressVertexCover.verifierandVertexCover.isVerifierviasubsetVerifierandisCover.Graph.toSimpleGraph_adj& dead/duplicate graph declarations: Switch all remainingSimpleGraph.fromRel_adjclient unfoldings inProblems/andParameterized/VertexCover*toGraph.toSimpleGraph_adj, remove the deadVertexCover.Buss.computableTidilyInPolyTime_distinctVertices(BussKernel.lean), and remove the duplicateHamCycle.citiesalias (TSP.lean,ComplexityTests/NPCompleteGraphs/TSP.lean).Part of #610
Validation
LEAN_NUM_THREADS=4 ./scripts/check.sh(all 6 gates:build --wfail --iofail,mk_all --check,test --wfail --iofail,lint,lint-style,checkInitImports)python3 scripts/check_tidy_surface.py(reduced by 3 public tidy statements across the modified modules)python3 scripts/check_hygiene.py --check-simppython3 scripts/build_abstracts.py --check(14 abstracts and 19 headline theorems unchanged)AI Disclosure
Authored by
worker-jetski-5950b838(Gemini) and independently reviewed at9d141d21be2a9a62f03d0902320f94b42dc8e692byreviewer-jetski-graph-toolkit-610(4495ed73-23c9-4b5a-8847-6312c7c968a7).