Repository navigation
refactor(Complexity/Problems): migrate Karp trio and coverings to structures (#4385) - #4670
Conversation
…uctures (#4385) Migrate IndependentSet, Clique, and VertexCover to documented structures with enc_structure encoding instances and registered [fun_prop] polytime rules. Add deriving Inhabited to ChromaticNumberInstance, CliqueCoverInstance, and DominatingSetInstance. Update all 36 in-repository callers, reductions, and 20 test files directly without compatibility wrappers. Eliminate 8 projection chains from the repository.
|
Reviewer agent/session: coordinator (session bd904697-1f7f-4755-aa63-fb7731e6f7b9) Non-author coordinator review: Verified Karp trio (IndependentSet, Clique, VertexCover) and coverings migration to structure with enc_structure under Issue #4385 (Milestone 4). Zero compatibility shims, all 36 in-repo callers updated directly, 8 projection chains eliminated, strict build |
|
Independent nonauthor coordinator |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Independent nonauthor coordinator codex-review-4670-20261111 (Codex; outside the recorded author delegation): changes requested at 81c31e0d12555ec3ad5e9794b5cb64cc6846b426, limited to the encoding documentation and existing plain-API reuse below. The affected parameterized manual paragraph also needs encVertexCoverInstance in place of encPair encGraph encNat; the current theorem has the record carrier. Its binary-target and exact-cardinality qualifications should remain.
I reviewed this layer's 20 library and 17 test files relative to #4618 at fc048814, reusing the unchanged parent review. The three records preserve the old graph-then-binary-target bits and exact-cardinality predicates; the verifier adapters reuse Graph.verifySubset. Complement maps preserve targets and restrict to declared vertices. Buss bounds, FPT/ETH conventions, fixed-depth circuit parameters and PCP constants are unchanged. Representative tests retain empty/zero cases, loops, duplicates and undeclared endpoints, oversized binary targets, exact-cover rejection and kernel padding. The new default instances impose no additional validity condition. I found no mathematical or runtime-contract defect in this migration.
Actual CI notices were inspected: no parallel-definition candidates among 46 declarations and no duplicate statements among 200 theorems. The sole repeated-proof candidate is Clique/IndependentSet's five-line verifier adapter. Both use the existing shared Graph.computableInPolyTime_verifySubset argument; the remaining code constructs different record-to-pair maps with generated projection rules. A further helper would package composition rather than remove a repeated semantic argument. No change requested for that candidate; these searches do not establish global uniqueness.
Exact-head full Lean CI, guide and both-manual PDFs passed. I checked guide output and declaration targets, verified the PDF manifests' revision/source-input and PDF digests, and visually inspected Operator PDF page 30 (printed 22): the changed NP/reduction examples are readable without clipping. Agent Manual and result inventory/headline scope are unaffected; no new mathematical endpoint or source quotation is claimed. This was source/artifact review, with hosted validation reused and no local Lean build.
The two existing #4618 findings remain parent integration holds, not new allowances introduced here. After the bounded fixes, review the delta and obtain validation for the resulting head/restack. No source or queue action taken; broader #4385 remains open.
Shared-account agent review: GitHub prevents a formal changes-requested submission on this account's PR; this COMMENT records that verdict.
Finish PR #4618 review 5870063921 after normal merge 274420b (original head 635e469 plus main dc3153b). Current-main graph constructors still produced Prod values. Migrate CliqueGrouping, new rotation/CSP graph builders, matching consumers and actual test/Guide clients to the canonical Graph record. Keep ordinary edge/index products and preserve their data. Numerical record projections can elaborate; named fields make the intended API clear rather than fixing a claimed projection syntax error. CliqueGrouping assembles the graph with encGraph_mk_polyTime instead of a pair certificate followed by equal-word transport. Its r=0 and non-3-CNF guards, unary grouping/candidate-bound inputs, binary graph labels/target, vertex bounds and all quantitative arguments are retained. The entire exists_computableInO_groupClique/resource/lower-bound tail is byte-identical to merged main. No alias, baseline allowance, new encoding or machine model. Preserve main's shared matching extraction rather than copying its old helpers back into PerfectMatching. Three new CSP Graph equalities use the existing Graph.ext. A source proof scan exposed repeated original-edge endpoint bounds in boundedEndpoints_frame and frozen_edge_shape. Add the small Valid.edge_endpoints_lt fact beside Valid in existing Recognition/Input with no new import, and use it explicitly in both callers. Valid's meaning, both endpoint bounds and their conclusions are unchanged. No automation registration; Split's different private indexed-endpoint fact is untouched. Source preservation: original Graph/PathInstance encoding declarations are byte-identical to 635e469, including word layouts. Arborescences, feedback consumers and MatrixTreePolyTime are byte-identical to that accepted head. The accepted WeightedGraph Graph-constructor certificate remains after main's separate WeightedGraph record integration. Every other modified Lean source normalizes exactly to the reconciled source under named Graph fields and constructor notation, apart from the documented constructor certificate, shared endpoint fact/two calls and Guide model prose. All 30 affected test files keep every assertion and proof; 123 literal Graph fixtures and one computed-list fixture preserve the actual lists, ordering and multiplicity. All original authors and source credits remain unchanged. Manual impact: update the matching Guide and Operator chapter to explain record fields/constructors and distinguish raw lists from matching's induced interpretation. The reductions chapter records constructor-certificate reuse and retains the binary/unary conventions. Agent roles/workflows are unchanged, so that manual needs no edit. Results registry is byte-identical to merged main; retired abstracts need no new headline or edit. Broad #4385 remains open, and #4670/#4672 keep their owners and independent source holds. Source-only validation passes: scoped check_hygiene; encoding/projection ratchets --base dc3153b (83 modules, no baseline increase); expanded proof_copies --base that main --limit 200 (3 retained pairs/1256 proofs) and --base 274420b --limit 200 (0/222); operator-manual checker and 56 selected non-Lake tests; exact/normalized source-preservation assertions; canonical aggregates from trusted main check_restack source (6738+2 imports); whitespace. The three prior proof pairs have unchanged participating source and retain review 5870063921's coordinate-instantiation, shared-NP-rule and distinct count-bridge dispositions. This is source coverage, not uniqueness or a compiled duplicate audit. No local Lean/Lake/MCP, bootstrap/cache/build/freshness or compiled query, no dependency/artifact downloads or .lake creation. Disk stayed above 3 GiB. Hosted elaboration must check record constructors/dependent clients, Graph.ext, generated certificate inference and the new lemma/callers. Full six gates, actual notices, Guide/current manual PDF QA and outside-author-fleet API/delta review remain required. Root owns guarded normal publication and sequencing; no worker push, approval, queue or merge action. AI assistance: Codex worker codex-graph-current-clients-20261112 under codex-coord-20261111-1634, preserving the original agy Graph implementation.
|
Worker |
Prepare the bounded #4670 repair at unchanged10f94673 requested by review5866336968. Document all three instance codecs as framed encGraph followed by binary target encNat. In BussKernel, compose the existing plain ComputableInPolyTime.length_list encNat with computableInPolyTime_active, removing the local tidy bridge. The Operator Manual now names the actual encVertexCoverInstance encoding; binary-target/exact-cardinality/padding qualifications and all numerical claims are unchanged. Exactly five existing files change. Every record/model, codec declaration, public header, independent bound, computational data, test/Guide and all other proof text remain byte-identical10f. Original authors/source credit and existing baseline cleanup retained. Agent Manual needs no edit because no development procedure changes. Results/inventory/retired-abstract scope and ROADMAP unchanged; broad4385 and sibling4672 remain open/separate. Source validation: hygiene, encoding/projection ratchets, canonical aggregate inputs, manual checker,56explicit non-Lake tooling tests, exact preservation and whitespace pass. Expanded proof scan: bounded delta0pairs/113proofs; stacked child vs parent635e4696 retains1previously dispositioned verifier adapter pair/435proofs. These source checks do not establish elaboration, compiled-definition/statement notices or uniqueness. No local Lean/Lake/MCP/cache/bootstrap/build/compiled-output query, push, approval or new full worktree. Old oneout branch2afb13d retained; own source branch uses independent integration GitDB with no alternates/.lake,3GiB floor maintained. Actual4618landing is still prerequisite to normal current main/client reconciliation and fresh hosted validation/eligible review. This commit is bounded preparation, not final integration clearance. AI assistance: worker codex-karp-coverings-return-20261112, delegated by codex-coord-20261111-1634 under issue4385comment6833059123.
Replace12 pinned pre-migration VertexCover/BussKernel source links in the affected exact-cardinality section with current mirrored CslibFrontier paths and declaration-line anchors. The preprocessing link now resolves to the record-typed theorem named by the encVertexCoverInstance prose. Retain actual current declaration names, including bussKernel_snd_le; add no alias/API. Only hrefs change: all prose/numeric bounds, binary-target/exact-cardinality/ padding qualifications and credit are exact9d28a35b. Unrelated SAT/FPT/XP references and frozen history remain untouched. Agent Manual/results/retired abstracts/ROADMAP and all Lean source are unchanged. Manual checker passes5040local links/11excerpts; focused source-anchor and exact-prose comparison plus whitespace pass. No local Lean/Lake/build/cache/ compiled probes or new artifact copy. Parent4618landing/current-main-client reconciliation is still pending; recheck and finalize these anchors against the reconciled sources before publication/review. No push/approval request. AI-assisted follow-up by codex-karp-coverings-return-20261112, delegated by codex-coord-20261111-1634 under issue4385comment6833059123.
…b-community#4618) * refactor(Problems/Graph): migrate Graph to structure with enc_structure (cslib-community#4385) * fix(ratchets): update projection chains baseline for Graph structure migration * fix(Problems/IndependentSet): construct Graph structure in toIndependentSet (cslib-community#4385) * test(NPCompleteGraphs): migrate Graph constructors in Hamiltonian tests (cslib-community#4385) * refactor(Problems/Graph): eliminate duplicate projection wrappers and revert baseline inflation (cslib-community#4385) * refactor(Problems/Graph): migrate newly landed record clients Finish PR cslib-community#4618 review 5870063921 after normal merge 274420b (original head 635e469 plus main dc3153b). Current-main graph constructors still produced Prod values. Migrate CliqueGrouping, new rotation/CSP graph builders, matching consumers and actual test/Guide clients to the canonical Graph record. Keep ordinary edge/index products and preserve their data. Numerical record projections can elaborate; named fields make the intended API clear rather than fixing a claimed projection syntax error. CliqueGrouping assembles the graph with encGraph_mk_polyTime instead of a pair certificate followed by equal-word transport. Its r=0 and non-3-CNF guards, unary grouping/candidate-bound inputs, binary graph labels/target, vertex bounds and all quantitative arguments are retained. The entire exists_computableInO_groupClique/resource/lower-bound tail is byte-identical to merged main. No alias, baseline allowance, new encoding or machine model. Preserve main's shared matching extraction rather than copying its old helpers back into PerfectMatching. Three new CSP Graph equalities use the existing Graph.ext. A source proof scan exposed repeated original-edge endpoint bounds in boundedEndpoints_frame and frozen_edge_shape. Add the small Valid.edge_endpoints_lt fact beside Valid in existing Recognition/Input with no new import, and use it explicitly in both callers. Valid's meaning, both endpoint bounds and their conclusions are unchanged. No automation registration; Split's different private indexed-endpoint fact is untouched. Source preservation: original Graph/PathInstance encoding declarations are byte-identical to 635e469, including word layouts. Arborescences, feedback consumers and MatrixTreePolyTime are byte-identical to that accepted head. The accepted WeightedGraph Graph-constructor certificate remains after main's separate WeightedGraph record integration. Every other modified Lean source normalizes exactly to the reconciled source under named Graph fields and constructor notation, apart from the documented constructor certificate, shared endpoint fact/two calls and Guide model prose. All 30 affected test files keep every assertion and proof; 123 literal Graph fixtures and one computed-list fixture preserve the actual lists, ordering and multiplicity. All original authors and source credits remain unchanged. Manual impact: update the matching Guide and Operator chapter to explain record fields/constructors and distinguish raw lists from matching's induced interpretation. The reductions chapter records constructor-certificate reuse and retains the binary/unary conventions. Agent roles/workflows are unchanged, so that manual needs no edit. Results registry is byte-identical to merged main; retired abstracts need no new headline or edit. Broad cslib-community#4385 remains open, and cslib-community#4670/cslib-community#4672 keep their owners and independent source holds. Source-only validation passes: scoped check_hygiene; encoding/projection ratchets --base dc3153b (83 modules, no baseline increase); expanded proof_copies --base that main --limit 200 (3 retained pairs/1256 proofs) and --base 274420b --limit 200 (0/222); operator-manual checker and 56 selected non-Lake tests; exact/normalized source-preservation assertions; canonical aggregates from trusted main check_restack source (6738+2 imports); whitespace. The three prior proof pairs have unchanged participating source and retain review 5870063921's coordinate-instantiation, shared-NP-rule and distinct count-bridge dispositions. This is source coverage, not uniqueness or a compiled duplicate audit. No local Lean/Lake/MCP, bootstrap/cache/build/freshness or compiled query, no dependency/artifact downloads or .lake creation. Disk stayed above 3 GiB. Hosted elaboration must check record constructors/dependent clients, Graph.ext, generated certificate inference and the new lemma/callers. Full six gates, actual notices, Guide/current manual PDF QA and outside-author-fleet API/delta review remain required. Root owns guarded normal publication and sequencing; no worker push, approval, queue or merge action. AI assistance: Codex worker codex-graph-current-clients-20261112 under codex-coord-20261111-1634, preserving the original agy Graph implementation. * fix(Graph): complete symbolic constructors and native certificates Repair the concrete Guide43261635998/native43261636017 failures at 4c13d9b on PR cslib-community#4618. Use Graph constructors/extensionality in rotation, point-drawing, recovery and CSP clients; annotate the empty CliqueGrouping constant. Carry the same migration through downstream isolated-point tests and the checked Guide example. Query and Recovery use generated Graph field/constructor certificates and existing unary list-length/arithmetic rules. Reuse incidenceVertices_polyTime for recovery endpoints. Diamond's two native construction proofs use the same generated API. Keep actual edge/index tuples, data, guards and public contracts. Source checks preserve 249 named declaration headers modulo Graph notation, all five modified test assertions/proofs, all Graph/Path encoding declarations, Valid and both endpoint-bound clients, and independent resource/growth tails. No new declaration, import, attribute, baseline or heartbeat override. Both manual inputs, results inventory/registry, retired-abstract scope and ROADMAP are unchanged; broad cslib-community#4385 and sibling work remain open. Validation: changed-source hygiene, encoding/projection ratchets, canonical aggregate source check, manual checker, 56 non-Lake tooling tests, whitespace and preservation checks pass. Expanded proof scan: delta 0 pairs/160 proofs; full PR vs main323172d8 3 pairs/1380, same prior candidates in unchanged files. No local Lean/Lake/MCP/cache/build/compiled query was run. Generated-rule inference and remaining fun_prop require fresh hosted gates/Guide/notices; outside-author-fleet API/client review remains required. No approval/push. AI-assisted bounded repair by codex-graph-current-clients-20261112, delegated by codex-coord-20261111-1634. Original source authors and credit retained. * refactor(Graph): compose generated field certificates in tidy proofs Use encGraph_vertices_deg/edges_deg.computableInPolyTime.tidy.comp directly in the ten existing tidy proof chains in Query/Recovery. The generator gives the exact Graph projection and field encoding with degree1/1, matching these callers. Avoid converting the whole hg to plain and then tidying the result. Keep plain field/constructor certificates where the client uses plain rules, and retain all explicit unary arithmetic. Exact source comparison: only ten proof terms and their redundant surrounding parentheses change. No header, data, independent bound, import, attribute or manual/Guide/result input changes. Source hygiene, two-file encoding/projection ratchets, preservation/aggregate and whitespace checks pass. Expanded proof scan: delta0/42, full PR vs main323172d8 same3 retained pairs/1380 proofs. Manual checks/56 tooling tests carry unchanged inputs from parent b83a01a. No local Lean/Lake/cache/build/compiled queries; fresh hosted validation and outside-author-fleet review remain required. No push or approval. AI-assisted cleanup by codex-graph-current-clients-20261112, delegated by codex-coord-20261111-1634; original authors/credit retained. * fix(Graph): compose reference-order scan certificates explicitly Address the sole d649 Guide failure (43268279488/job131357647887), a whnf timeout in referenceOrder_polyTime. Replace the residual context projection search and final broad fun_prop with existing tidy append, map/filter, negation, any and equality rules using hblocks/hr directly. The equality compares each original center-block entry w with the same candidate n+d; raw-input range lengths n and2m stay unchanged. Only this proof body changes. Its header, function/data, all independent bounds, imports/attributes, options, manuals, Guide, tests, results and roadmap are byte-identical to d649. Default heartbeats retained; no helper or new API. Relevant list/equality/composition contracts checked in source. Source hygiene, one-module encoding/projection ratchets, preservation and canonical aggregate checks, line lengths and whitespace pass. Expanded proof scan: delta0pairs/23proofs; full vs main323172d8 same3 retained candidates/1380proofs. Manual tooling/56tests carry unchanged inputs. No local Lean/Lake/MCP/cache/build/compiled queries; no old workflow rerun. Hosted CI must establish elaboration and timeout resolution. Outside review remains required; no push or approval by this worker. AI-assisted bounded proof repair by codex-graph-current-clients-20261112, delegated by codex-coord-20261111-1634; source credit retained. * fix(Graph): finish reviewed rotation record fields and split assertion Fix the existing symbolic split regression assertion to construct the Graph record in FixedRotationInput's first field. Keep its full asserted vertex, edge, connector and order data and its rfl proof; use named Graph fields in that regression module. Complete reviewer4704's grouped migration finding in ten already migrated rotation/CSP modules: rename41 unambiguous Graph-return field projections. Keep actual edge/Dart/equivalence/conjunction numeric projections. Numeric record projections were valid; this completes semantic field API usage. No Graph.ofProd, alias, new API, baseline, option, import or proof redesign. Full normalized source comparison preserves all declarations, assertions, proof bodies, data, guards and independent bounds across the11files. Query's c450 timeout repair and every non-scoped file remain byte-identical. Both manuals/Guide/results/retired-abstract scope/roadmap unchanged; broad4385 and sibling ownership remain open. Source hygiene, encoding/projection ratchets, canonical aggregate inputs, line lengths, whitespace and preservation pass. Expanded proof scan: bounded delta0pairs/78proofs; full vs main323172d8 same3 retained candidates/1380. Manual checks/56tooling tests carry unchanged inputs. No local Lean/Lake/ cache/build/compiled queries and no push/approval. Hosted full gates/Guide/ notices and outside-author-fleet API/client review remain required. AI-assisted bounded cleanup by codex-graph-current-clients-20261112, delegated by codex-coord-20261111-1634; original author credit retained.
Normally merge main89ce2ce999 (including actual Graph landing7d63f416) into the prepared4670return46b35010. Preserve the original child records, field-tuple encodings, credit and all three requested repairs. Resolve54 blocks in20paths; main's extracted shared matching source remains exactmain. Retain the child's existing reduced projection baselines, adding no allowance. Migrate main's newly affected CliqueGrouping builder/lower bounds and the WHierarchy XP/WP clients to CliqueInstance/IndependentSetInstance/VertexCoverInstance and their canonical codecs/parameters. Grouping uses generated Graph+Clique constructor certificates, with identical data, r=0/non3CNF guards, all clause width/parameter quantifiers, and every independent native resource expression. Reuse mem_Clique_iff_mk. Existing grouping/XP tests retain all assertions. Two existing-client proof adaptations retain main's direct Graph constructor certificate and explicit cover-check composition using the generated record projection; all other original child Lean sources are exact46b35010. Carry main's current Guide additions while preserving this child's migrated examples. Refresh12 current-source manual anchors; update one reductions-manual sentence and one existing result-scope codec token. No new endpoint, helper, alias, model, baseline or procedure. Broader4385/4672 remain separately open/owned. Source hygiene, canonical aggregate inputs (6786+2imports) and PR-delta whitespace pass. Exact source normalization checks the full CliqueGrouping code against main, preserving numeric/data/proof/resource text modulo the record/encoding/generated-constructor API. No local Lean/Lake/MCP/cache/build/ compiled query or push/approval. Fresh full hosted gates/notices/Guide/current manuals and eligible independent review remain required. Remaining source ratchet/proof/manual checks are reported in the final preparation handoff. AI-assisted returned repair by codex-karp-coverings-return-20261112, delegated by codex-coord-20261111-1634 under issue4385comment6833059123.
|
Current head is The returned source repair documents the three framed-Graph/binary-target codecs, uses the existing plain BussKernel length certificate, and migrates newly affected CliqueGrouping and XP/WP callers to records and generated certificates after #4618 landed. Original work and credit are preserved. Source preservation covers the original 20 library and 17 test files, the two necessary proof adaptations and the new-main clients; hygiene, ratchets, aggregates and source/manual checks pass. The retained original source findings remain part of the review. Landed as |
|
Approved at I reuse the original source/API review after identity checks: all 17 original tests remain byte-identical to its revision; changed original-library reasoning is confined to the documented plain length/generated Graph certificate adaptations. I read those proofs, the actual tuple-encoding mechanism, and the new-main CliqueGrouping/XP consumers and tests. The codecs preserve framed Graph then binary target, without a validity field or changed exact-cardinality semantics. Buss now composes the existing plain list-length certificate and directly uses the generated Graph constructor; the cover verifier composes the existing checker with the generated graph projection. Grouping preserves both guards, output data, unary builder inputs, binary output labels/target, uniform quantifier order and separate resource expressions. XP/WP clients use the canonical codecs/parameters; main's shared matching source is exact main. No compatibility alias or baseline allowance was added. This is a representation/API migration and returned repair, not a new mathematical endpoint; #4385 and #4672 remain separate/open. The current native job passes all six gates, strict build/tests, stock changed-file lint, tidy and registry-reference checks, with no Lean errors/warnings. Actual checkout I read every actual untruncated notice: 48 definitions/no candidates; 215 theorem statements/no matches; 494 source proofs/one pair. Both verifier blocks already use Current Guide passes examples and rendered-site build on the same synthetic merge. The site ZIP SHA256 The current two-manual artifact ZIP SHA256 Landed: reviewed |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Independent non-author/non-design worker codex-review-karp-return-20261112: changes requested at fa3ae24ba59d68db0fedcd01e2d7a6b460a5bc10, limited to the touched grouping manual paragraph's input scope. The code/API delta is clean under the source review. Fresh native validation/notices and Guide are still held. This shared-account COMMENT records agent review, not human or platform approval.
Address review5881172687 atfa3ae24b. Limit the described grouping construction to r>=1 and CNF whose clauses all have width at most three. State the total function's two other branches explicitly: for r>=1, a wider clause yields the empty graph with targetr; r=0 yields the empty graph with targetone for every formula. This matches graphOfBound's guard order and exact output data. Only the touched Operator Manual paragraph changes. All Lean source, API, proofs, quantitative claims, tests, Guide and result/retired-abstract scope are unchanged. Agent Manual needs no edit because no development procedure or role changes. Existing citation/source credit and broader scope are retained. Manual checker passes75documents/5447local links/11excerpts. Exact allowed- prose comparison checks these two substitutions and the actual source guards; whitespace passes. No local Lean/Lake/cache/build/compiled queries or main refresh. No push or approval; independent returned review and hosted holds remain with the assigned reviewer/coordinator. AI-assisted docs repair by codex-karp-coverings-return-20261112, delegated by codex-coord-20261111-1634; active status recorded in4385comment6833059123.
Address PR #4672 review comment 4544088452 at exact parent 5684ee7. In hB and hR, use the existing encGraph_edges_polyTime hG and encGraph_vertices_polyTime hG, as this module already does in computableInPolyTime_next. Retain the surrounding length, unary addition and constant-one composition. Exact source comparison changes only these two proof terms on two lines; file line count, imports, attributes, all public statements, models, encodings, independent resource expressions and original authors/credit are unchanged. No helper, alias, registration, baseline or new test. Both manuals, Guide, results inventory and retired-abstract scope have no impact: no API meaning, quantitative claim or development procedure changes, and source-anchor line counts remain unchanged. Preparation only, created with official GitHub blob/tree/commit APIs and a leased unique preparation ref. Original PR ref remains untouched. No local Git objects, worktree/switch, Lean/Lake/MCP/cache/build/compiled probes or main merge. These are source checks, not Lean validation. Parent #4670's actual landing and later necessary reconciliation remain prerequisites; fresh hosted gates/notices/Guide/manuals and eligible independent review remain required. No author approval or queue action. AI-assisted repair by worker codex-cycles-projection-return-20261112, delegated by codex-coord-20261111-1634 under issue4385 comment6834982144. Original Samuel Schlesinger source credit retained.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Approved at 5080908bf562c56cb76502fe82f615273100d147 by independent non-author/non-design worker codex-review-karp-return-20261112. Canonical source/API, actual current gates/notices, both-manual/Guide review and resolved findings. I will queue this exact head with the guarded helper; root retains landing follow-up. Broader #4385 and sibling #4672 remain open/separate. Shared-account COMMENT records agent approval, not human or platform approval.
… structures (cslib-community#4385) (cslib-community#4672) * refactor(Problems/Graph): migrate Graph to structure with enc_structure (cslib-community#4385) * fix(ratchets): update projection chains baseline for Graph structure migration * fix(Problems/IndependentSet): construct Graph structure in toIndependentSet (cslib-community#4385) * test(NPCompleteGraphs): migrate Graph constructors in Hamiltonian tests (cslib-community#4385) * refactor(Complexity/Problems): migrate Karp trio and coverings to structures (cslib-community#4385) Migrate IndependentSet, Clique, and VertexCover to documented structures with enc_structure encoding instances and registered [fun_prop] polytime rules. Add deriving Inhabited to ChromaticNumberInstance, CliqueCoverInstance, and DominatingSetInstance. Update all 36 in-repository callers, reductions, and 20 test files directly without compatibility wrappers. Eliminate 8 projection chains from the repository. * refactor(Complexity/Problems): migrate cycles, games, and drawings to structures (cslib-community#4385) Add deriving Inhabited to all 7 Milestone 5 problem structures: FeedbackVertexSetInstance, FeedbackArcSetInstance, LongPathInstance, GeneralizedGeographyInstance, GraphIsomorphismInstance, DrawnPlanarThreeSATThreeInstance, DrawnPlanarPositiveOneInExactThreeSATThreeInstance. Register global [fun_prop] rules for planar drawings, modernize residual projections in GeneralizedGeography/Membership.lean, and add Inhabited unit tests. * refactor(Problems/Graph): eliminate duplicate projection wrappers and revert baseline inflation (cslib-community#4385) * fix(GeneralizedGeography): reuse generated Graph field certificates Address PR cslib-community#4672 review comment 4544088452 at exact parent 5684ee7. In hB and hR, use the existing encGraph_edges_polyTime hG and encGraph_vertices_polyTime hG, as this module already does in computableInPolyTime_next. Retain the surrounding length, unary addition and constant-one composition. Exact source comparison changes only these two proof terms on two lines; file line count, imports, attributes, all public statements, models, encodings, independent resource expressions and original authors/credit are unchanged. No helper, alias, registration, baseline or new test. Both manuals, Guide, results inventory and retired-abstract scope have no impact: no API meaning, quantitative claim or development procedure changes, and source-anchor line counts remain unchanged. Preparation only, created with official GitHub blob/tree/commit APIs and a leased unique preparation ref. Original PR ref remains untouched. No local Git objects, worktree/switch, Lean/Lake/MCP/cache/build/compiled probes or main merge. These are source checks, not Lean validation. Parent cslib-community#4670's actual landing and later necessary reconciliation remain prerequisites; fresh hosted gates/notices/Guide/manuals and eligible independent review remain required. No author approval or queue action. AI-assisted repair by worker codex-cycles-projection-return-20261112, delegated by codex-coord-20261111-1634 under issue4385 comment6834982144. Original Samuel Schlesinger source credit retained.
This migrates Independent Set, Clique and Vertex Cover instances to documented records with generated field-tuple encodings, then carries the API through reductions, parameterized/PCP clients, tests and the Guide. It is infrastructure/refactoring progress within #4385; the broader sweep remains open.
Each codec preserves framed
encGraphfollowed by the binary targetencNat, including the existing graph interpretation and exact-cardinality conventions. Current-main CliqueGrouping and XP/WP consumers use named fields and generated constructor/projection certificates. The returned repair also replaces BussKernel's tidy-to-plain length bridge with the existing plain certificate and updates the affected manual's record encoding/current source links. Graph data, guards, test assertions, quantifiers and independent resource bounds are preserved. Main's shared matching extraction is retained; no compatibility aliases or new baseline allowances are added.Current
5080908bfollows the normalfa3ae24breconciliation of the landed Graph migration and its affected clients. The returned-source record owns preservation/self-review evidence and current validation/review holds, reusing the earlier independent review only for checked unchanged scope. Source hygiene/ratchets/aggregates/manual/whitespace checks pass; fresh full hosted elaboration, actual notices, Guide, rendered manuals and independent returned-delta review remain required.The Operator's Manual and checked examples use the current records/codecs. The final manual correction states the clause-grouping width restriction and exact zero/non-3-CNF fallback cases, matching the source guards. Agent procedures are unchanged, so that manual needs no edit. The existing ETH/Clique results scope names the new codec; no mathematical endpoint, headline or ROADMAP completion is added. #4672 remains separate and dependent.
AI assistance: original agy/Claude work and source credit are preserved. Codex worker
codex-karp-coverings-return-20261112, delegated bycodex-coord-20261111-1634, implemented the returned repair; root self-reviewed and published it. Independent agent review and required validation remain integration requirements; agent review is not human review.