Repository navigation
feat(drawing): finite orthogonal crossing layouts with linear grid bounds #1082
Description
Build reusable finite integer-grid orthogonal drawing foundations and the explicit controlled-crossing layout for degree-at-most-three incidence graphs. Use fixed disjoint vertex boxes along the diagonal, separate endpoint columns and edge track rows. Prove endpoint correctness, orthogonality, no unintended vertex contacts, isolated transverse crossings/no overlaps, and explicit linear width/height and quadratic crossing/segment/wire-length bounds. Reuse existing Graph/CNF APIs and upstream/mathlib geometry rather than duplicate notions; coordinate the interface with the parent worker. This independently useful milestone is a crossing drawing, not a planar drawing or SAT hardness theorem. Owner: worker t3-96187517-layout. State: active.
Full objective: #1079
Activity
edemaine commentedon Oct 25, 2026
Worker t3-96187517-gadget (#1083): please post the shared drawing interface/module early. I am starting ordinary CNF semantics and fixed local splitting; will keep coordinates private until your drawing API is available. Need integer points, axis-aligned segment routes, exact endpoints, continuous disjointness except shared endpoints, boundary isolation, and explicit box bounds.
edemaine commentedon Oct 25, 2026
active — worker t3-96187517-layout claims #1082 on branch
t3/finite-orthogonal-layout-bounds, worktreeC:/Users/edemaine/.t3/worktrees/complexitylib/t3-2124f229.Proposed API: small reusable
Foundations/Geometry/Orthogonalmodule for integer points, polygonal route lists, real segment support using Mathlib, orthogonality, and wire length. A separateComputability/Complexity/Problems/Graph/OrthogonalLayoutmodule will tie finite position/route lists to the existingGraphedge indices and implement diagonal boxes, three endpoint ports, and unique upper tracks. Concrete bounds and contact certificates will be stated separately from construction data so incomplete geometry cannot be mistaken for a planar layout theorem. This milestone does not finish #1079; crossover and SAT splitting remain outside this issue.edemaine commentedon Oct 25, 2026
active — t3-96187517-layout published shared finite-route foundations in e2989c78, branch
t3/finite-orthogonal-layout-bounds. The foundation elaborates without warnings using isolated output paths. Full gates remain pending during cache seeding. Next: finish checking the explicit diagonal-box layout, quantitative bounds, and contact classification; #1082 and the broader #1079 remain open.feat(geometry): construct simple orthogonal crossing routes with line…
feat(graph): assign canonical ports to bounded incidence occurrences
feat(graph): bind finite crossing layouts to graph edge occurrences
edemaine commentedon Oct 25, 2026
active — t3-96187517-layout published graph drawing binding, building on the checked finite geometry and canonical-port commits. Continuous simplicity, no incidental vertices, strict transverse contact classification, linear sides, five segments per edge, quadratic wire length, and a finite
2m²crossing-site cover are proved. All changed module target builds pass with strict warning/I/O gates; full project validation remains pending final integration. Next: unit subdivision for the parent SAT macrocell construction, regression instances, and full gates. This is a crossing-layout milestone; #1079's planar SAT construction remains with the parent worker.feat(geometry): construct simple orthogonal crossing routes with line…
feat(geometry): subdivide orthogonal routes into unit grid steps
edemaine commentedon Oct 25, 2026
awaiting review — t3-96187517-root integrated t3-96187517-layout’s checked geometry/port/Graph APIs into #1107 (stacked on #1094), with shared contact certificates and CNF incidence construction. All six required gates pass on b9d66cd. Source and validation are recorded in the PR. This milestone is a controlled-crossing drawing; the full planar SAT endpoint remains open in #1079. Independent API/correctness review is requested.
edemaine commentedon Oct 25, 2026
awaiting review — t3-96187517-layout: #1082's finite crossing-layout milestone is implemented in PR #1107, with source implementation by this worker and integration by t3-96187517-root. The PR records the combined core's successful six-gate validation and remaining scope. Coordinator review requested; keep this issue open until integration. The full planar SAT objective #1079 remains open. Unit subdivision continues as a separate delegated subtask for the next stack layer.
edemaine commentedon Oct 25, 2026
active — t3-96187517-layout resumes #1082 on actual PR branch
feat/orthogonal-planar-three-satatb9d66cd4, isolated worktreeC:/Users/edemaine/.t3/worktrees/complexitylib/t3-2124f229; root's integration checkout is untouched. Parent assigned all three blocking items and concrete nits from outside-fleet changes requested: targeted tactic imports, Batteries occurrence-rank reuse, accurate original-construction references, module-path mirror, nonvacuous incidence/ports/layout tests and proof/whitespace hygiene.Also providing the requested low-level tail helpers and moving the existing unit-length axis lemma into Orthogonal for the separately owned unit review fixes. No bibliography edits, no other branch merges, no new mathematical endpoint. Full six gates will run on the final core head; #1079 remains open.
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.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 bounded crossing-layout foundations and unit-subdivision milestone are landed.
Landed implementation: #1107 (actual squash
43d1e572), #1111 (actual squash79ffc878). Existing author, validation and independent-review records remain in those PRs. This is issue-status reconciliation, not a new mathematical review.