refactor(PEPS): use prod comm equivalence in torus sum#3124
Conversation
|
PR cleanup
No linked issue found. The branch name ( Conventions: CONTRIBUTING.md |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Review: refactor(PEPS): use prod comm equivalence in torus sum
Verdict: APPROVE — no 🔴 or 🟡 issues found.
This is a tightly-scoped, proof-only refactor of the reindexing step inside threeBlockBlueCoeff_comp (TNLean/PEPS/TorusWindowChain4.lean:496). It replaces the hand-built Finset.sum_nbij' swap with Finset.sum_equiv (Equiv.prodComm _ _).
Correctness. The two are equivalent reindexings of the same product sum:
Equiv.prodCommsends(q₁, q₂) ↦ (q₂, q₁), matching the old forward mapi := fun q => (q.2, q.1)and inversej.Finset.sum_equiv's membership obligation∀ i, i ∈ s ↔ e i ∈ tis discharged byrintro ⟨q₁, q₂⟩; constructor, where the forward branch reuses the originali-membership argument and the backward branch reuses the originalj-membership argument — bothsimp only/obtain/exactbodies are unchanged.- The summand equality
hfgremainsfun _ _ => rfl, as in the originalsum_nbij'value argument; the summands are definitionally equal under the swap.
The theorem statement, summands, and surrounding fiberwise grouping (Finset.sum_fiberwise, mergeCollapse2) are untouched.
Proof integrity. No new sorry/axiom/admit/native_decide. The pre-existing TNLean/MPS/Periodic/Overlap/Case3.lean:586 sorry is unrelated to this PR.
Modularity. Net improvement: a project-local explicit bijection is replaced by the standard Mathlib Equiv.prodComm + Finset.sum_equiv pair.
Style, type-safety, performance, and documentation are unaffected (the explanatory comments on both membership branches are preserved).
Note: PR is currently in draft state.
There was a problem hiding this comment.
Blueprint ↔ Lean review (Categories A and B only)
Category A — Blueprint ↔ Lean equivalence and status accuracy
The only Lean declaration modified is TNLean.PEPS.threeBlockBlueCoeff_comp (pure tactic refactor; statement unchanged). Its blueprint counterpart is thm:peps_corner_extension_coefficient_composition in blueprint/src/chapter/ch24_peps_ft_torus.tex:881–898.
A.1 — Mathematical equivalence. The blueprint states
$$\sum_{\nu\in\partial S}\Phi_{R,S}(\mu,\sigma|{S\setminus R},\nu),\Phi{S,P}(\nu,\sigma|{P\setminus S},\omega) = P{V\setminus S},\Phi_{R,P}(\mu,\sigma|_{P\setminus R},\omega)$$
for nested regions regionInteriorBondProd, threeBlockBlueCoeff, and a sum over RegionBoundaryConfig A S, with matching implicit parameters hRS, hSP, bdryR, σ, bcP. No quantifier, hypothesis, or conclusion discrepancy. ✓
A.2 — \leanok accuracy. The statement-level \leanok at line 884 is valid: the Lean signature matches and the proof contains no sorry or admit. There is no \begin{proof}...\leanok...\end{proof} block for this theorem in the blueprint, but that is a pre-existing gap — this PR neither closes a sorry nor touches any .tex file, so it does not introduce or remove any status tags. ✓
A.3 / A.4. No \notready tags involved. No blueprint files changed. No declarations added or renamed. ✓
Category B — Prose quality
The PR changes only tactic proof lines. No docstrings, block comments, section names, or inline comments are added or modified. The two -- comments visible in the diff context are pre-existing and unchanged. No .tex files are touched. ✓
Summary: 0 equivalence mismatches, 0 stale \leanok, 0 prose issues.
There was a problem hiding this comment.
Review: refactor(PEPS): use prod comm equivalence in torus sum
Summary
This is a concise, clean refactor that replaces an ad-hoc Finset.sum_nbij' call in threeBlockBlueCoeff_comp with the higher-level Finset.sum_equiv along Equiv.prodComm. The theorem statement, summands, and proof strategy are unchanged. All review categories pass.
Per-category assessment
| Category | Verdict |
|---|---|
| 1. 🔴 Proof integrity | ✅ Clean — no sorry, axiom, admit, native_decide, unsafeCast, circular reasoning, or debug artifacts introduced |
| 2. 🔴 Proof correctness | ✅ The equivalence swap (q₁, q₂) ↔ (q₂, q₁) is exactly what Equiv.prodComm provides; the membership ↔ is correctly proved by the constructor block, carrying forward the same membership reasoning as the original sum_nbij' |
| 3. 🟡 Mathlib style | ✅ Improves style — sum_equiv is the idiomatic Mathlib API for reindexing sums with equivalences |
| 4. 🔴 Type safety | ✅ No issues; build succeeds |
| 5. 🟡 Performance | ✅ Negligible; the proof is actually simpler |
| 6. 🟡 Modularity | ✅ Uses a standard Mathlib lemma instead of a hand-rolled sum_nbij' pattern |
| 7. 🟡 Documentation | ✅ The theorem already has a thorough docstring (lines 409–416) with paper citation |
| 8. 🟡 Paper-gap notes | N/A — no paper-gap documents changed |
Verdict
APPROVE — no blocking or advisory issues.
2 participants
Motivation
threeBlockBlueCoeff_compinTNLean/PEPS/TorusWindowChain4.leanused a hand-builtFinset.sum_nbij'to swap the product-configuration pairFinset.sum_equivalongEquiv.prodCommis the canonical way to perform this reindexing.Description
TNLean/PEPS/TorusWindowChain4.lean(modified): inthreeBlockBlueCoeff_comp, the explicitFinset.sum_nbij'-based pair-swap is replaced byFinset.sum_equiv Equiv.prodComm. The membership arguments for the separated and agreeing-pair index sets are preserved. The theorem statement and summands are unchanged.Testing
lake env lean TNLean/PEPS/TorusWindowChain4.leanlake build TNLean.PEPS.TorusWindowChain4 -q --log-level=infolake build TNLean -q --log-level=inforg -n "sorry|axiom|admit|native_decide|unsafeCast" TNLean/PEPS/TorusWindowChain4.lean— no new occurrencesTNLean/MPS/Periodic/Overlap/Case3.lean:586:14sorry; no new failures from this change.Note
Low Risk
Proof-only refactor in a PEPS Lean file; no runtime, API, or mathematical statement changes.
Overview
In
threeBlockBlueCoeff_comp, the step that reindexes the product of two filtered virtual-config sums into the agreeing-pair fiber sum no longer uses a hand-builtFinset.sum_nbij'with an explicit(q₂, q₁) ↔ (q₁, q₂)swap.It now applies
Finset.sum_equivalong Mathlib'sEquiv.prodComm, with the same filter membership arguments packaged asrintro/constructorproofs for the separated vs agreeing-pair index sets. The theorem statement and summands are unchanged.Reviewed by Cursor Bugbot for commit 1131034. Bugbot is set up for automated code reviews on this repo. Configure here.