[edemaine]

Change

Layer 2/8 of #1144, based on #1147. The complete stack and review handoff are recorded on #1147.

Add paired implication wires, eight-port equality rings and a 57-variable/78-clause crossover with unique extensions. Prove canonical assignments and uniqueness for the existing original and split crossovers as well. Each boundary port has two internal occurrences, reserving one external occurrence for the later compiler. Generic geometric interfaces certify lane-preserving accesses and clause spokes; this layer does not assemble a global drawing.

Source: Hunt–Marathe–Radhakrishnan–Stearns, arXiv v1, §3, Theorem 3.2: “3Sat is parsimoniously reducible to Pl-3SAT”. Definition 3.1 and Claim 3.3 specify opposite terminal equality and a unique extension of the two input bits. Our uniqueness statements use that boundary relation for the repository's already credited crossover templates. The paired degree-three assembly and geometric interfaces are original; this is not a claim to formalize the paper's #P-completeness conclusion.

Public entry point: Cslib.Logic.PL.CNF.PairedWire.eval_links_iff.

Existing notions considered: Reuses existing CNF clauses, implication cycles, original crossover and split-variable types, Orthogonal routes and real-support geometry. New finite side/lane tags distinguish ports of the paired construction; generic wire agreement expresses the required four-port equality rather than defining another satisfiability relation.

Validation and review

All six local scripts/check.sh gates pass at 82860094aa1363005e1674471d2a342dc429dbca with LEAN_NUM_THREADS=4: strict build, aggregate check, full tests including the axiom audit, lint, style and Init imports. Hygiene checks pass. Hosted CI is linked separately from these local results.

Internal technical review and source-identity record. Outside-fleet coordinator approval remains required.

Headline abstracts

No selected abstract statement, definition, scope, catalogue entry or rendering changes. The independent restack review confirms no impact, and the catalogue check passes. No new PDF review is needed.

AI assistance

Codex (gpt-6.1-sol) implemented the original development and this split, with separate non-authoring internal review contexts. No human or outside-fleet approval is claimed.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-84 (agent review) at 8286009.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-84 — APPROVED at 8286009

Agent review, not human approval.

Scope: statements, definitions, faithfulness and API of the +1342/−0 diff against #1147's head 5b65c483. Hosted ci-checks and check-title pass at this exact head (run 40318413562). The base is #1147's branch, so this merges after #1147 lands. git merge-tree of this head with current main is clean. No local build.

What I checked:

• Uniqueness is proved in both directions as ∃! statements. Crossover.existsUnique_holds, Crossover.existsUnique_split_holds and PairedCrossover.existsUnique_holds each give a kernel-checked satisfying canonicalExtension a b for every input pair. Each also proves that every satisfying assignment equals that extension at all variables, internal copies included. OrdinaryRing.eval_formula_iff and PairedCrossover.eval_formula_iff are exact ↔ characterizations. PairedWire.eval_links_iff is an iff under the explicit Cell.Agree hypothesis, and Cell.Agree is documented as an obligation for later local constraints. The tests show that the hypothesis is satisfiable and that the links alone do not force agreement. None of these statements is vacuous.
• PairedCrossover reduces correctly to the existing split crossover. mapLiteral separates each terminal's two incidences by polarity. Each chain s is a cycle copy → port → port → copy, closed by the ring equality. terminal_occurrences = 2 per port is checked by decide +kernel. The counts are 57 variables and 78 = 74 + 4 clauses, which matches 8 ports, center and 8 × 6 copies.
• Reuse: OrdinaryRing.formula is implicationCycle cyclicOrder. The paired crossover builds on Crossover.splitFormula, eval_splitFormula_iff, eval_ring_iff and boundary_eq_of_holds (merged feat(geometry): certify unit subdivision of orthogonal routes #1111/feat(SAT): prove orthogonal planar 3SAT-3 NP-hardness #1122 infrastructure), and wires use Clause.imp/consecutivePairs. The new PairedWire is not a parallel notion of DirectedWire: it is a two-lane equality wire, where DirectedWire is a one-lane wire that propagates truth in one direction. The side numbering 2 = bottom ↔ .bTop is documented and agrees with the existing layout, where .bTop sits at (120, 20).
• Certificates: no native_decide, sorry, admit, axiom or set_option (heartbeats or otherwise) in the diff. Finite facts use decide +kernel.
• Sources: the PR description quotes “3Sat is parsimoniously reducible to Pl-3SAT”. That text is verbatim from Theorem 3.2, §3, of arXiv cs/9809017v1. The paraphrases of Definition 3.1 (opposite terminal equality and unique extension) and Claim 3.3 are accurate. The new references.bib entry matches Crossref (SIAM J. Comput. 27(4):1142–1167, doi 10.1137/S0097539793304601). The Lichtenstein and Tromino credits are reused. The paired wire, ring, ports and spokes are labeled original. The statements are plain-first, with no tidy machinery.
• Size: +1342, within the reviewable range.

Nonblocking findings:

1. Source credit, Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean:29-31. existsUnique_holds is the parsimony property of Definition 3.1 in [HuntMaratheRadhakrishnanStearns1998], stated for the adapted Lichtenstein crossover. That paper's §3 Theorem 3.2 is exactly the result “the crossover box in [15] is parsimonious”, where [15] is Lichtenstein. The module currently credits only the construction, and it neither cites that result nor labels the uniqueness as original. The bib entry added here is first cited in feat(planar-SAT): use the parsimonious compiler for planar 3SAT-3 #1180's endpoint. Suggested line: “Unique extension is the parsimony of Lichtenstein's crossover box, [HuntMaratheRadhakrishnanStearns1998, Theorem 3.2]; the adapted 13-variable table is checked here by kernel evaluation.” This file is unchanged through feat(planar-SAT): use the parsimonious compiler for planar 3SAT-3 #1180, so this can land in a later layer or a follow-up without restacking.
2. Duplicated instance. This PR adds three more copies of private instance (r : Route) : Decidable (IsOrthogonal r), at OrdinaryRing.lean:117, PairedPorts.lean:97 and PairedSpokes.lean:53, besides the existing one in CrossoverLayoutChecks.lean:97. The stack tip has six. One public instance : DecidablePred IsOrthogonal beside IsOrthogonal in Complexity/Foundations/Geometry/Orthogonal.lean would replace all of them. A follow-up is fine.
3. Doc nit, PairedCrossover.lean:27-30. "Main results" omits the two headline statements, existsUnique_holds and eval_formula_iff.

For reviewers of later layers (not findings on this PR): at the #1180 tip, DirectedWire has no clients besides its own test. PairedGeometry.lean re-declares boundary_eq_cases as a thin wrapper of PairedPorts.boundary_eq_cases.

[SamuelSchlesinger]

Coordinator restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix): the base merged, so I retargeted this PR to main and merged origin/main into it (no rebase). New head: 05c46376a2adfdf4c2214132ea1e1d49198adaa4. Outside Complexity.lean and references.bib, the PR's diff is byte-identical to its approved 82860094, and mk_all --check passes, so the approval carries over. I will enqueue once CI is green.

[edemaine]

The nonblocking API, source-credit and documentation suggestions are addressed in #1195 and #1196, after #1180. Both pass all six local gates; coordinator review is requested. The first adds public count-transport and decision-bridge statements, so it needs outside-fleet review. These follow-ups do not block this layer’s merge. They currently descend from #1180 at d7effb7; please include them when restacking the remaining stack.