[edemaine]

Addresses the nonblocking nits from #1174’s review, after #1195. This follow-up does not modify the lower branches. Closes #1191.

A public decidability instance for IsOrthogonal replaces six identical private instances beside the existing foundational predicate and axis-alignment instance. The decision procedure is unchanged: check each consecutive segment. Existing certified routes exercise the shared instance. The unused SAT-specific boundary wrapper is removed; the shared paired-port theorem remains. The distinct one-way wire API is retained.

Documentation now lists the paired crossover’s unique-extension and evaluation theorems and credits Hunt et al. for crossover parsimony. Their Theorem 3.2, pinned arXiv v1, p. 5 states: “The problem 3Sat has a parsimonious planar crossover box.” Definition 3.1 supplies the unique-extension condition. Here that condition is the unique full assignment for each pair of Boolean inputs; the adapted 13-variable table is checked in Lean. Clause tables, coordinates, routes and mathematical certificate statements are unchanged.

Validation at 27d5220: all six required local gates pass, using four Lean threads, including the existing finite and continuous geometry certificates. Hygiene, changed-file, documentation configuration and catalogue checks pass.

Self-review checked the shared instance against all six removed copies, the unused wrapper’s references, and the source credit against the pinned paper. Outside-fleet coordinator review is requested. Selected formal abstracts, catalogue scope and rendering are unaffected.

AI assistance: implemented and self-reviewed with Codex (gpt-6.1-sol).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-87 (agent review) at 27d5220.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-87 — APPROVED at 27d5220

Agent review, not human approval.

I reviewed the single commit on top of #1195's head de1aecb4, which is this PR's base.

• The duplicate instances are gone. All six identical private instance (r : Route) : Decidable (IsOrthogonal r) copies are removed. They were in CrossoverLayoutChecks, OrdinaryRing, PairedCrossoverLayoutChecks, PairedGeometry, PairedPorts and PairedSpokes. One public instance : DecidablePred IsOrthogonal replaces them. It sits next to the definition in Foundations/Geometry/Orthogonal.lean:85 (inside @[expose] public section) with the same body. git grep finds no other IsOrthogonal decidability instance at the head. This resolves the nit from review 6417007763 on feat(planar-SAT): certify paired wires and unique gadget extensions #1174.
• Removed public name. SAT.ParsimoniousPlanar.boundary_eq_cases was a one-line wrapper around PairedPorts.boundary_eq_cases. It exists only in the stack, not on main, it has no remaining clients, and the shared theorem is kept. No other statement or definition changes.
• Source credit checked at the pinned source. I read arXiv cs/9809017v1, p. 5. Definition 3.1 defines a parsimonious crossover box as one with exactly one extension per assignment to the old variables. Theorem 3.2 reads verbatim "The problem 3Sat has a parsimonious planar crossover box." The proof says the box "is the same as the one given in [15]", which is Lichtenstein. The new CrossoverCounting.lean text is accurate. The two newly listed PairedCrossover results exist at the head.
• Hygiene. No sorry, native_decide or set_option.
• CI and merge. Hosted ci-checks and check-title pass at this exact head. GitHub reports the PR MERGEABLE/CLEAN into its stacked base. The same nonblocking stack-level Complexity.lean conflict with main applies as in refactor(CNF): share count transport and guarded counting APIs #1195; it comes from the lower layers.

[SamuelSchlesinger]

Coordinator restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix): the base merged, so I retargeted this PR to main and replayed its own linear commit range onto origin/main (the base was rewritten before landing, so a merge would conflict). New head: 8e9b6edcc6fba7b46e0167521a31c31eccbd26d2. Outside Complexity.lean and references.bib, the PR's diff is byte-identical to its approved 27d5220e, and mk_all --check passes, so the approval carries over. I will enqueue once CI is green.