refactor(PEPS): use pi congruence for boundary casts

[LionSR]

Motivation

• regionBoundaryConfigCastEquiv, the cast equivalence for boundary configurations of a reindexed PEPS tensor, was constructed by hand using Fin.cast on each boundary leg with explicit left_inv and right_inv proofs, duplicating Mathlib machinery.
• Mathlib's Equiv.piCongrRight provides this equivalence directly, composing finCongr (congr_fun h f.1) per open edge and delegating bijectivity to Mathlib.

Description

• TNLean/PEPS/RegionBlock/ReindexInjectivity.lean (+2/−11): replace the manual structure literal for regionBoundaryConfigCastEquiv with Equiv.piCongrRight. Remove the hand-written Fin.cast inverse and its two proof obligations (left_inv, right_inv).
• The public name and type of regionBoundaryConfigCastEquiv are unchanged; regionBlockedTensorInjective_reindexTensor, which precomposes the blocked family with this map and applies linearIndependent_equiv, is unaffected.

Testing

• lake env lean TNLean/PEPS/RegionBlock/ReindexInjectivity.lean
• lake build TNLean.PEPS.RegionBlock.ReindexInjectivity -q --log-level=info
• rg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/PEPS/RegionBlock/ReindexInjectivity.lean (no matches)
• lake build TNLean -q --log-level=info (only pre-existing warnings)
• Relies on Lean CI (lean_action_ci.yml) to validate build.

---

Note

Low Risk
Proof-only refactor in one Lean file; no changes to theorem statements or downstream call sites beyond the equivalent definition.

Overview
regionBoundaryConfigCastEquiv is no longer built by hand with Fin.cast on each boundary leg and custom left_inv / right_inv proofs. It is now Equiv.piCongrRight composed with finCongr (congr_fun h f.1) per open edge, delegating bijectivity to Mathlib.

The public name and type of the equivalence are unchanged, so regionBlockedTensorInjective_reindexTensor still precomposes the blocked family with this map and applies linearIndependent_equiv—behavior is the same, with less boilerplate.

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

[claude]

Blueprint/prose review — categories A and B only.

Category A (blueprint ↔ Lean equivalence and status): No issues. Neither regionBoundaryConfigCastEquiv nor regionBlockedTensorInjective_reindexTensor has a blueprint entry, and no .tex files were changed in this PR. There are no \lean{...} tags, \leanok annotations, or \notready tags to check.

Category B (prose quality, no Lean jargon, formula-driven sketches): No issues. The diff consists entirely of Lean proof terms; no docstrings, comments, or section names were added or modified.

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

[claude]

PR cleanup

Field	Before	After
Title	refactor(PEPS): use pi congruence for boundary casts	unchanged (already compliant)
Body	## Summary / ## Validation non-standard headings	restructured to ### Motivation / ### Description / ### Testing; Cursor Bugbot block preserved verbatim
Labels	(none)	added: cleanup
Issue	no linked issue found (branch has no issue-N segment; body has no Addresses/Closes/Fixes reference; commits have no #N; no open issue matches the changed file TNLean/PEPS/RegionBlock/ReindexInjectivity.lean)

No issue footer was added to the body because no linked issue could be identified. Please link the relevant issue manually by adding Addresses #N (or Closes #N) to the body footer, or open a new issue if none exists.

Conventions: CONTRIBUTING.md

[claude]

Review: refactor(PEPS): use pi congruence for boundary casts

Verdict: Approve. No 🔴 or 🟡 issues found. This is a clean, behavior-preserving simplification.

What changed

regionBoundaryConfigCastEquiv (TNLean/PEPS/RegionBlock/ReindexInjectivity.lean:31) is no longer built as a hand-written Equiv structure literal with per-leg Fin.cast and manual left_inv/right_inv proofs. It is now Equiv.piCongrRight fun f => finCongr (congr_fun h f.1), delegating bijectivity to Mathlib.

Correctness verification (🔴)

The new definition is definitionally equal to the old one, so the refactor cannot change behavior:

• Old toFun bdry = fun f => Fin.cast (congr_fun h f.1) (bdry f); old invFun uses (congr_fun h f.1).symm.
• finCongr (h : a = b) is the equivalence with toFun = Fin.cast h and invFun = Fin.cast h.symm; Equiv.piCongrRight F acts pointwise as fun g a => F a (g a).
• Hence the new toFun/invFun reduce to exactly the old maps.

This is load-bearing for the only consumer, regionBlockedTensorInjective_reindexTensor (:45): its hfam step (funext bdry τ; exact regionBlockedWeight_reindexTensor …) needs regionBlockedTensorFamily T R ∘ regionBoundaryConfigCastEquiv T h R to reduce to the Fin.cast-based reindex that regionBlockedWeight_reindexTensor is stated for. Because the new equiv's toFun is the same Fin.cast map definitionally, that proof and the final linearIndependent_equiv … |>.mpr hT step are unaffected.

Other categories

• Proof integrity (🔴): no sorry/axiom/admit/native_decide introduced — the diff removes proof obligations rather than adding any.
• Mathlib style / duplication (🟡): net improvement; replaces hand-rolled Fin.eq_of_val_eq + funext boilerplate with the canonical Equiv.piCongrRight + finCongr combinator.
• Type safety (🔴): types align — congr_fun h f.1 : bd f.1 = T.bondDim f.1, so finCongr (congr_fun h f.1) : Fin (bd f.1) ≃ Fin (T.bondDim f.1), and piCongrRight yields the declared RegionBoundaryConfig (reindexTensor T h) R ≃ RegionBoundaryConfig T R.
• Documentation (🟡): docstring on the definition is retained; mathematical meaning unchanged.

ℹ️ Advisory (non-blocking)

regionBoundaryConfigCastEquiv remains marked noncomputable, but Equiv.piCongrRight and finCongr are computable, so the keyword is now (and likely was already) unnecessary. Harmless; out of scope for this minimal diff. Optionally drop it in a follow-up.

[claude]

Review summary

This is a clean, minimal refactor in one file (TNLean/PEPS/RegionBlock/ReindexInjectivity.lean) that replaces a hand-written Equiv structure literal (11 lines) with a 2-line construction using Mathlib's Equiv.piCongrRight and finCongr. No theorem statements change; the public interface is identical.

Findings by category

🔴 Proof integrity — ✅ No issues. Build succeeds (lake build completes, 1834 jobs). No sorry, admit, axiom, native_decide, or unsafeCast in the changed file or its import chain.

🔴 Proof correctness — ✅ The new definition

Equiv.piCongrRight fun f => finCongr (congr_fun h f.1)

is mathematically equivalent to the old hand-written structure literal. finCongr (Mathlib Data/Fin/SuccPred.lean:138) wraps Fin.cast in an Equiv with the same toFun/invFun/inverse proofs. Equiv.piCongrRight lifts the family of Fin (bd f.1) ≃ Fin (T.bondDim f.1) equivalences to RegionBoundaryConfig types via Pi.map. The downstream theorem regionBlockedTensorInjective_reindexTensor is unchanged and linearIndependent_equiv transport is preserved.

🟡 Mathlib style — ✅ No issues. regionBoundaryConfigCastEquiv uses camelCase. regionBlockedTensorInjective_reindexTensor uses snake_case. Line length under 100 chars. finCongr is the standard Mathlib name (replacing the legacy n notation). Equiv.piCongrRight is accessed with full namespace.

🔴 Type safety — ✅ No type mismatches or universe issues. Build confirms full typechecking.

🟡 Performance — ✅ This simplification removes custom inverse proofs (4 lines of funext/Fin.eq_of_val_eq/simp). The replacement is a direct Mathlib call; no performance regression.

🟡 Modularity & duplication — ✅ Improvement: replaces 11 lines of project-local boilerplate with Mathlib combinators, reducing duplication and maintenance burden.

🟡 Documentation — ✅ Module-level docstring and definition-level docstrings are present and include arXiv source references.

🟡 Paper-gap notes — ✅ No changes to docs/paper-gaps/.

Previous feedback

• One prior review from @claude (approved, blueprint/prose categories only) — no unresolved issues.
• No inline review threads. No PR conversation comments.

Verdict

APPROVE — zero 🔴 or 🟡 issues.