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

[LionSR]

Motivation

• tiBoundaryConfigEquiv was defined with hand-written invFun and left_inv / right_inv proofs. These are derivable from Mathlib's Equiv.piCongrRight via the fibrewise finCongr arising from translation-invariant bond dimensions, removing the need for explicit inverse proofs.

Description

• Modified TNLean/PEPS/TorusGaugedWeightCovariance.lean: rewrites tiBoundaryConfigEquiv as the composition of regionBoundaryConfigMapEquiv with Equiv.piCongrRight over finCongr.
• The forward map tiBoundaryConfigMap and the simp lemma tiBoundaryConfigEquiv_apply (which holds by rfl) are unchanged; call sites (surjectivity, Equiv.sum_comp, etc.) are unaffected.
• Eliminates 20 lines of hand-written inverse and inverse-law proofs.

Testing

• lake env lean TNLean/PEPS/TorusGaugedWeightCovariance.lean
• lake build TNLean.PEPS.TorusGaugedWeightCovariance -q --log-level=info
• rg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/PEPS/TorusGaugedWeightCovariance.lean || true
• lake build TNLean -q --log-level=info
• Pre-existing style/header warnings and the known periodic-overlap sorry in TNLean/MPS/Periodic/Overlap/Case3.lean are unrelated to this change.

---

Note

Low Risk
Proof-only refactor in PEPS torus covariance; no API or runtime behavior change beyond Mathlib-derived inverse laws.

Overview
tiBoundaryConfigEquiv is no longer built with hand-written invFun and left_inv / right_inv proofs. It is now regionBoundaryConfigMapEquiv composed with Equiv.piCongrRight and fibrewise finCongr from translation-invariant bond dimensions.

The forward map is still tiBoundaryConfigMap; tiBoundaryConfigEquiv_apply remains rfl, so callers (surjectivity, Equiv.sum_comp, etc.) are unchanged.

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

[claude]

Blueprint ↔ Lean equivalence and status (Category A)

No blueprint .tex files are modified in this PR. tiBoundaryConfigEquiv has no blueprint entry (/blueprint/src/ contains no reference to this declaration or the surrounding PEPS torus module), so there are no \lean{...}, \leanok, or \notready tags to verify. No declarations are added or removed, and the type signature of tiBoundaryConfigEquiv is unchanged — only the proof body is replaced.

0 equivalence mismatches. 0 stale \leanok. 0 missing tags.

Prose quality (Category B)

The diff introduces no docstrings, inline comments, section names, or namespace names. The pre-existing docstring /-- The transported boundary configuration as a bijection. -/ is untouched and not in scope for this review.

0 prose issues.

---

No issues in either category.

[claude]

PR cleanup

Field	Before	After
Title	refactor(PEPS): use pi congruence for torus boundary casts	unchanged (already compliant)
Body	## Summary / ## Validation headings	restructured to ### Motivation / ### Description / ### Testing template; Cursor Bugbot block preserved verbatim
Labels	(none)	added: cleanup, 1804.04964
Issue	no linked issue found

Issue search notes: The branch name (codex/torus-boundary-config-pi-congr) contains no issue-N pattern, the PR body has no #N references, the commit message has no issue reference, and a search of open and recent closed issues found no match for tiBoundaryConfigEquiv, TorusGaugedWeightCovariance, or piCongrRight. If a tracking issue exists for PEPS torus covariance work, please link it manually with Addresses #N in the PR body.

Conventions: CONTRIBUTING.md

[claude]

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

Verdict: Approve. This is a clean, correctness-preserving proof-only refactor. No 🔴 or 🟡 issues found.

What I verified

The change replaces the hand-written invFun/left_inv/right_inv of tiBoundaryConfigEquiv with the composition

(regionBoundaryConfigMapEquiv T (translate a b) R).trans
  (Equiv.piCongrRight fun f => finCongr (congrFun (congrArg Tensor.bondDim (hT a b)) f.1))

The load-bearing claim is that tiBoundaryConfigEquiv_apply still holds by rfl, i.e. the new forward map is definitionally tiBoundaryConfigMap. I confirmed this from the definitions:

• finCongr eq is defined with toFun := Fin.cast eq (Mathlib/Data/Fin/SuccPred.lean:138), so finCongr h x is defeq to Fin.cast h x — matching the cast used in tiBoundaryConfigMap (TorusGaugedWeightCovariance.lean:81).
• regionBoundaryConfigMapEquiv A φ R's forward map is regionBoundaryConfigMap A φ R by rfl (RegionTransport.lean:141-144).
• Equiv.trans composes second-after-first and Equiv.piCongrRight (fun f ↦ e_f) g = fun f ↦ e_f (g f).

Unfolding the composition on bdry yields exactly
fun f => Fin.cast (congrFun (congrArg Tensor.bondDim (hT a b)) f.1) (regionBoundaryConfigMap T (translate a b) R bdry f),
which is the body of tiBoundaryConfigMap. The index set is unchanged (both regions live on torusGraph width height; translate a b is a graph automorphism), and the per-fiber Fin (bondDim …) mismatch from hT a b : T.transport (translate a b) = T is handled by the fibrewise finCongr exactly as the deleted hand-written code did.

Checks

• Proof integrity (🔴): No sorry/axiom/native_decide/admit introduced; the change removes hand-written proof terms in favor of Mathlib equivalences.
• Proof correctness (🔴): Equivalence laws (apply_symm_apply etc.) used at call sites (tiBoundaryConfigMap_surjective, Equiv.sum_comp) are generic Equiv methods, independent of construction; unaffected.
• Type safety (🔴): Fiber and index types align as above.
• Style / documentation / modularity (🟡): Docstring on tiBoundaryConfigEquiv retained; lines within 100 chars; reuses Mathlib Equiv.piCongrRight/finCongr rather than re-deriving inverse laws — a net modularity improvement.

Note: I was unable to run a full lake build (TNLean oleans are not cached in this review environment), so I relied on the definitional verification above plus the author's reported lake env lean / lake build runs. The rfl simp lemma being preserved is the key invariant and it holds.

[claude]

Review Summary

Verdict: APPROVE

This is a clean, well-scoped refactoring that replaces a hand-written Equiv (with explicit invFun, left_inv, right_inv) with a composition of regionBoundaryConfigMapEquiv, Equiv.piCongrRight, and finCongr — all standard Mathlib constructions. The change eliminates 20 lines of manual proofs while maintaining definitional equality of the forward map (verified by tiBoundaryConfigEquiv_apply remaining rfl).

Category-by-category assessment

Category	Severity	Status
🔴 Proof integrity	Blocker	✅ No sorry, axiom, admit, native_decide, or unsafeCast introduced
🔴 Proof correctness	Blocker	✅ New definition is mathematically equivalent; tiBoundaryConfigEquiv_apply holds by rfl (verified by full lake build); all downstream theorems unchanged
🟡 Mathlib style	Required	✅ Uses idiomatic Equiv.trans, Equiv.piCongrRight; cleaner than the hand-written version
🔴 Type safety	Blocker	✅ Types are compatible: regionBoundaryConfigMapEquiv transports across the graph isomorphism, finCongr adjusts bond dimensions back via hT
🟡 Performance	Required	✅ No performance concerns; simpler proof terms
🟡 Modularity	Required	✅ Removes duplication by leveraging existing Mathlib and PEPS lemmas
🟡 Documentation	Required	✅ Existing docstring preserved
🟡 Paper-gap notes	Required	✅ N/A — no paper-gap notes changed

Mathematical verification

The composition is correct:

1. regionBoundaryConfigMapEquiv T (translate a b) R maps RegionBoundaryConfig T R → RegionBoundaryConfig (T.transport (translate a b)) (Region.map (translate a b) R), handling the geometric reindexing of boundary edges.

2. Equiv.piCongrRight with finCongr (congrFun (congrArg Tensor.bondDim (hT a b)) f.1) adjusts each fiber from Fin (T.bondDim (Edge.map (translate a b).symm f.1)) (definitionally from the transported tensor's bond dim) to Fin (T.bondDim f.1) using the translation-invariance hypothesis hT : IsTorusTranslationInvariant T.

3. The forward map is definitionally Fin.cast with the same proof as tiBoundaryConfigMap, so tiBoundaryConfigEquiv_apply remains rfl.

No concerns.