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

Replace the directed-wire planar 3SAT-3 reduction with a parsimonious reduction, stacked on #1122. The existing equisatisfiable reduction remains a valid milestone until the stronger compiler is checked.

Acceptance criteria:

Prove exact model-count preservation for occurrence splitting and the total 3SAT-to-3SAT-3 compiler on width-at-most-three inputs.
Certify unique extensions through the existing crossover and its internal occurrence splitting.
Emit a width-at-most-three, occurrence-at-most-three formula with an actual integer orthogonal incidence drawing and a bijection of satisfying assignments.
Retain polynomial-time computation, linear grid sides, and quadratic formula/segment/total-wire costs; recover the decision-hardness theorems and remove superseded wiring.
Validate and independently review the final change, including any affected abstracts.

Worker t3-96187517-parsimony owns this work on feat/parsimonious-planar-three-sat, based on feat/orthogonal-planar-three-sat-reduction. Delegated subtasks: occurrence model counts (parsimony-occurrence), crossover uniqueness (parsimony-crossover), and read-only wiring design (parsimony-wiring-design). The parent owns the actual planar compiler and integration.

Follow-up requested by the user: the Another Solution Problem (ASP) framework, with explicit polynomial-time solution bijections. This is recorded in ROADMAP.md and is outside this implementation. A general parsimonious SAT-to-3SAT conversion is also separate; the present source is width-at-most-three CNF.

Reference: Hunt, Marathe, Radhakrishnan and Stearns, The Complexity of Planar Counting Problems, §3, Theorem 3.2 and Claim 3.3, https://doi.org/10.1137/S0097539793304601.

active — worker t3-96187517-parsimony owns the parsimonious stacked change on feat/parsimonious-planar-three-sat, based on #1122. Occurrence-count and crossover-uniqueness proofs are being checked in parallel; the parent is resolving the smallest degree-three geometric wiring construction. Next: finish these local certificates and fix the actual compiler design before replacing the global reduction.

active — t3-96187517-parsimony: occurrence splitting and the total guarded 3SAT-to-3SAT-3 counting reduction are checked, including boundary cases. The new compiler uses paired implication lanes, eight-port ordinary rings and a 57-variable paired crossover. Root owns global assignment/count correspondence; delegated workers own geometry, native polynomial time/bounds and fixed-crossover certificates. The original compiler is still the endpoint until the stronger drawing, occurrence and count theorems pass. ASP is recorded as a separate ROADMAP follow-up.

active — t3-96187517-parsimony: the actual model-count, drawing, occurrence-three, native polynomial-time and quantitative modules now pass strict targeted Lean checks; top endpoint also passes. Two independent internal technical reviews found no blocking issues in counting or geometry/resources (coordinator approval still required). The old directed output compiler is being removed after extracting its shared path machinery. Next: validate that cleanup, run all six full gates, and submit the stacked PR against #1122. No merge or self-approval.

awaiting review — t3-96187517-parsimony: implementation and full local validation are complete in #1147, stacked on #1122. The PR records exact revision, source mapping, internal reviews and the Windows-only optional guide linker limitation. Outside-fleet coordinator review is requested before integration; issue remains open until merge. ASP is retained as a separate ROADMAP follow-up.

active — t3-96187517-parsimony resumes the requested #1147 restack. Parent #1122 is merged. I will split the existing reviewed development into dependency-ordered PRs on current main, preserve the complete endpoint, validate each layer, and post internal evidence with an explicit outside-review request. No competing ownership claim appears in the issue.

active — t3-96187517-parsimony retains ownership of the #1147 restack; no takeover claim is present. Eight layer scopes and their compatibility extraction are prepared, with a clean independent API/import review and exact final-source identity to the original reviewed mathematics. The refreshed strict build passes. A full test attempt hit Windows allocation failures; validation is rerunning with lower concurrency before the layers are committed and published.

feat(CNF): preserve model counts under occurrence splitting

awaiting review — t3-96187517-parsimony: the requested refresh and split are complete, from #1147 (now based on main) through the endpoint PR #1180. Every layer passes all six local gates, hygiene and description-name checks. The internal review, source-identity evidence, full stack and named outside-review request are recorded once at #1147 (comment). The full objective remains open until integration; no self-approval or merge.