feat(SAT): prove orthogonal planar 3SAT-3 NP-hardness by edemaine · Pull Request #1122 · cslib-community/complexitylib

edemaine · 2026-10-25T20:24:38Z

This proves NP-hardness of planar 3SAT with clause width and literal-occurrence count at most three, both for formulas whose incidence graph admits an integer orthogonal drawing and for formulas with that drawing supplied. Binary clauses are allowed; repeated literals count separately. Every generated route is simple, avoids nonincident vertices, and meets other routes only at common graph endpoints on their full real supports. Parallel incidence occurrences retain distinct routes.

The total native polynomial-time compiler starts from ordinary binary-encoded 3SAT. For original size S = clauses + literal occurrences + 1, it emits grid sides at most 13440*S, at most 29400*S² clauses and 59290*S² literal occurrences/routes, 1127000*S² segments, and Manhattan wire length at most 14700000*S². These are bounds on the actual emitted formula and drawing, including empty and syntactically rejected inputs. Source labels and emitted coordinates use binary encodings. The supplied-drawing and existential-drawing languages are proved NP-hard; no membership theorem for these target languages is claimed.

The implementation reuses CNF, listed Graph, the ordered incidence graph, first-occurrence selection, compaction, real segment support, and plain computability. The new drawing encoding combines existing binary point/route encodings; the syntax guard isolates the width/count tests from the assignment verifier. The global finite tiling and quantitative proof are original. Source credit for the occurrence splitter and fixed crossover adapted from lean-trominoes is preserved in their modules.

This completes the mathematical scope of #1079 and stacks on #1111. The earlier stack layers retain their own validation and reviews. Final wrapper/hardness delta review found no blocking findings in the unchanged endpoint semantics. Maintainer integration and outside-fleet coordinator approval remain required.

Validation: b971639d, tree af3e4ebf: all six required gates pass, including the global axiom audit, plus focused regressions, hygiene and documentation configuration. Each updated parent PR also records all six gates at its final restacked head. The additional guide build retains the existing Windows Verso lean_md4c_markdown_parse linker limitation before chapter elaboration; no dependency source was edited.

Compiler/semantics/count/time/bounds review, actual geometry closure review, and the wrapper/hardness review above cover the mathematical development. The later citation, Batteries/CNF reuse, shared-tail and encoding APIs, module-placement and targeted-import fixes have a clean independent technical delta review. Final merge ancestry preserves that reviewed tree exactly. No statement meaning, emitted data, encoding or resource bound changed. All stale module imports are removed and the aggregate is regenerated. The nonblocking checker-speed suggestion is tracked in #1125. These records do not claim execution of the certified native machines. Fresh outside-fleet coordinator verdicts remain required for the updated stack.

Selected abstract catalogue/rendering: no impact. No new headline is selected; existing selected statements and scope are unchanged. ROADMAP.md has no existing direction changed by this result, and no upstream pin or coordination exception changes.

AI assistance: GPT-6.1-sol, including delegated implementation and technical review. Agent reviews do not imply human approval.

Initial shared foundation for #1082 and #1079. Narrow Lean elaboration passes without warnings using isolated outputs; full project gates remain pending while package seeding finishes. New original geometry API reuses Mathlib segments and List.consecutivePairs. Curated abstracts: no impact; no existing statements or selected headlines changed.

Checkpoint for #1083: adapt the credited Figure 8(b) clauses, prove exact independent opposite-port equality, and replace eight degree-six internal variables by fixed six-copy implication rings. The resulting formula has 53 variables, 74 clauses, width at most three, occurrence at most three, and degree-two terminals with one external occurrence available. Validation: narrow Lean checks of both modules passed with LEAN_NUM_THREADS=2. Full gates and orthogonal geometry certification remain pending; this checkpoint does not complete #1083 or #1079. Curated abstracts: no impact (new helper construction; no selected headline statement or scope changes). AI assistance: implementation by Codex GPT-6.1.

Checkpoint for #1079 and #1083: certify an integer bounding-box checker against complete real segment supports; compose it over finite routes, including empty and singleton supports. Tests cover transverse crossings, forbidden collinear overlap, permitted endpoints, vertex exclusion, and diagonal intersections away from the integer lattice. Validation: narrow native Lean checks of the source and concrete tests passed, using isolated output files and the compiled Orthogonal foundation at e2989c7. A coherent strict Lake target build and the full six validation gates remain in progress; this is not a ready-to-integrate endpoint. Curated abstracts: no impact; helper geometry with no selected statement changes. AI assistance: Codex GPT-6.1 implementation and self-review.

Split finite literal occurrences with binary implication cycles, prove exact linear counts, and certify a total binary-encoded native polynomial-time reduction and verifier. Preserve the lean-trominoes construction credit. Planarity remains outside this milestone.

…ar sides Part of #1082. Prove continuous simplicity, no incidental vertex centers, and shared-endpoint-or-strict-transverse contacts for explicit five-segment routes. Width is at most 8n, height at most 8n+2m, and each edge wire length at most 80n+10m. Strict Lake target build passes; full six validation gates remain pending the graph-binding integration. Curated abstracts: no impact; no selected abstract or headline changes. Construction and proofs are original; Mathlib supplies the continuous segment semantics.

Checkpoint for #1083: adapt the credited Figure 8(b) clauses, prove exact independent opposite-port equality, and replace eight degree-six internal variables by fixed six-copy implication rings. The resulting formula has 53 variables, 74 clauses, width at most three, occurrence at most three, and degree-two terminals with one external occurrence available. Validation: narrow Lean checks of both modules passed with LEAN_NUM_THREADS=2. Full gates and orthogonal geometry certification remain pending; this checkpoint does not complete #1083 or #1079. Curated abstracts: no impact (new helper construction; no selected headline statement or scope changes). AI assistance: implementation by Codex GPT-6.1.

Split finite literal occurrences with binary implication cycles, prove exact linear counts, and certify a total binary-encoded native polynomial-time reduction and verifier. Preserve the lean-trominoes construction credit. Planarity remains outside this milestone.

Part of #1082. Enumerate endpoints of the existing Graph edge list and assign preceding-occurrence ranks. When each endpoint label occurs at most three times, equal vertex/port pairs identify the edge occurrence and endpoint side. Provide canonical_index_port_ne for geometric layout specialization. Strict Lake target builds pass for both new modules. Full validation remains pending the complete graph drawing binding. Curated abstracts: no impact.

Initial shared foundation for #1082 and #1079. Narrow Lean elaboration passes without warnings using isolated outputs; full project gates remain pending while package seeding finishes. New original geometry API reuses Mathlib segments and List.consecutivePairs. Curated abstracts: no impact; no existing statements or selected headlines changed.

Checkpoint for #1079 and #1083: certify an integer bounding-box checker against complete real segment supports; compose it over finite routes, including empty and singleton supports. Tests cover transverse crossings, forbidden collinear overlap, permitted endpoints, vertex exclusion, and diagonal intersections away from the integer lattice. Validation: narrow native Lean checks of the source and concrete tests passed, using isolated output files and the compiled Orthogonal foundation at e2989c7. A coherent strict Lake target build and the full six validation gates remain in progress; this is not a ready-to-integrate endpoint. Curated abstracts: no impact; helper geometry with no selected statement changes. AI assistance: Codex GPT-6.1 implementation and self-review.

…ar sides Part of #1082. Prove continuous simplicity, no incidental vertex centers, and shared-endpoint-or-strict-transverse contacts for explicit five-segment routes. Width is at most 8n, height at most 8n+2m, and each edge wire length at most 80n+10m. Strict Lake target build passes; full six validation gates remain pending the graph-binding integration. Curated abstracts: no impact; no selected abstract or headline changes. Construction and proofs are original; Mathlib supplies the continuous segment semantics.

Part of #1082. Enumerate endpoints of the existing Graph edge list and assign preceding-occurrence ranks. When each endpoint label occurs at most three times, equal vertex/port pairs identify the edge occurrence and endpoint side. Provide canonical_index_port_ne for geometric layout specialization. Strict Lake target builds pass for both new modules. Full validation remains pending the complete graph drawing binding. Curated abstracts: no impact.

For #1079, tag each auxiliary variable by its gadget site and prove extension to the assembly iff extension to each gadget with one common shared assignment. Prove exact clause/literal counts. Concrete tests cover fresh private variables, repeated sites, conflicting shared assignments, and empty families. Validation: strict targeted Lake build of source and tests passed; default full build passed with an unrelated inherited crossover long-line warning. Full six gates will be rerun on the final stacked revision. Curated abstracts: no impact (new helper API, existing headline statements and rendering unchanged). AI assistance: Codex GPT-6.1 implementation/self-review.

For #1079, reuse Graph lists with dense variable names followed by indexed clause names and one listed edge per literal occurrence. Prove exact sizes, endpoint declaration, bipartiteness, looplessness and native polynomial-time construction under arbitrary encoded variable names. Tests include huge binary labels, repeated incidences, isolated empty clauses, empty formulas and finite variable types. Validation: source passes current-source Lean MCP diagnostics and the default full Lake build, including the native time certificate; concrete tests pass Lean diagnostics. Full six gates on the final stacked revision remain pending. Curated abstracts: no impact. AI assistance: Codex GPT-6.1 implementation/self-review.

Part of #1082. Emit explicit finite position and route lists using existing Graph labels and edge indices. Prove exact endpoints, proper orthogonality, continuous simplicity, five segments per edge, total wire length at most 90(n+m)^2, and a 2m^2 finite cover for crossing sites under canonical degree-three ports. Strict Lake target build passes. Full validation pending route-unit-subdivision integration. Curated abstracts: no impact.

Complete source checkpoint for #1083: explicit 53-variable, 74-clause ordinary CNF template; 154 simple orthogonal incidence routes in a 240-by-240 box with four isolated access ports. Certify real-support planarity contacts, exact endpoints, distinct vertices, nonincident vertex avoidance, terminal capacity, 414 total segments and 2196 total wire length including access. Validation checkpoint: all five gadget modules passed narrow Lean checks; strict Lake build and mk_all check passed. Full test/lint gates are still running, and final module-doc heading edits will be rechecked after merging the published integration base. No completion or hardness claim for #1079. Curated abstracts: no impact; no selected headline statement or scope changed. Source credit retained from the pinned lean-trominoes gadget. AI assistance: Codex GPT-6.1.

Merge ca6f5a4, retaining the core bridge_stem_crossing_point addition. Remove the route_segments_length simp tag reported by the first full lint run; its statement is unchanged. All first-run gates except this shared simpNF finding passed. Revalidate the merged final tree before PR handoff.

Remove the redundant simp attribute from route_segments_length; its statement, name and proof are unchanged. All six strict project gates pass on the resulting tree at ca6f5a4 plus this exact one-line diff (COMPLEXITYLIB_CACHE_AUTO=0 LEAN_NUM_THREADS=2 scripts/check.sh). Selected abstracts and rendering are unaffected.

Delegated subtask of #1079 after the #1082 crossing-layout core. Prove exact point count and wire length, endpoint preservation, unit adjacency, proper orthogonality, and equality of continuous real supports. Signed-coordinate and empty/singleton regression instances pass. Strict Lake module and test target builds pass; complete validation awaits final native-computation extension. Curated abstracts: no impact; no headline or renderer changes.

… time Add a binary-coordinate/unary-budget compiler using existing plain ComputableInPolyTime APIs. Bound output by budget times segment count plus one, and recover full subdivision whenever the budget bounds total wire length. Add cap-sufficient, cap-insufficient, zero-budget, and native-certificate regression examples. Strict module/test target builds pass with default heartbeats. Normalize new Lean file modes. Curated abstracts: no impact; full six-gate validation follows on the final stacked base.

…dations

Delegated subtask of #1079 after the #1082 crossing-layout core. Prove exact point count and wire length, endpoint preservation, unit adjacency, proper orthogonality, and equality of continuous real supports. Signed-coordinate and empty/singleton regression instances pass. Strict Lake module and test target builds pass; complete validation awaits final native-computation extension. Curated abstracts: no impact; no headline or renderer changes.

Add radius-parametric real grid cells and side-midpoint ports. Prove continuous support translation, orthogonality/simplicity/wire-length invariance, disjoint open/closed cells, and exact adjacency from equal ports. Bounds on listed vertices imply bounds on entire real route supports. Checked examples include fractional real points, negative cell indices, contact and noncontact. Checkpoint validation: MCP diagnostics are clean for the module and tests; LEAN_NUM_THREADS=2 lake build ComplexityTests.OrthogonalMacrocell --wfail --iofail passed. Full six-gate validation remains pending. Selected abstract catalogue: no impact; this geometry API changes no selected theorem, model, bound or scope. AI assistance: implementation by Codex worker t3-96187517-macrocell for #1079; independent review remains with the parent worker/coordinator.

For the global #1079 client, prove IsOrthogonal r and IsSimple r imply (subdivide r).Nodup, using original continuous endpoint-contact certificates. A sufficient-budget native enumeration inherits Nodup. Add a positive canonical-route regression and a distinct-listed-points/self-crossing negative example. Strict geometry/native/test target builds pass. Full six-gate validation follows on the frozen gadget #1108 base; curated abstracts remain unaffected.

…hogonal-planar-three-sat-reduction

Follow the core module move in unit-neighborhood and subdivision regression imports. Public declarations and proofs are unchanged. Final combined validation follows.

Cite Lichtenstein1982 Figs. 4–5 and the MIT–ULB CompGeom Group Tromino2025 Fig. 8(b) in all five modules. Add the original SIAM bibliography entry and complete the existing arXiv entry. Verified the pinned lean-trominoes paper narrative and caption (texlish lines 1244–1285, PDF page 19) against arXiv v1 §3.5 and SIAM DOI metadata; preserve original authors. Reuse CNF.eval_implicationCycle for eval_ring_iff without changing ring or theorem statements, remove unused Holds, and narrow tactic imports. Move only the fixed layout trio to Problems/SAT/Planar with coordinator agreement, preserving namespaces and all declaration/proof payloads. Update the aggregate and add regression clients. Nonblocking elaboration optimization is tracked in #1125. Focused strict Split and moved layout/test targets pass (6306 jobs); import aggregate check and scoped hygiene/bibliography checks pass. Full six gates intentionally await an ordinary merge of the coordinator’s updated core branch, then will run on the final PR head. Curated abstracts unaffected: no selected statement, definition or scope changes. AI-assisted implementation by t3-96187517-gadget. Addresses #1108 review; #1083 / #1079 scope unchanged.

…hogonal-planar-three-sat-reduction

Follow the reviewed reduction-geometry placement without changing emitted data or public statement meanings. Full final integration checks follow.

Regenerate sorted module imports after layout and encoding relocations, removing merge duplicates. Full six-gate validation is running on this unchanged source tree. Mathematical statement meanings, selected abstracts and catalogue are unchanged.

…hogonal-planar-three-sat-reduction

Integrate PR1111's final parent-restacked source. The complete tree remains identical to reviewed source1b83b0fe, treeaf3e4ebf1716d0de0dc0f912a5929167a6737ca6. All six required scripts/check.sh gates PASS on this exact source tree with LEAN_NUM_THREADS=2 and cache downloads disabled: strict library build, aggregate check, strict full tests and global axiom audit, lint, style, and Init imports. Hygiene and documentation configuration checks pass. Unit source99caeb46 also passes all six gates in its isolated checkout. All outside-fleet requests and practical optional nits are addressed across 1094/1107/1108/1111. Citation mapping/source credit is preserved, duplicate proof plumbing uses Batteries/CNF APIs, shared geometry facts serve actual clients, imports and module placement are updated, and mathematical endpoint statements, data definitions, encodings and bounds retain meaning. Checker acceleration is explicitly tracked as nonblocking followup1125. Independent non-author delta review planar-stack-reviewfix-delta-r1 found no blocking findings at source1b83b0fe/treeaf3e4ebf; unchanged mathematical reviews remain applicable. Current outside-fleet coordinator review and maintainer integration remain required. No author approval or merge to main performed. Selected abstracts/catalogue/rendering have no impact. The prior extra Windows guide linker limitation remains unchanged. AI-assisted implementation and delegated technical review by GPT-6.1-sol.

edemaine · 2026-10-25T23:37:51Z

Independent technical delta review by planar-stack-reviewfix-delta-r1 (recorded here by the parent): no blocking findings or changes requested at 1b83b0fe87042ada1a7eb5061afe91c98b2310cc, tree af3e4ebf1716d0de0dc0f912a5929167a6737ca6. Published head b971639d52273e397a7f5b9365536ab132b4eb39 has the identical tree (verified after its ancestry-only unit merge).

The reviewer checked the source/scope citations, Batteries occurrence-rank reuse, shared tail lemmas, exact point/route encoding extraction, module moves, targeted tactic imports and updated regression clients. Affected prefix files match #1094 cf3b1ddc, #1107 ff53772b, #1108 2bd821a0 and #1111 99caeb46. Existing endpoint semantics, emitted data, binary encodings and advertised resource bounds retain their meanings. No obsolete module imports or removed-API clients remain; the aggregate is sorted, unique and complete. Prior mathematical reviews remain applicable, and selected abstracts/catalogue/rendering are unchanged.

Limits: read-only source review, with no elaboration, builds, certified-machine execution or checkout changes. This records agent technical review, not outside-fleet coordinator approval or a merge verdict. Final validation and current revision are recorded in the PR description.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

SamuelSchlesinger · 2026-10-26T05:08:15Z

Coordinator restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix): #1111 merged, so I retargeted this PR to main and merged origin/main into it. New head: 5c7a18b231c441654448f502d42b92f5f25ea430. The only conflict was in guide/ComplexityGuide/NPCompleteness.lean, where main added nothing at that point; I kept this PR's planar 3SAT-3 bullet. Outside Complexity.lean and references.bib, the PR's diff is byte-identical to b971639d. mk_all --check and check_hygiene.py pass. The outside verdict is still pending.

SamuelSchlesinger · 2026-10-26T05:09:02Z

Review claimed by reviewer-claude-c4b0c164-79 (agent review) at 5c7a18b.

SamuelSchlesinger · 2026-10-26T05:25:07Z

reviewer-claude-c4b0c164-79 — APPROVED at 5c7a18b (statement-level outside review; proof internals covered by the internal reviews planar-global-compiler-review-r1 (pullrequestreview-5645238698), planar-full-geometry-review-r1 (pullrequestreview-5645391233), planar-total-hardness-review-r1 (pullrequestreview-5645449436) and the delta review planar-stack-reviewfix-delta-r1 (issuecomment-6404981483))

Agent review, not human approval.

No blocking findings.

Restack identity. For every file this PR touches except the regenerated Complexity.lean, the blob at this head is identical to the one at b971639d, the tree the internal delta review covered. Across the old stack's full file set, only Complexity.lean and references.bib differ, and both match main. The internal reviews therefore apply unchanged.
Headline statements. I checked these against the Lean in Problems/PlanarThreeSATThree.lean and Problems/Graph/OrthogonalDrawing.lean.
- Both targets build on feat(ThreeSAT): prove 3SAT-3 completeness #1094's ThreeSATThree: clause width at most 3 with binary clauses allowed, vars.count v ≤ 3 counting repetitions, and ordinary Satisfiable.
- The drawing data is a list of integer positions following G.1 plus one route per edge occurrence in G.2, matching the feat(planar-SAT): add finite drawing and substitution foundations #1107 layout convention.
- IsPlanarOrthogonalDrawing requires: exact counts; distinct labels and positions; declared, loopless endpoints in either orientation; and nondegenerate axis-aligned segments.
- It also requires IsSimple routes, real-support avoidance of nonincident vertices, and pairwise contacts only at common endpoint positions. Parallel incidences keep separate routes.
- PlanarThreeSATThree quantifies the drawing existentially. DrawnPlanarThreeSATThree takes it as input under encPair encCNF Graph.encOrthogonalDrawing, which uses the existing binary signed encRoute and encPoint.
- Neither target is vacuous. ComplexityTests/PlanarThreeSATThree.lean covers [] ∈, [[]] ∉, a compiled 2^100-label instance ∈ DrawnPlanarThreeSATThree, and the rejection output ∉.
Hardness and compiler. Both _npHard theorems are ThreeSATThree_npHard.trans of plain PolyTimeReducible with the standard NPHard. ThreeSATThree_npHard is itself ThreeSAT_npHard.trans …, so the chain starts from the library's 3SAT. toDrawnPlanarThreeSAT composes feat(ThreeSAT): prove 3SAT-3 completeness #1094's splitter with the guarded compiler, and its ComputableInPolyTime is total. Tidy appears only inside proofs: .of_tidy and a local fun_prop attribute. No public statement mentions tidy.
Bounds. toDrawnPlanarThreeSAT_fits bounds every position and every route point to [0, 13440·S]², where S = φ.length + φ.vars.length + 1 measures the original formula. _costs bounds clauses, literal occurrences, routes, segments and Manhattan wire length by 29400, 59290, 59290, 1127000 and 14700000 times S². These are exactly 7 and 49 times the per-stage constants (1920; 600, 1210, 1210, 23000, 300000), via the splitter's size ≤ 7·S. Both bounds also cover the rejection and empty branches.
Reuse and placement. I found no existing drawing or planarity predicate on main that IsPlanarOrthogonalDrawing duplicates. The PR reuses Graph, SAT.incidenceGraph, Orthogonal.support, IsSimple, IsOrthogonal, the encRoute encodings and CNF.compact. File placement follows the existing stack under Foundations/Geometry/Orthogonal, Logics/Propositional/CNF and Problems/{Graph,SAT/Planar}.
- Nonblocking: CNF.implicationChain (new) overlaps implicationPath/implicationCycle in CNF/ImplicationCycle.lean. A follow-up could define the cycle as the chain closed back to its first element.
Sources. The diff contains no quotations, so the doc(AGENTS): quotations are copied from the pinned source or labeled paraphrase #1072 rule is not triggered. The new constructions are labeled original. The fixed crossover is credited in CNF/Planar/Crossover.lean and CrossoverSplit.lean, which are already merged and cite [Lichtenstein1982], [Tromino2025] and lean-trominoes at a pinned revision.
- Nonblocking: the headline module's References section and the new guide bullet do not credit the classical NP-hardness of planar 3SAT to [Lichtenstein1982]. Suggested follow-up: one References line crediting it, plus a sentence relating this formulation to Lichtenstein's (incidence-graph drawing, occurrence bound, supplied integer orthogonal drawing). That sentence should be labeled as a paraphrase and checked against the source.
Tests. Nonblocking: no regression shows IsPlanarOrthogonalDrawing failing for a satisfiable formula whose drawing has a crossing or a vertex pass-through. Such a test would show that the contacts and avoidsVertices fields have force.
Size. At about +8.6k lines and 39 files, with Geometry.lean alone 2073 lines, this would have been easier to review as separate compiler/semantics, geometry-closure and wrapper PRs. That matches how the internal reviews were already staged. Size note only; not blocking.
Hygiene. A grep of the diff finds no sorry, native_decide, admit, axioms, implemented_by or set_option (heartbeat or otherwise). The only set_option lines are pre-existing guide settings.
Hosted CI at this head: ci-checks passes (run 40272626221) and check-title passes. guide fails (run 40272626170) at ComplexityGuide/NPCompleteness.lean:127. That code block is pre-existing: a polytime example on List.filter (· ≤ p.2), where aesop exhausts its search.

This failure comes from main, not this PR. The nightly API documentation run on main at 8d845488 (run 40265276356) fails at the same block, at line 126 because this PR adds one import line above it.
The chapter reports no other error, including on this PR's new {name} references. The guide passed at the reviewed pre-restack head b971639d.
The main guide regression needs a separate fix and should not block this PR.

edemaine added 30 commits October 25, 2026 14:12

style(geometry): normalize Lean modes and wrap contact documentation

f0e705d

style(graph): normalize Lean source modes

ca6f5a4

Merge validated planar-SAT core lint fix

5c210c9

chore(planar-SAT): combine checked crossover with finite drawing foun…

2ff60d2

…dations

edemaine added 11 commits October 25, 2026 19:16

Merge commit 'fc199d87395532e5e44659a4cd24179a3dc0e076' into feat/ort…

94ea576

…hogonal-planar-three-sat-reduction

refactor(geometry): update consumers of the mirrored layout module

0e8cf03

Follow the core module move in unit-neighborhood and subdivision regression imports. Public declarations and proofs are unchanged. Final combined validation follows.

Merge commit '8a25f7be0dd50357f8227b2ef20753e7541f60ad' into feat/ort…

ea01808

…hogonal-planar-three-sat-reduction

Merge commit 'ff53772b53e2f0c1f43900b9c0ac4218715d3e6a' into feat/ort…

8afd783

…hogonal-planar-three-sat-reduction

Merge reviewed source-frozen planar foundations into crossover

2bd821a

refactor(planar-SAT): import the relocated crossover drawing template

66ed4f6

Follow the reviewed reduction-geometry placement without changing emitted data or public statement meanings. Full final integration checks follow.

Merge commit '2bd821a01ebe8639dc288f1f70e134cc4cef6004' into feat/ort…

1b83b0f

…hogonal-planar-three-sat-reduction

Merge reviewed gadget fixes and refresh subdivision imports

99caeb4

This was referenced Oct 26, 2026

feat(planar-SAT): parsimonious planar 3SAT-3 with explicit grid bounds #1144

Closed

feat(CNF): preserve model counts under occurrence splitting #1147

Merged

SamuelSchlesinger and others added 2 commits October 26, 2026 01:07

Merge origin/main after #1111 squash (coordinator restack)

b509f3c

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

chore: regenerate Complexity.lean

5c7a18b

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

SamuelSchlesinger changed the base branch from t3/orthogonal-unit-subdivision to main October 26, 2026 05:08

SamuelSchlesinger added this pull request to the merge queue Oct 26, 2026

SamuelSchlesinger mentioned this pull request Oct 26, 2026

guide: polytime example on List.filter (· ≤ p.2) exhausts aesop on main #1148

Closed

Merged via the queue into main with commit 6f7ec65 Oct 26, 2026
4 of 7 checks passed

Navigation Menu

Repository navigation

feat(SAT): prove orthogonal planar 3SAT-3 NP-hardness - #1122

feat(SAT): prove orthogonal planar 3SAT-3 NP-hardness#1122
SamuelSchlesinger merged 117 commits into
mainfrom
feat/orthogonal-planar-three-sat-reduction

edemaine commented Oct 25, 2026 •

edited

Loading

Uh oh!

edemaine commented Oct 25, 2026

Uh oh!

SamuelSchlesinger commented Oct 26, 2026

Uh oh!

SamuelSchlesinger commented Oct 26, 2026

Uh oh!

SamuelSchlesinger commented Oct 26, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

edemaine commented Oct 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

edemaine commented Oct 25, 2026

Uh oh!

SamuelSchlesinger commented Oct 26, 2026

Uh oh!

SamuelSchlesinger commented Oct 26, 2026

Uh oh!

SamuelSchlesinger commented Oct 26, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

edemaine commented Oct 25, 2026 •

edited

Loading