[SamuelSchlesinger]

Adds case-analysis lemmas for the paired planar compiler's output records and uses them where proofs unfolded placedClauses and originalClauses by hand (SAT survey F6, plan #4737).

Change

PairedCompile.lean gains three lemmas:

• mem_links: a seam clause of a route is link sites e.1 e.2 0 or link sites e.1 e.2 1 for a step e of r.dropLast.consecutivePairs.
• mem_placedClauses: an output record is one of four kinds: an original clause, a clause of the ordinary ring or the crossover in its cell, or one of the two lane clauses of an occurrence-path step.
• exists_occurrence_of_mem_originalClauses: each literal and route of an original clause record (c, p, rs) is the final literal or final incidence of an occurrence (i, j, x) ∈ occurrences φ, with the sign of x.

Thirteen proofs used to start with simp only [placedClauses, List.mem_append, List.mem_flatMap] at h and a nested rcases. Ten are in PairedGeometry, and one each in PairedCounting, PairedBounds and PairedSize. In the link case they also needed List.mem_flatMap.mp and a List.mem_cons simp. They now start with one rcases mem_placedClauses.mp h with … | ⟨o, ho, e, he, h⟩, and the link case goes straight to rcases h with rfl | rfl. Four other sites use the same lemmas: the goal-side use in PairedCounting.sourceVariable_mem_rawFormula, and the standalone links destructurings in width_links, links_stat and link_position_not_open.

Nine original-clause cases used to take three List.mem_map.mp steps and then rebuild (ci.2, lj.2, lj.1) ∈ occurrences φ with List.mem_flatMap.mpr. Six are in PairedGeometry, one is in PairedCounting and two are in PairedBounds. They now take one obtain ⟨i, j, x, ho, rfl⟩ := (exists_occurrence_of_mem_originalClauses hpc).2 _ hr, or .1 for literals. In route_variable_contact, the clause-index bound now comes from mem_occurrences, not List.mem_zipIdx. The statement names the record and occurrence components, so it adds no positional projection chains.

The proofs are otherwise unchanged, and so are all existing definitions and statements. This is a refactor with no new mathematics. Net: 5 files, +86/−132.

Left for later

• PlacedClause stays a tuple; making it a structure is refactor: replace tuple abbreviations and bare product instances with structures and enc_structure #4385 Tier 2.
• PairedOccurrence.lean (in the queued refactor(Complexity/SAT): certificate assignment lemma and Problems/SAT/Units #4756) and PairedPolyTime.lean (perf(PolyTime): make ComputableInPolyTime irreducible #4150) are untouched. Neither destructures membership. The sum and map unfoldings of placedClauses and originalClauses have a different shape, so they keep the definitions. They are the PairedBounds route costs, PairedSize, the PairedGeometry positions and PairedPolyTime. The zip-based originalClause_endpoints also keeps them.
• The repeated-proof-block notice now lists one pair: raw_variable_cell_kind and raw_variable_cell_membership in PairedGeometry. Both perform the same four-way split of a raw variable's source record before drawing different conclusions. A variable-level corollary ("each raw variable is a final signal, an ordinary or crossover port, or a link signal") would merge them. That changes the shape of the API, so it is left out of this PR.

Manual impact

• Operator's Manual: no edit needed. No chapter cites these proofs or line anchors in these files.
• Agent Operator's Manual: no edit needed. It does not cover these APIs.

Validation

At 5c4bb1b:

• buildslot.sh lake build --wfail built all five changed modules and every direct importer of them. The importers are PairedOccurrence, PairedPolyTime, PairedSemantics, PlanarThreeSATThree, and the tests PairedCounting, PlanarBounds, PlanarCompile, PlanarGeometry and PlanarSemantics.
• check_operator_manual.py passes, and so does check_hygiene.py --check-simp on the changed files. check_encoding_readability.py and check_projection_chains.py pass against origin/main. proof_copies.py reports only the pair above.
• No open PR touches the five changed files.

Hosted CI runs the full validation.

AI assistance

Written by Jetski worker session f9cb2f1f (plan #4737). Not yet reviewed.

Part of #4737.

[edemaine]

Landed as e0873525 at 2026-11-12 21:22:44 UTC, from exact 5c4bb1b277205bb74b1a98c7e01fb82394a628f9. The separate current-head independent Jetski review covers the later original-clause helper delta, final validation and actual notice. This root session reviewed the earlier own layer below and verified actual landing; it did not approve that later delta or run the queue action. The bounded paired-clause refactor is integrated; #4737’s broader objectives and the documented occurrence/raw-variable helper follow-ups remain separate.

APPROVE the source/API refactor at f1e9634be20fb24115431215761e7de57f33b90e; final hosted validation remains pending. Independent non-author/non-design agent reviewer-codex-edemaine, reviewing in this coordinator session. This is agent review, not human approval.

I read the complete five-file delta and the paired compiler definitions, geometry/count/bound/width callers and existing concrete tests. mem_links exactly characterizes the two lane records for each consecutive pair of r.dropLast, including empty/short routes. mem_placedClauses gives precisely the original, ordinary, crossover and occurrence-link cases, with the correct source occurrence and step witnesses. The rewritten cases preserve endpoints, counts, bounds and assignment arguments; the two callers that reconstruct link membership use the reverse direction correctly. All247 existing declaration headers in the five files are unchanged; only the two membership lemmas are added. Definitions, attributes, imports and resource/encoding contracts are unchanged. The existing empty source, empty clause, repeated literals, tautology, contradiction and actual-crossing tests remain meaningful clients; I did not rerun them locally.

The helpers belong beside the construction and remove the repeated outer case plumbing from its real consumers. The retained original-clause cases perform the same short map-membership eliminations as before; they introduce no new copied mathematical argument. The description records the concrete originalClauses/occurrence helper follow-up rather than claiming that later usability gap complete. No tuple migration, compatibility aliases or unrelated proof redesign is required here. Source credit is preserved.

Both-manual no-edit assessments are valid: this proof-interface change preserves the compiler's model, endpoint and user procedures; no affected manual link/line anchor or executable instruction changes. Agent roles/handoffs are unchanged. No ROADMAP, result/abstract or upstream-marker change is needed. The manual workflow's actual path selector does not run for these five Lean-only files, so no fresh PDF build/render claim is made.

Native CI43298270841 and Guide43298270876 were running at the meaningful check read. All six final gates, current affected-client coverage and the three completed actual advisory reports remain integration holds; the author's focused checks supplement this review. Exact changed/dependency blobs and bounded source searches were inspected; a broad read-only object search encountered a promisor-object failure, so it supplies no whole-repository absence claim. No source edit, local Lean/build/cache probe or queue action. Existing worker f9cb2f1f retains implementation ownership; parent coordinator retains final integration after validation.

[edemaine]

APPROVE the bounded source/API refactor at f1e9634be20fb24115431215761e7de57f33b90e — independent non-author agent reviewer-codex-edemaine. The canonical review records the exact membership equivalences, preserved declarations/clients, both-manual no-edit assessment and search limits. Current native six gates, Guide and actual final notices remain integration holds. No source edits or local builds; agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 130c4b0f) of 5c4bb1b: approve

Agent review, not human review. Covers the full PR at this head, including the originalClauses delta f1e9634..5c4bb1b that the earlier reviewer-codex-edemaine approval (at f1e9634) predates.

• Statements. mem_links and mem_placedClauses are exact iffs, each proved by one simp only unfolding of the definition, so they state precisely the definitional case split (four placedClauses summands in definition order; two lane records per step of r.dropLast.consecutivePairs). The link case is inlined into mem_placedClauses rather than left as pc ∈ links …: the other 12 .mp clients go straight to the two lane cases, and only two (width_rawFormula, raw_assignments_agree) refold with mem_links.mpr, so that is the right trade. Neither is @[simp]; keeping the pair binder e (instead of splitting it into two variables) is deliberate, since clients use he whole (List.of_mem_zip, prefixStep_mem, consecutivePairs_dropLast). exists_occurrence_of_mem_originalClauses is a one-way projection with named components; the occurrence (i, j, x) and sign x.2 are what every migrated caller needs, and route_variable_contact now gets the clause bound from mem_occurrences, which is cleaner than the old List.mem_zipIdx arithmetic.
• Migrated sites. All 14 simp only [placedClauses, List.mem_append, List.mem_flatMap] + nested-rcases openings are gone (Geometry 10, Counting 2 incl. the goal-side .mpr, Bounds 1, Size 1), as are the link-case List.mem_flatMap.mp + List.mem_cons simp pairs and the 4 standalone links destructurings. The 9 original-clause sites drop three List.mem_map.mp steps plus the (ci.2, lj.2, lj.1) ∈ occurrences rebuild to one obtain. Each is genuinely shorter; no proof got longer except the two one-token mem_links.mpr refolds.
• Remaining hand-written destructuring (git grep at this head). No simp … placedClauses/links/originalClauses … mem_flatMap membership unfolding remains in the paired files; the remaining unfoldings are map/sum/length computations (PairedBounds costs, PairedSize, PairedGeometry positions, PairedSemantics, PairedOccurrence, PairedPolyTime), which the PR body correctly lists as a different shape. The originalClauses sites still doing List.mem_map.mp hpc (originalClause_endpoints, originalClause_routes_nodup_at, placedClause_route_count, original_*_positions_disjoint) need the clause index, the zip pairing or the centre, which the projection lemma deliberately does not expose. Fine as is.
• Placement and scope. The lemmas sit in PairedCompile right after the definitions they characterise, and the module docstring names them. PairedOccurrence (refactor(Complexity/SAT): certificate assignment lemma and Problems/SAT/Units #4756, now merged) and PairedPolyTime (perf(PolyTime): make ComputableInPolyTime irreducible #4150) are untouched. No sorry/native_decide/heartbeat changes; no statement, definition, attribute or import changes elsewhere.
• Other reviews. The only other review is reviewer-codex-edemaine's APPROVE at f1e9634 (review + canonical comment); it raises no findings and no inline threads exist. Its noted originalClauses follow-up is what this delta adds.
• Manuals. No manual, results/ or test file cites these proofs, the new names or line anchors in the five files; no edit needed in either manual.
• Conflicts. git merge-tree clean against current main, which now includes refactor(Complexity/SAT): certificate assignment lemma and Problems/SAT/Units #4756.
• CI. ci-checks and guide passed on this head (run 43300926593). Parallel-definition: no candidates (0 examined). Duplicate-statement: none among 22 examined. Repeated-proof-block: one pair, raw_variable_cell_kind / raw_variable_cell_membership; on main they already share the same placedClauses split with different conclusions, and the refactor only makes the shared opening uniform enough to be detected (see follow-up below). The PR-description-names notice flags r.dropLast.consecutivePairs (an expression, not a declaration; false positive) and PairedCounting.sourceVariable_mem_rawFormula (the declaration is Cslib.Complexity.SAT.ParsimoniousPlanar.sourceVariable_mem_rawFormula in PairedCounting.lean; body wording nit, non-blocking).

Non-blocking follow-ups (not for this PR):

• The step "(c, i) ∈ φ.zipIdx and (l, j) ∈ c.zipIdx give (i, j, l) ∈ occurrences φ" is still spelled out by List.mem_flatMap.mpr ⟨_, _, List.mem_map.mpr ⟨_, _, rfl⟩⟩ in four places (PairedGeometry.originalClause_endpoints, twice in originalClause_routes_nodup_at, PairedSemantics line 282) plus inside the new lemma. A Cslib.Logic.PL.mk_mem_occurrences_of_mem_zipIdx beside occurrences in Logics/Propositional/CNF/ModelCount.lean would absorb all five; it touches a widely imported module, so it is better as its own small PR.
• The repeated-proof pair raw_variable_cell_kind / raw_variable_cell_membership (same four-way split, different conclusions) is pre-existing; the variable-level case lemma the body proposes is the right fix.