refactor(MPS/Core): use arrow congruence for word reversal

[LionSR]

Motivation

• The hand-built reversal equivalence on words of length L in sum_evalWord_mul_conjTranspose_evalWord (a local revEquiv with explicit inverse proofs) can be replaced by Mathlib's Equiv.arrowCongr applied to Fin.revPerm, matching patterns used elsewhere in the repository (e.g. rotateConfig).
• This reduces reliance on local equivalence machinery and aligns the proof with established Mathlib idioms for permutation-indexed families.

Description

• Modified TNLean/MPS/Core/Blocking.lean: in the proof of sum_evalWord_mul_conjTranspose_evalWord, replaced the local revEquiv definition with Equiv.arrowCongr Fin.revPerm (Equiv.refl (Fin d)).
• The reversed-word step still goes through list_ofFn_comp_fin_rev; the only proof change is unfolding revEquiv, Equiv.arrowCongr, and Function.comp_def in the hword simplification instead of the old local equivalence definition.
• No mathematical content is changed; no new sorrys are introduced.

Testing

• lake env lean TNLean/MPS/Core/Blocking.lean
• lake exe cache get
• lake build TNLean.MPS.Core.Blocking -q --log-level=info
• rg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/MPS/Core/Blocking.lean || true
• lake build TNLean -q --log-level=info
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main
• python3 scripts/blueprint_lean_sync.py --root . --ci

---

Note

Low Risk
Proof-only refactor in one theorem; no API or runtime behavior change.

Overview
In sum_evalWord_mul_conjTranspose_evalWord, the hand-built equivalence that reverses length-L physical words (ρ ↦ ρ ∘ Fin.rev with explicit inverse proofs) is replaced by Equiv.arrowCongr Fin.revPerm (Equiv.refl (Fin d)), matching patterns elsewhere in the repo (e.g. rotateConfig).

The reversed-word step still goes through list_ofFn_comp_fin_rev; the only proof tweak is unfolding revEquiv, Equiv.arrowCongr, and Function.comp_def in the hword simplification instead of the old local equivalence definition.

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

[claude]

Blueprint ↔ Lean review (categories A and B only)

Category A — Blueprint ↔ Lean equivalence and status

Theorem MPSTensor.sum_evalWord_mul_conjTranspose_evalWord

Blueprint entry: blueprint/src/chapter/ch13_parent_hamiltonian_block_diagonal.tex, lines 1176–1208.

• Statement equivalence (A.1): blueprint hypothesis $\sum_a A_a A_a^\dagger = I$ matches hRight : ∑ i : Fin d, A i * (A i)ᴴ = 1; blueprint conclusion "for every length $M$, $\sum_\rho A_\rho A_\rho^\dagger = I$" matches ∀ L : ℕ, ∑ ρ : Fin L → Fin d, evalWord A (List.ofFn ρ) * (evalWord A (List.ofFn ρ))ᴴ = 1. No discrepancy.
• \leanok accuracy (A.2): The PR is a pure proof-body refactor — the theorem signature is unchanged and no sorry is introduced. Both the statement \leanok (line 1179) and proof \leanok (line 1193) remain valid.
• No blueprint files were modified, so no stale tags, missing \lean{...} tags, or \uses drift to flag.

Category B — Prose quality

No blueprint .tex files, docstrings, or comments were modified by this PR. Nothing to flag.

---

0 equivalence mismatches · 0 stale \leanok · 0 prose issues

[claude]

PR cleanup

Field	Before	After
Title	`refactor(MPS): use arrow congruence for word reversal`	`refactor(MPS/Core): use arrow congruence for word reversal`
Body	`## Summary` / `## Validation` sections	Restructured to `### Motivation` / `### Description` / `### Testing` template; Cursor Bugbot block preserved
Labels	(none)	added: `cleanup`
Issue	No linked issue found — branch name contains no issue number, body has no `Refs`/`Closes`/`Addresses` reference, commit messages contain no `#N` reference. Please link the relevant issue manually if one exists.

Conventions: CONTRIBUTING.md

[claude]

Review: refactor(MPS/Core): use arrow congruence for word reversal

I reviewed the single change to TNLean/MPS/Core/Blocking.lean against all required categories. No 🔴 Blocker or 🟡 Requires-changes issues found.

What changed

In the proof of sum_evalWord_mul_conjTranspose_evalWord, the local revEquiv (a hand-built (Fin L → Fin d) ≃ (Fin L → Fin d) carrying ρ ↦ ρ ∘ Fin.rev with explicit left_inv/right_inv proofs) is replaced by Equiv.arrowCongr Fin.revPerm (Equiv.refl (Fin d)), and the hword step now closes via simpa [revEquiv, Equiv.arrowCongr, Function.comp_def] instead of the old unfolding.

Proof correctness ✅

The refactor is faithful. Equiv.arrowCongr e₁ e₂ sends f ↦ e₂ ∘ f ∘ e₁.symm, so here revEquiv ρ = ρ ∘ Fin.revPerm.symm. Since Fin.rev is an involution, Fin.revPerm.symm reduces to Fin.rev, giving revEquiv ρ = ρ ∘ Fin.rev — the same toFun as the deleted equivalence. The two downstream steps that depend on revEquiv (list_ofFn_comp_fin_rev rewriting List.ofFn (revEquiv ρ) to (List.ofFn ρ).reverse, and the Fintype.sum_equiv reindexing) are therefore unaffected, and _ = 1 still discharges via sum_evalWord_conjTranspose_mul_evalWord. No mathematical content changes; the theorem statement and its source citation (arXiv:quant-ph/0608197, Theorem 12) are untouched.

Proof integrity ✅

No sorry, admit, axiom, native_decide, or unsafeCast introduced. Net −8 lines.

Build verification ✅

• lake build TNLean.MPS.Core.Blocking → Build completed successfully (2968 jobs).
• The only warnings emitted are pre-existing header-style lints (Copyright too short, Mathlib.Tactic import) unrelated to this diff.

Type safety / Performance / Modularity / Documentation ✅

No type or coercion concerns (the equivalence types match exactly). The new form aligns with the existing rotateConfig idiom in MPS/MPDO/AreaLaw.lean. No performance regression (the simpa set is small and bounded). Documentation is unaffected.

ℹ️ Advisory (non-blocking)

The hword simplification manually unfolds Equiv.arrowCongr. A slightly more idiomatic alternative would lean on the Equiv.arrowCongr_apply simp lemma rather than unfolding the definition, but the current form is correct and compiles cleanly — acceptable as-is.

Approving. (Note: the PR is currently in draft state, so this approval does not enable merge until it is marked ready.)

[claude]

Review Summary

Verdict: ✅ APPROVE

This is a clean, focused refactor in TNLean/MPS/Core/Blocking.lean that replaces a hand-built reversal equivalence (revEquiv with explicit toFun/invFun/left_inv/right_inv proofs, 8 lines) with Mathlib's Equiv.arrowCongr Fin.revPerm (Equiv.refl (Fin d)) (1 line). No mathematical content is changed.

Detailed findings

🔴 Proof integrity — PASS

• No sorry, axiom, admit, native_decide, or unsafeCast introduced.
• No kernel bypasses or circular reasoning.
• lake build TNLean.MPS.Core.Blocking succeeds cleanly.

🔴 Proof correctness — PASS

• The new equivalence Equiv.arrowCongr Fin.revPerm (Equiv.refl (Fin d)) is mathematically identical to the old ρ ↦ ρ ∘ Fin.rev.
  • arrowCongr's toFun maps f to e₂ ∘ f ∘ e₁.symm; with e₂ = refl (identity) and e₁.symm = Fin.revPerm (self-inverse by revPerm_symm), this reduces to f ∘ Fin.rev.
  • Fin.revPerm is extensionally Fin.rev (via @[simps! apply] revPerm_apply).
• All three uses of revEquiv in the proof remain valid:
  1. hword simplification (line 355): after unfolding revEquiv and arrowCongr, list_ofFn_comp_fin_rev still applies to produce List.ofFn (ρ ∘ Fin.rev) = (List.ofFn ρ).reverse.
  2. Fintype.sum_equiv reindexing (line 369): Fintype.sum_equiv requires only a valid Equiv — arrowCongr produces one.
  3. simpa on line 369: the goal and Fintype.sum_equiv's conclusion are syntactically identical after the f/g abstractions; the simpa succeeds gracefully.

🟡 Mathlib style — PASS

• Replacing hand-built equivalence machinery with Equiv.arrowCongr is idiomatic Mathlib style and matches patterns used elsewhere in this repository (e.g., rotateConfig).
• Fin.revPerm is available via the existing import Mathlib.Data.Fin.Tuple.Basic, which publicly imports Mathlib.Data.Fin.Rev.
• Equiv.arrowCongr and Equiv.refl are foundational and available transitively.
• Line breaks and formatting conform to Mathlib conventions.

🔴 Type safety — PASS

• Equiv.arrowCongr Fin.revPerm (Equiv.refl (Fin d)) : (Fin L → Fin d) ≃ (Fin L → Fin d) — types align correctly.
• No universe or coercion issues.

🟡 Performance — PASS

• No algorithmic change; the simpa unfolds one additional definition (Equiv.arrowCongr), which is negligible.
• No decide, omega, norm_num on large types.

🟡 Modularity & duplication — PASS

• This refactor reduces duplication by replacing custom equivalence proofs with a standard Mathlib combinator.

🟡 Documentation — PASS

• No new definitions or theorems; no new docstrings required.
• The existing theorem docstring (with arXiv reference) is preserved.

🟡 Paper-gap notes — N/A

• No changes under docs/paper-gaps/.

---

No issues found across any review category. The PR is ready to merge.