refactor(PEPS): use native equivalences for double-complement configs

[LionSR]

Motivation

• The hand-written Equiv records for the double-complement boundary and physical configuration transports duplicate structure already present in Mathlib, creating unnecessary proof obligations.
• Replacing them with the Mathlib combinators Equiv.piCongrLeft' and Equiv.arrowCongr reduces custom reasoning and makes the constructions more legible.

Description

• TNLean/PEPS/RegionBlock/Recovery10.lean: regionDoubleComplBoundaryConfigEquiv is now constructed via Equiv.piCongrLeft' applied to regionBoundaryEdgeDoubleComplEquiv (replacing a hand-built Equiv record).
• TNLean/PEPS/RegionBlock/BlockCoeffTransfer.lean: regionDoubleComplPhysicalConfigEquiv is now constructed via Equiv.arrowCongr applied to regionDoubleComplVertexEquiv (replacing a hand-built Equiv record).
• The transported values remain definitionally compatible with the existing blocked-tensor and injectivity proofs; no downstream theorem statements change.

Testing

• lake env lean TNLean/PEPS/RegionBlock/Recovery10.lean
• lake env lean TNLean/PEPS/RegionBlock/BlockCoeffTransfer.lean
• lake build TNLean.PEPS.RegionBlock.Recovery10 TNLean.PEPS.RegionBlock.BlockCoeffTransfer -q --log-level=info
• rg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/PEPS/RegionBlock/Recovery10.lean TNLean/PEPS/RegionBlock/BlockCoeffTransfer.lean || true — no new proof obligations introduced.
• Full build (lake build TNLean) reports only pre-existing warnings outside the changed files, including the known sorry in TNLean/MPS/Periodic/Overlap/Case3.lean.

---

Note

Low Risk
Proof-only refactor with no API or theorem signature changes; behavior is intended to stay definitionally aligned with the previous manual equivalences.

Overview
Replaces hand-built Equiv records for double-complement physical and boundary configuration transport with Mathlib combinators: Equiv.arrowCongr on regionDoubleComplVertexEquiv and Equiv.piCongrLeft' on regionBoundaryEdgeDoubleComplEquiv.

The change is localized to regionDoubleComplPhysicalConfigEquiv in BlockCoeffTransfer.lean and regionDoubleComplBoundaryConfigEquiv in Recovery10.lean; downstream proofs still call the same transport functions and equivalence names, so blocked-tensor and injectivity statements are unchanged.

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

[claude]

PR cleanup

Field	Before	After
Title	refactor(PEPS): use native equivalences for double-complement configs	unchanged — already compliant
Body	## Summary / ## Validation (non-standard headings)	restructured to ### Motivation / ### Description / ### Testing template; Cursor Bugbot block preserved verbatim
Labels	(none)	added: cleanup
Issue	no linked issue found	no Addresses footer added — author should link an issue manually if one exists

Issue search: Checked branch name, PR body, PR title, commit messages, and open issues mentioning Recovery10, BlockCoeffTransfer, regionDoubleCompl, arrowCongr, piCongrLeft — no match found. If this PR addresses an open issue, please add Addresses #N to the body footer.

Conventions: CONTRIBUTING.md

[claude]

Blueprint ↔ Lean equivalence and prose review

Category A — Blueprint ↔ Lean equivalence and status

regionDoubleComplBoundaryConfigEquiv (Recovery10.lean) is referenced in blueprint/src/chapter/ch24_peps_ft_region_transfer_maps.tex:219 inside the \lean{...} list for thm:peps_region_transfer_coeff_double_factorization, which carries \leanok. The PR changes only the proof body (explicit where/funext/simp block → Equiv.piCongrLeft' _ (...).symm); the declaration name and type signature are unchanged and the new term contains no sorry. Blueprint sync remains valid.

regionDoubleComplPhysicalConfigEquiv (BlockCoeffTransfer.lean) has no direct blueprint entry — ch24_peps_ft_region_transfer_insertions.tex:484 references only regionDoubleComplPhysicalConfig (the underlying function, not the equivalence). This gap is pre-existing and not introduced by this PR.

No \leanok becomes invalid, no \notready becomes stale, and no \lean{...} tag requires renaming.

Category B — Prose quality

No prose is changed. The only new lines are Lean proof terms (Equiv.arrowCongr and Equiv.piCongrLeft'); no docstrings, module comments, or .tex files are touched.

---

Summary: 0 equivalence mismatches, 0 stale \leanok, 0 prose issues.

[claude]

Review: refactor(PEPS): use native equivalences for double-complement configs

Verdict: APPROVE — no 🔴 or 🟡 issues found.

This is a clean, minimal proof-only refactor that replaces two hand-written Equiv records with Mathlib combinators, exactly the kind of library reuse the contributing guidelines encourage. I verified correctness both by definitional analysis and by a full local build.

Proof integrity 🔴 — clean

No sorry/axiom/admit/native_decide/unsafeCast introduced (rg over both files returns nothing new). Declaration names and type signatures of regionDoubleComplPhysicalConfigEquiv (BlockCoeffTransfer.lean) and regionDoubleComplBoundaryConfigEquiv (Recovery10.lean) are unchanged.

Proof correctness 🔴 — verified

The load-bearing question for this refactor is whether each new combinator's toFun is definitionally equal to the previous explicit toFun, since downstream proofs (regionBlockedTensorInjective_doubleCompl's change, and regionBlockedTensorMap_doubleCompl's Equiv.sum_comp) depend on it.

• regionDoubleComplPhysicalConfigEquiv: old toFun = regionDoubleComplPhysicalConfig R = fun w => σ (regionDoubleComplVertexEquiv R w). New Equiv.arrowCongr (regionDoubleComplVertexEquiv R).symm (Equiv.refl (Fin d)) reduces its toFun σ to fun x => σ ((regionDoubleComplVertexEquiv R).symm.symm x), i.e. fun x => σ (regionDoubleComplVertexEquiv R x) — definitionally identical.
• regionDoubleComplBoundaryConfigEquiv: the boundary config codomain Fin (A.bondDim f.1) is dependent, which is why the old proof needed congr 1. Equiv.piCongrLeft' _ (regionBoundaryEdgeDoubleComplEquiv R).symm type-checks here precisely because regionBoundaryEdgeDoubleComplEquiv_apply_coe (Recovery6) makes the underlying-edge coercion rfl, so the target ∀ b, Fin (bondDim (e.symm b).1) is defeq to ∀ b, Fin (bondDim b.1), and toFun = fun b => bdry (regionBoundaryEdgeDoubleComplEquiv R b) = regionDoubleComplBoundaryConfig A R bdry.

Confirmed empirically: lake build TNLean.PEPS.RegionBlock.BlockCoeffTransfer TNLean.PEPS.RegionBlock.Recovery10 and all downstream modules build at exit 0. The only warnings emitted are the pre-existing Copyright too short! header-linter warnings on the RegionBlock/* files, which are untouched by this diff.

Style / type safety / performance / modularity / documentation 🟡 — clean

Replacing bespoke Equiv records with Equiv.arrowCongr / Equiv.piCongrLeft' improves modularity and removes duplicated left_inv/right_inv boilerplate. No new instances, coercion chains, or universe concerns. Docstrings on both definitions are unchanged and remain accurate. No paper-gap notes touched.

Looks good to merge once moved out of draft.

[claude]

Review: refactor(PEPS): use native equivalences for double-complement configs

Verdict: APPROVE — no 🔴 or 🟡 issues found. Concurring with the earlier claude[bot] reviews.

Proof integrity 🔴 — clean

No sorry/axiom/admit/native_decide/unsafeCast introduced. The only warnings from the build are pre-existing Copyright too short! header-linter warnings on the RegionBlock/* files, untouched by this diff.

Proof correctness 🔴 — verified

Both new combinator definitions are definitionally equivalent to the old hand-written Equiv records:

• regionDoubleComplPhysicalConfigEquiv (BlockCoeffTransfer.lean:148): Equiv.arrowCongr (regionDoubleComplVertexEquiv R).symm (Equiv.refl (Fin d)) reduces toFun f to f ∘ (regionDoubleComplVertexEquiv R), which is definitionally regionDoubleComplPhysicalConfig R. The old toFun matches exactly.

• regionDoubleComplBoundaryConfigEquiv (Recovery10.lean:135): Equiv.piCongrLeft' _ (regionBoundaryEdgeDoubleComplEquiv R).symm handles the dependent codomain Fin (A.bondDim f.1) correctly. The key property is that regionBoundaryEdgeDoubleComplEquiv_apply_coe (Recovery6.lean:92-94) makes the underlying edge coercion definitional, so P (e.symm b) = Fin (A.bondDim b.val) by rfl — no transport needed.

Downstream proofs (regionBlockedTensorInjective_doubleCompl, regionBlockedTensorMap_doubleCompl) depend only on the equivalence type and toFun being definitionally regionDoubleComplPhysicalConfig/regionDoubleComplBoundaryConfig, which is preserved.

Confirmed: lake build TNLean.PEPS.RegionBlock.BlockCoeffTransfer TNLean.PEPS.RegionBlock.Recovery10 exits 0.

Style / type safety / performance / modularity / documentation 🟡 — all clean

• Style: Replacing bespoke Equiv records with Equiv.arrowCongr / Equiv.piCongrLeft' improves library reuse and removes duplicated left_inv/right_inv boilerplate. Declaration names and type signatures are unchanged.
• Type safety: No new instances, coercion chains, or universe concerns. Type inference for the _ argument to piCongrLeft' resolves correctly from the target type annotation.
• Performance: Trivial — these are combinator applications with no recursive or heavy computation.
• Modularity: The underlying transport functions (regionDoubleComplPhysicalConfig in Recovery6, regionDoubleComplBoundaryConfig in Recovery6) remain defined and are still used in 10+ downstream call sites — no dead code created.
• Documentation: Existing docstrings on both definitions are preserved unchanged and remain accurate.

Paper-gap notes 🟡 — N/A

No files under docs/paper-gaps/ are changed.

---

Looks good to merge.