refactor(PEPS): use subtype product equivalence for incidence swap

[LionSR]

Motivation

• sigmaSwap in PEPS/EdgeScalarSolve.lean was defined by explicit toFun / invFun fields with manual inverse proofs. Replacing this construction with Mathlib's Equiv.subtypeProdEquivSigmaSubtype, composed with Equiv.prodComm via Equiv.subtypeEquiv, reduces bespoke proof obligations and aligns the construction with the library (arXiv:1804.04964, Section 3).

Description

• TNLean/PEPS/EdgeScalarSolve.lean (6 additions, 5 deletions): sigmaSwap is now built as a chain of Mathlib equivalences — (Equiv.subtypeProdEquivSigmaSubtype).symm, Equiv.prodComm transported through subtypes via Equiv.subtypeEquiv, and Equiv.subtypeProdEquivSigmaSubtype — replacing the previous explicit toFun/invFun definition with manual inverse lemmas.
• The equivalence still reindexes pairs from (Σ v : V, IncidentEdge v) to (Σ e : Edge G, IncVertex e).
• The downstream lemma prod_orientedIncidence_eq_one (which applies Equiv.prod_comp (sigmaSwap).symm) is unchanged; the refactor is definitionally compatible.
• No mathematical content is altered.

Testing

• lake env lean TNLean/PEPS/EdgeScalarSolve.lean
• lake build TNLean.PEPS.EdgeScalarSolve -q --log-level=info
• rg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/PEPS/EdgeScalarSolve.lean || true
• Full build (lake build TNLean -q --log-level=info): passes with only pre-existing warnings (including the known sorry in MPS/Periodic/Overlap/Case3.lean).
• Relies on Lean CI (lean_action_ci.yml) to validate the build.

---

Note

Low Risk
Proof-only refactor in one combinatorial lemma; behavior is intended to stay definitionally compatible for the existing product-cancellation proof.

Overview
sigmaSwap in EdgeScalarSolve.lean is no longer defined by explicit toFun / invFun and rfl inverse lemmas. It is built as a chain of Mathlib equivalences: Equiv.subtypeProdEquivSigmaSubtype (sym), Equiv.prodComm on V × Edge G via subtypeEquiv, and another subtypeProdEquivSigmaSubtype.

The equivalence still reindexes (Σ v, IncidentEdge) to (Σ e, incVertex e); prod_orientedIncidence_eq_one is unchanged and still uses Equiv.prod_comp (sigmaSwap).symm.

^{Reviewed by Cursor Bugbot for commit 82754cf. Bugbot is set up for automated code reviews on this repo. Configure here.}

[claude]

Blueprint ↔ Lean & Prose Review

Category A — Blueprint ↔ Lean equivalence and status: no issues.

sigmaSwap has no blueprint entry (the PEPS/ module is exploratory and carries no \lean{...} tags). No .tex files were changed, no \leanok/\notready tags are affected, and no declaration with a blueprint counterpart was modified.

Category B — Prose quality: no issues.

The only reader-facing text in scope is the unchanged docstring for sigmaSwap (lines 66–67). It contains no Lean jargon, no banned software-engineering terms, and no LLM writing patterns.

---

Summary: 0 equivalence mismatches, 0 stale status tags, 0 prose issues.

[claude]

PR cleanup

Field	Before	After
Title	refactor(PEPS): use subtype product equivalence for incidence swap	unchanged
Body	## Summary / ## Validation sections (non-standard)	restructured to ### Motivation / ### Description / ### Testing template; Cursor Bugbot note preserved verbatim
Labels	(none)	added: cleanup, 1804.04964
Issue	no linked issue found

No issue number was found in the branch name (codex/peps-disjoint-sigma-subtype-equivalence), commit message, or PR body after exhaustive search. Please link a relevant issue manually by adding Addresses #N (or Closes #N) to the PR body.

Conventions: CONTRIBUTING.md

[claude]

Review: refactor(PEPS): use subtype product equivalence for incidence swap

Verdict: Approve. No 🔴 or 🟡 issues found. One ℹ️ advisory below.

Scope

The PR rewrites the single definition sigmaSwap in TNLean/PEPS/EdgeScalarSolve.lean:68-74, replacing the explicit toFun/invFun/left_inv/right_inv record (with rfl inverse proofs) by a composition of three Mathlib equivalences. No other declaration changes.

Proof integrity 🔴 — pass

No sorry/axiom/admit/native_decide/unsafeCast introduced (the only project sorry remains the unrelated, known MPS/Periodic/Overlap/Case3.lean). This is a proof-only refactor of an Equiv definition.

Correctness 🔴 — pass (verified)

The new sigmaSwap is mathematically identical to the original. Tracing the forward map of
((Equiv.subtypeProdEquivSigmaSubtype p).symm.trans ((Equiv.prodComm V (Edge G)).subtypeEquiv …)).trans (Equiv.subtypeProdEquivSigmaSubtype q):

• subtypeProdEquivSigmaSubtype p |>.symm : ⟨v, ⟨e, h⟩⟩ ↦ ⟨(v, e), h⟩
• (prodComm V (Edge G)).subtypeEquiv (fun _ => Iff.rfl) : ⟨(v, e), h⟩ ↦ ⟨(e, v), h⟩ — the predicate is preserved by Iff.rfl because both p (v, e) and q (e, v) are literally e.1.1 = v ∨ e.1.2 = v
• subtypeProdEquivSigmaSubtype q : ⟨(e, v), h⟩ ↦ ⟨e, ⟨v, h⟩⟩

Composite: ⟨v, ⟨e, h⟩⟩ ↦ ⟨e, ⟨v, h⟩⟩, identical to the deleted toFun p := ⟨p.2.1, ⟨p.1, p.2.2⟩⟩. The downstream consumer prod_orientedIncidence_eq_one (lines 96-112) closes the inner Finset.prod_congr … rfl (line 109) by definitional unfolding of (sigmaSwap).symm ⟨e, x⟩ to ⟨x.1, ⟨e, x.2⟩⟩. I confirmed this still holds by building the module locally:

lake build TNLean.PEPS.EdgeScalarSolve  →  Build completed successfully

The only warnings emitted are pre-existing and on unrelated lines (v0Inc_subsingleton unused-section-var at 226-228, header copyright linter); none touch the changed definition.

Type safety 🔴 — pass

Both predicate arguments are spelled out explicitly (fun (v : V) (e : Edge G) => … and fun (e : Edge G) (v : V) => …), so the two subtypeProdEquivSigmaSubtype instantiations and the subtypeEquiv transport unify without relying on elaboration order. Build confirms.

Style / performance / docs 🟡 — pass

Naming (sigmaSwap, camelCase def) and the docstring are preserved; noncomputable is retained as before. No performance concern (term-mode definition).

ℹ️ Advisory (non-blocking)

The original explicit form was already a one-glance-verifiable Equiv with rfl inverse laws. The composed version is more "library-idiomatic" but requires the reader to unfold subtypeProdEquivSigmaSubtype, the subtypeEquiv transport, and prodComm to re-derive the map. This is a readability/transparency tradeoff, not a defect — either form is acceptable. No action required.

Note: PR is currently in draft state.

[claude]

Review Summary: ✅ APPROVE

This PR refactors sigmaSwap in TNLean/PEPS/EdgeScalarSolve.lean, replacing a manually-defined equivalence with a composition of standard Mathlib equivalences (Equiv.subtypeProdEquivSigmaSubtype + Equiv.prodComm.subtypeEquiv). The mathematical content is unchanged.

Detailed analysis

🔴 Proof integrity: Pass. No sorry, axiom, admit, native_decide, or unsafeCast in the changed file. The build succeeds with only pre-existing warnings unrelated to this change.

🔴 Proof correctness: Pass. The chain of equivalences is mathematically correct:

• Equiv.subtypeProdEquivSigmaSubtype.symm converts (Σ v, IncidentEdge G v) to {p : V × Edge G // …}
• (Equiv.prodComm …).subtypeEquiv (fun _ => Iff.rfl) swaps the pair to Edge G × V
• Equiv.subtypeProdEquivSigmaSubtype converts to the target (Σ e, incVertex e)

The downstream proof prod_orientedIncidence_eq_one (line 109) uses rfl to equate the reindexed edgeScalarUnit term with (if e.1.1 = x.1 then s e else (s e)⁻¹). This rfl holds definitionally because:

• Equiv.subtypeProdEquivSigmaSubtype.invFun is structurally transparent (explicit ⟨⟨x.1, x.2⟩, x.2.property⟩)
• subtypeEquiv with (fun _ => Iff.rfl) gives definitionally transparent invFun — the ▸ term collapses at rfl (since prodComm.apply_symm_apply is rfl)
• Equiv.trans uses ∘ for invFun, which reduces compositionally
• The resulting (sigmaSwap.symm ⟨e, x⟩).1 and .2 reduce to exactly x.1 and ⟨e, x.2⟩, matching the old explicit definition

The edgeScalarUnit function only inspects .1.1.1 and .1 of the IncidentEdge argument, which are independent of the proof term in .2, so the rfl is robust.

🟡 Mathlib style: Pass. The definition uses standard Mathlib equivalence combinators (subtypeProdEquivSigmaSubtype, prodComm, subtypeEquiv) rather than a custom manual construction. Line length, naming, and formatting follow conventions. The Iff.rfl pattern is correct and idiomatic when predicates are definitionally equal under the equivalence (as they are here, due to the symmetric form e.1.1 = v ∨ e.1.2 = v).

🔴 Type safety: Pass. No universe issues, missing instances, or coercion problems. The noncomputable attribute is preserved.

🟡 Performance: Pass. The rfl proofs are fast. No decide, simp with unbounded lemma sets, or deep rw chains.

🟡 Modularity & duplication: Pass. This is an improvement — using standard library components instead of a bespoke equivalence definition.

🟡 Documentation: Pass. The existing docstring is preserved and accurately describes the equivalence.

🟡 Paper-gap notes: N/A — no changes to docs/paper-gaps/.