refactor(MPS): use finRotate for periodic config rotation

[LionSR]

Motivation

• The hand-written rotateCfg equivalence in TNLean/MPS/Periodic/Overlap/Case3Transport.lean
  used custom Fin.cons/Fin.snoc with explicit left_inv/right_inv proofs.
  Replacing it with Mathlib's Equiv.arrowCongr (finRotate …) reduces bespoke code while
  preserving the mathematical content (one-site cyclic rotation of physical configurations,
  arXiv:1708.00029, Appendix A).

Description

• Modified TNLean/MPS/Periodic/Overlap/Case3Transport.lean:
  • rotateCfg is now defined as Equiv.arrowCongr (finRotate (L' + 1)) (Equiv.refl (Fin d)).
  • evalWord_ofFn_rotateCfg is adapted: it first establishes
    rotateCfg σ = Fin.cons (σ (Fin.last L')) (Fin.init σ) via finRotate_symm_apply,
    then applies the existing List.ofFn_cons / evalWord_cons steps.
  • Public lemmas consuming rotateCfg (trace covariance and overlap shift) are unchanged.
  • No new sorry or proof-integrity workaround introduced.

Testing

• lake env lean TNLean/MPS/Periodic/Overlap/Case3Transport.lean
• lake build TNLean.MPS.Periodic.Overlap.Case3Transport -q --log-level=info
• rg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/MPS/Periodic/Overlap/Case3Transport.lean || true
• lake build TNLean -q --log-level=info

---

No issue found. If this refactor addresses an open issue, please link it manually with Addresses #N.

Note

Low Risk
Local proof refactor in Case 3 transport with no API or mathematical claim changes beyond the new definition of rotateCfg.

Overview
rotateCfg is no longer built by hand with Fin.cons / Fin.snoc and explicit left_inv / right_inv proofs. It is now Equiv.arrowCongr (finRotate (L' + 1)) (Equiv.refl (Fin d)), aligning periodic "last letter to front" rotation with Mathlib's cyclic index map.

evalWord_ofFn_rotateCfg no longer unfolds the old equivalence directly. It first proves rotateCfg σ = Fin.cons (σ (Fin.last L')) (Fin.init σ) using finRotate_symm_apply and related Fin lemmas, then reuses the same List.ofFn_cons / evalWord_cons step as before.

No change to the public lemmas that consume rotateCfg (trace covariance and overlap shift); behavior is intended to be definitionally the same with less custom equivalence code.

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

[claude]

Blueprint ↔ Lean equivalence and prose review

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

Neither rotateCfg nor the private evalWord_ofFn_rotateCfg has a blueprint entry. No .tex files are changed in this PR and no \lean{...} tags are added, removed, or renamed. No \leanok or \notready accuracy to check.

Category B — Prose quality: no issues.

The diff touches only Lean proof and definition bodies. The two affected docstrings (rotateCfg and evalWord_ofFn_rotateCfg) are unchanged context lines; both are already clean of banned terms, Lean-jargon leakage, and LLM writing patterns.

---

0 equivalence mismatches · 0 stale status tags · 0 prose issues

[claude]

PR cleanup

Field	Before	After
Title	refactor(MPS): use finRotate for periodic config rotation	unchanged (already compliant)
Body	## Summary / ## Validation headings (non-standard)	restructured to ### Motivation / ### Description / ### Testing template; Cursor Bugbot block preserved
Labels	(none)	added: cleanup, 1708.00029
Issue	no issue found in branch name, commits, or body	no issue linked; please add Addresses #N manually if applicable

Conventions: CONTRIBUTING.md

[claude]

Review: refactor(MPS): use finRotate for periodic config rotation

Verdict: Approve. Correct, low-risk refactor. No 🔴 or 🟡 issues found.

Proof integrity (🔴) — clean

No sorry, axiom, admit, native_decide, or unsafeCast introduced.

Proof correctness (🔴) — verified

The refactor replaces the hand-written rotateCfg equiv (explicit toFun/invFun/left_inv/right_inv) with Equiv.arrowCongr (finRotate (L' + 1)) (Equiv.refl (Fin d)), and re-derives the old toFun form as a lemma. I checked this against Mathlib:

• Equiv.arrowCongr e₁ e₂ has toFun f = e₂ ∘ f ∘ e₁.symm (Mathlib/Logic/Equiv/Defs.lean:455). With e₂ = Equiv.refl, rotateCfg σ j = σ ((finRotate (L' + 1)).symm j).
• finRotate_symm_apply gives (finRotate _).symm i = i - 1 cyclically (Mathlib/Logic/Equiv/Fin/Rotate.lean:106).
• Hence at j = 0: (finRotate (L'+1)).symm 0 = 0 - 1 = L' = Fin.last L', matching the Fin.cons head. At j = i.succ: i.succ - 1 = i.castSucc, matching Fin.init σ i = σ i.castSucc.

So evalWord_ofFn_rotateCfg's helper hrotate : rotateCfg σ = Fin.cons (σ (Fin.last L')) (Fin.init σ) is exactly the old toFun, and the proof of trace_proj_evalWord_rotateCfg/sum_trace_proj_overlap_shift is unaffected (they only need an Equiv for Equiv.sum_comp plus evalWord_ofFn_rotateCfg). The change/Fin.ext/congrArg σ chain is well-structured; by simp discharges the index goals because finRotate_symm_apply is a @[simp] lemma, and the i.succ ≠ 0 side-goal for Fin.val_sub_one_of_ne_zero is supplied. The mathematical content matches the cited source (arXiv:1708.00029, Appendix A, lines 985–1002) and is unchanged by this PR.

Type safety (🔴), style (🟡), performance (🟡), modularity (🟡), docs (🟡)

No issues. Using the canonical finRotate/arrowCongr is the more idiomatic Mathlib formulation and reduces custom equivalence code. Docstrings are unchanged and accurate.

ℹ️ Advisory (non-blocking)

At lines 49–50 the two consecutive single-lemma rewrites

rw [finRotate_symm_apply]
rw [Fin.val_sub_one_of_ne_zero (by simp)]

could be merged into one rw [finRotate_symm_apply, Fin.val_sub_one_of_ne_zero (by simp)], the more common Mathlib idiom. Purely cosmetic.

(Blueprint/prose review handled by the dedicated workflow; out of scope here.)

[claude]

Code Review: PR #3134

All 8 review categories pass with no blocking issues.

Summary

This PR replaces the hand-written rotateCfg equivalence with Equiv.arrowCongr (finRotate (L'+1)) (Equiv.refl (Fin d)), aligning the periodic configuration rotation with Mathlib's cyclic index map. The private lemma evalWord_ofFn_rotateCfg is updated to prove the identity between the new Mathlib-based definition and the old Fin.cons form via a local hrotate equality, then reuses the existing List.ofFn_cons / evalWord_cons proof path.

Category results

Category	Result
🔴 Proof integrity	No blockers. No sorry, axiom, native_decide, unsafeCast, or circular reasoning.
🔴 Proof correctness	The new definition σ ∘ (finRotate (L'+1)).symm is mathematically equivalent to Fin.cons (σ (Fin.last L')) (Fin.init σ). The hrotate proof correctly establishes this using finRotate_symm_apply and Fin.val_sub_one_of_ne_zero. Consumer lemmas are unchanged.
🟡 Mathlib style	Naming follows conventions. Uses Mathlib API (finRotate, Equiv.arrowCongr) instead of custom equivalence logic — good modularity.
🔴 Type safety	No issues. Equiv.arrowCongr is applied with matching index types.
🟡 Performance	Lightweight proof — no timeout risk.
🟡 Modularity	Good reuse of Mathlib. No duplication.
🟡 Documentation	Existing docstrings unchanged and adequate.
🟡 Paper-gap notes	N/A.

Verdict: APPROVE