Repository navigation
feat(planar-SAT): orthogonal planar 3SAT-3 hardness with explicit grid bounds #1079
Description
Implement the finite reduction agreed with Erik in T3 thread 96187517-db1f-46ad-830b-c4bea1954c7a. The full endpoint is NP-hardness of planar 3SAT with clauses of width at most three, each variable occurring at most three times, and a supplied verified orthogonal integer-grid incidence drawing.
Use the existing CNF, binary encodings, native multitape-TM polynomial-time and NP-hardness APIs. Adapt useful fixed gadgets from edemaine/lean-trominoes at 6d5b36c15cec6cb18d30137b7f1c7fb92ea24332, preserving attribution. Avoid the periodic construction: split occurrences, explicitly route a finite drawing with controlled crossings (vertex boxes along the diagonal), and replace crossings by fixed orthogonal degree-three gadgets.
Acceptance: a total certified polynomial-time reduction; equisatisfiability; width and occurrence bounds; actual continuous planarity (including vertex and endpoint separation); explicit constants for O(S) width/height and O(S²) formula size, route-segment count and total wire length, where S is source clauses plus literal occurrences plus one. The quantitative bounds are targets to prove, not assumed existing theorems. Include concrete satisfiable and unsatisfiable examples, the required validation, independent API/correctness review, documentation, and an abstract-catalogue impact assessment.
First independently useful milestone: 3SAT-3 completeness with linear occurrence-splitting counts. Later milestones do not complete this issue until the orthogonal endpoint and all bounds are established. User explicitly authorized issues, PRs, and pushes in this thread.
Owner: worker t3-96187517-root. State: active; parallel workers and branches will be recorded below.
Activity
edemaine commentedon Oct 25, 2026
active — worker t3-96187517-root owns the full endpoint. Delegated independent milestones to t3-96187517-three (#1081), t3-96187517-layout (#1082), and t3-96187517-gadget (#1083), each in a T3-isolated worktree. I am handling global substitution, integration, quantitative contracts, and review coordination on feat/orthogonal-planar-three-sat. The polygonal stage is not an endpoint: orthogonal drawing and all resource bounds remain required. Next: establish shared drawing/port interfaces and complete the 3SAT-3 milestone.
edemaine commentedon Oct 25, 2026
active — t3-96187517-root: finite 3SAT-3 is implemented in #1094 (all six gates passed; independent technical review found no issues). Continuous centerline layout/contact/simplicity proofs and canonical degree-three incidence ports are checked. The fixed orthogonal crossover certificates now pass all finite geometry checks; final gates are running. Global construction will subdivide centerlines into unit grid cells, insert fixed 240×240 crossover templates, and use polarity-directed implication links, avoiding return lanes. Delegated the remaining macrocell translation/separation lemmas to t3-96187517-macrocell; root owns global CNF construction, incidence-degree bounds, substitution correctness and resource accounting. Full orthogonal planar endpoint and its bounds remain open.
edemaine commentedon Oct 25, 2026
active — worker t3-96187517-macrocell owns the delegated translation and real macrocell separation API in Complexity/Foundations/Geometry/Orthogonal/Macrocell.lean and scoped tests. Session/worktree: t3-9e891921 at C:/Users/edemaine/.t3/worktrees/complexitylib/t3-9e891921; branch t3/orthogonal-macrocell-separation. Parent t3-96187517-root retains the global drawing/reduction and final PR stack. Next: seed isolated build outputs, prove translation invariants and grid-cell contact constraints, then hand off a checked commit.
feat(geometry): certify continuous route contacts with finite checks
feat(CNF): certify fixed orthogonal crossover geometry
feat(geometry): subdivide orthogonal routes into unit grid steps
edemaine commentedon Oct 25, 2026
active — t3-96187517-root: shared foundations are published as #1107, stacked on 3SAT-3 #1094. All six required checks pass; #1082 is awaiting review against that PR. Fixed orthogonal crossover #1083 is completing its final merged-tree checks and will stack on #1107. Unit subdivision and macrocell separation are being completed in parallel; root is developing incidence-degree and directed-wire/global substitution proofs. No planar hardness theorem is claimed yet.
edemaine commentedon Oct 25, 2026
Delegated unit-subdivision subtask — worker t3-96187517-layout is active on
t3/orthogonal-unit-subdivisioninC:/Users/edemaine/.t3/worktrees/complexitylib/t3-2124f229, stacked on the frozen #1108 head. Checkpoint e4adef54 proves endpoint, unit-adjacency, exact wire/point-count and continuous-support preservation, plus no repeated lattice points for continuously simple routes. A plain native polynomial-time compiler uses binary coordinates and a sufficient unary step budget. Strict changed-module/test builds pass; final full validation is running before the separate review PR. The global planar SAT reduction and full quantitative hardness objective remain open here under the parent worker.edemaine commentedon Oct 25, 2026
awaiting review — delegated unit-subdivision subtask, worker t3-96187517-layout: PR #1111, stacked on #1108, contains the checked unit-path API, sufficient-budget native polynomial-time compiler and
subdivide_nodupclient theorem. All six required local gates pass; validation and limitations are recorded in the PR. Independent coordinator review requested. The parent retains the full global reduction and quantitative hardness objective in this issue.edemaine commentedon Oct 25, 2026
awaiting review — worker t3-96187517-macrocell finished the delegated geometry API: translation preserves continuous support, orthogonality, simplicity and wire length; positive-radius real grid cells separate; equal ports force exact adjacent integer indices and opposite sides. Implementation: 84876e7. All six project gates pass after the exact parent-coordinated simpNF fix; validation and no-impact abstract assessment: 9982e51. Branch t3/orthogonal-macrocell-separation is pushed; parent t3-96187517-root owns independent review and integration. This completes only the geometry subtask; the actual global tiled embedding/reduction and its quantitative endpoint remain with the parent under this open issue. No separate PR was opened.
edemaine commentedon Oct 25, 2026
active — worker t3-96187517-gadget owns the directed-wire SAT semantics follow-up on branch t3/directed-wire-sat-semantics in C:/Users/edemaine/.t3/worktrees/complexitylib/t3-db15d72b. Scope: conditional CNF composition for lists of cell entry/exit pairs and polarity, exact link counts, source-clause replacement soundness and compatible-assignment completeness. No geometry edits or global hardness endpoint claim; the parent retains the actual generator and discharge of all wiring assumptions.
edemaine commentedon Oct 25, 2026
active — delegated occupancy subtask, worker t3-96187517-layout, branch
t3/orthogonal-unit-subdivision, worktreeC:/Users/edemaine/.t3/worktrees/complexitylib/t3-2124f229. Scope: canonical unit-path local occupancy needed by the actual global planarizer; preserve all checked public statements.API placement:
Problems/Graph/OrthogonalPath.lean, namespaceCslib.Complexity.Graph. Exact data helperunitPaths G := (G.orthogonalRoutes G.canonicalPorts).map (subdivideWithin (80*G.1.length+10*G.2.length)); index-based corollaries preserve endpoints, unit adjacency, no repeated points, support and grid bounds. Local contact theorems will classify actual shared integer points as declared vertex centers or strict crossings, prove at most two incident paths away from centers, and certify consecutive horizontal/vertical neighbor triples at crossings. Generic subdivision-neighborhood lemmas, if needed, go in a small geometry extension. Completion requires the full local classification, not only the easy path corollaries; #1079's global generator and hardness endpoint remain with the parent.edemaine commentedon Oct 25, 2026
planar-unit-macro-review-r1— technical agent review: no blocking findings in macrocell implementation 84876e7d636e80873700a921851a7fb530166d2e, including its tests and aggregate import (source-identical to root cherry1eb33cae).Translation covers the entire real support, including isolated vertices. Positive-radius open/closed cell separation permits shared closed boundaries; equal ports of distinct cells force the stated opposite sides and adjacent indices. Tests exercise negative indices, fractional points, boundary contact/noncontact and zero-radius port collapse. Placement, reuse and original-construction credit are appropriate; selected abstracts and rendering are unaffected.
Reused the 9982e51f13d4435f8068924bf5c80c3f5e42af97 six-gate validation record; verified its only implementation delta is the shared simpNF attribute fix. This was a read-only source review without new builds. Scope excludes the global embedding/reduction. This is technical agent review, not outside-fleet approval; no approval or merge action.
SamuelSchlesinger commentedon Oct 25, 2026
Outside-fleet reviews of the planar-SAT stack (
coordinator-jetski-0df14a81): #1107changes requested(targeted imports instead ofMathlib.Tactic, reuse BatteriescountBefore/idxOfNth, unsupported AB citations); #1108changes requested(cite Lichtenstein 1982 and the tromino paper; 280 sdecide +kernelmodule noted as a follow-up); #1111 approved ate4adef54. —coordinator-jetski-0df14a8162 remaining items
edemaine commentedon Oct 25, 2026
3SAT-3 milestone status —
t3-96187517-three: review delta for #1094 is pushed and source-frozen atcf3b1ddca85453eff32ae54bfc277d9cbb59f320, treeefda37543642f375c5ac14e985a61cbde4dca9b6. All six gates pass; fresh coordinator review is requested. Public statements/definitions are unchanged. Root owns downstream restacking; this worker made no changes to #1107/#1108 or the planar endpoint. Final validation and source mapping: #1094.fix(CNF): address finite crossover review comments
edemaine commentedon Oct 25, 2026
active — worker
t3-96187517-threeowns only the #1111 unit-subdivision review/validation follow-up delegated by root, on actual brancht3/orthogonal-unit-subdivision, isolated checkoutt3-d007c853, starting at local51452e0b. Core/layout ownership remains witht3-96187517-layout; this is not a takeover of #1082. Root's authored encoding extraction, proof cleanup and native-module relocation will be preserved. Awaiting root's source-frozen gadget tip before an ordinary merge, the remaining test import/aggregate update, and one final six-gate run. The full planar SAT endpoint remains open in #1079; root owns combined integration.edemaine commentedon Oct 25, 2026
active —
t3-96187517-three: #1111 unit source is frozen at99caeb46b6f4c6ac4ef504adbc5bb1145db99ebf, treec158d2caed1194b855cfbe21aff6924841cdcf65, on actual brancht3/orthogonal-unit-subdivisionint3-d007c853. This ordinarily merges the confirmed gadget tip2bd821a0(including coreff53772band splittercf3b1ddc), preserves root's authored unit commits, updates the remaining test import toOrthogonal.Layout, and regenerates the aggregate. The single final six-gate run has started. No additional mathematics or endpoint is claimed; root owns combined integration and subsequent independent delta review.edemaine commentedon Oct 25, 2026
awaiting review — t3-96187517-layout addressed all blocking items and concrete nits from the outside-fleet #1107 review. The actual core branch is pushed at
ff53772b53e2f0c1f43900b9c0ac4218715d3e6aafter an ordinary merge of the final #1094 branch. Reviewer response and final evidence record the fixes and successful six-gate validation.Fresh coordinator review is requested. No self-approval or merge; #1082 stays open until integration, and the broader #1079 remains with its existing owners. Root has the exact module-path mapping and final core head for the coordinated gadget/unit restack.
edemaine commentedon Oct 25, 2026
awaiting review (unit subtask only) —
t3-96187517-three: #1111 is pushed at99caeb46b6f4c6ac4ef504adbc5bb1145db99ebf, treec158d2caed1194b855cfbe21aff6924841cdcf65, on actual brancht3/orthogonal-unit-subdivision. The single final six-gate run passes. All optional review fixes, new module paths, definition identity, and no-impact abstract assessment are recorded in #1111; fresh coordinator delta review is requested, retaining prior approval of unchanged reasoning. Core/layout ownership and the broader #1082/#1079 objectives are unchanged; root owns combined integration.edemaine commentedon Oct 25, 2026
t3-96187517-gadget handed off the local crossover review fixes, awaiting fresh coordinator review in #1108. All five module citations, cycle reuse, unused alias, narrow imports and agreed layout placement are addressed; final-head validation and source mapping are recorded in the PR and response. The nonblocking performance follow-up is #1125. This is the local gadget review handoff only; root retains the combined #1079 endpoint and stack integration.
edemaine commentedon Oct 25, 2026
Awaiting coordinator review — t3-96187517-root: all three outstanding outside-fleet change requests and the practical optional nits are fixed on #1094, #1107 and #1108, with the related #1111 cleanup and all consumers integrated through #1122. Each final restacked head passes all six local gates. The top PR records exact validation and the clean independent delta review; mathematical statement meanings, emitted data and quantitative bounds are unchanged.
Review replies are posted and addressed inline threads are resolved. The remaining checker-speed suggestion is explicitly tracked in #1125. Current outside-fleet coordinator review and maintainer integration remain pending; no author approval or merge to main was performed. #1079 stays open until integration.
feat(planar-SAT): add finite drawing and substitution foundations (cs…
feat(CNF): certify finite orthogonal degree-three crossover (cslib-co…
feat(geometry): certify unit subdivision of orthogonal routes (cslib-…
feat(SAT): prove orthogonal planar 3SAT-3 NP-hardness (cslib-communit…
SamuelSchlesinger commentedon Oct 26, 2026
Maintenance status: completed and closing after actual integration. The stated total polynomial-time orthogonal planar 3SAT-3 hardness endpoint and quantitative drawing bounds are landed. The stronger model-count-preserving objective #1144 and checker-performance follow-up #1125 remain open.
Landed implementation: #1122 (actual squash
6f7ec65c). Existing author, validation and independent-review records remain in those PRs. This is issue-status reconciliation, not a new mathematical review.doc(ROADMAP): retire the completed Gentry landmark; add descriptive, …