refactor(MPS/RFP): use native commute algebra for complements#3271
Conversation
claude
Bot
added
formalization
|
PR cleanup
Conventions: CONTRIBUTING.md |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Blueprint ↔ Lean & Prose Review
0 equivalence mismatches · 0 stale tags · 0 prose issues
Category A — Blueprint ↔ Lean equivalence
Only TNLean/MPS/RFP/Decorrelation.lean is changed; no .tex file is touched.
comm_of_complement_comm (removed). No \lean{...} tag references this declaration anywhere in the blueprint. Its removal leaves no stale tag behind.
complement_comm_of_comm (proof rewritten, statement unchanged). This auxiliary lemma carries no direct blueprint tag. It is called by HasCommutingParentHam.complement_comm, whose blueprint entry (\lean{Decorrelation.HasCommutingParentHam.complement_comm}, ch13_parent_hamiltonian_decorrelation.tex lines 221–222) is unaffected. Checked on all A.1 axes:
-
Hypothesis:
HasCommutingParentHam P_Kbundles exactly the idempotent-product data the blueprint names ("$P_K = P_{AX} \circ P_{XB}$ is idempotent-product data"). ✓ -
Conclusion: Lean
(id - h.P_AX) ∘ₗ (id - h.P_XB) = (id - h.P_XB) ∘ₗ (id - h.P_AX)matches blueprint$Q_{AX} \circ Q_{XB} = Q_{XB} \circ Q_{AX}$ . ✓ -
Proof
\leanok: the rewritten proof issorry-free. ✓
Category B — Prose quality
The sole prose change removes the bullet for the deleted theorem from the module overview. No new text is added. No banned terms, Lean jargon, or word-only proof sketches are introduced.
There was a problem hiding this comment.
Review: refactor(MPS/RFP): use native commute algebra for complements
Verdict: Approve. Clean, tightly-scoped refactor of TNLean/MPS/RFP/Decorrelation.lean. No 🔴 or 🟡 issues found.
What I checked
Proof integrity (🔴) — No sorry/admit/axiom/native_decide/unsafeCast introduced. lake build TNLean.MPS.RFP.Decorrelation completes successfully; the only warning is the pre-existing "Copyright too short!" header linter note, which appears in both touched modules and is unrelated to this diff.
Proof correctness (🔴) — The rewritten complement_comm_of_comm ([P, Q] = 0 → [1 − P, 1 − Q] = 0) is mathematically sound and well-structured:
hPQ : Commute P QfromP ∘ₗ Q = Q ∘ₗ PviaModule.End.mul_eq_comp;(Commute.one_right P).sub_right hPQ : Commute P (id − Q);(Commute.one_left (id − Q)).sub_left hP_comp : Commute (id − P) (id − Q);hcomp.eq, translated back to composition notation, closes the goal.
The statement of complement_comm_of_comm is unchanged, and HasCommutingParentHam.complement_comm still calls the same forward lemma. This is a genuine improvement over the prior simp/abel expansion — it delegates to Mathlib's Commute API rather than re-deriving the complement identity by hand.
Modularity / duplication (🟡) — The removed comm_of_complement_comm (reverse direction) has no callers in TNLean/, blueprint/, or scripts/ (it appears only in the .trusted-actions/ working snapshot, which is a copy of this same file). Removal is safe and reduces unused surface area.
Documentation (🟡) — The module overview docstring is correctly updated to drop the removed declaration.
Type safety / performance — No concerns; the proof is a handful of Commute combinators.
Blueprint ↔ Lean sync and prose are out of scope here (handled by the dedicated workflow); I note only that no \lean{comm_of_complement_comm} reference exists in blueprint/, so the removal does not leave a dangling declaration reference.
There was a problem hiding this comment.
Review Summary
The PR is clean and minimal — it removes an unused lemma comm_of_complement_comm and rewrites complement_comm_of_comm using Mathlib's idiomatic Commute API.
🔴 Proof Integrity — PASS
No sorry, admit, axiom, native_decide, or unsafeCast introduced. The removed lemma had zero callers throughout the codebase (confirmed by rg). No circular reasoning or castle-in-the-air issues.
🔴 Proof Correctness — PASS
The new proof of complement_comm_of_comm correctly chains Commute lemmas:
hcomm : P ∘ₗ Q = Q ∘ₗ P→Commute P QviaModule.End.mul_eq_compCommute P Q+Commute.one_right P→Commute P (id - Q)viasub_rightCommute 1 (id - Q)+Commute P (id - Q)→Commute (id - P) (id - Q)viasub_left- Back to composition notation via
Module.End.mul_eq_comp
All Mathlib API lemmas verified present: Commute.one_right (Algebra/Group/Commute/Defs.lean:125), Commute.one_left (Algebra/Group/Commute/Defs.lean:129), Commute.sub_right (Algebra/Ring/Commute.lean:97), Commute.sub_left (Algebra/Ring/Commute.lean:101), Module.End.mul_eq_comp (Algebra/Module/LinearMap/End.lean:53).
🟡 Mathlib Style — PASS
The proof uses idiomatic Commute algebra rather than simp/abel expansion. Variable names are clear. Module overview correctly updated to drop the removed lemma. The abel import is retained because frustration_free_ham_eq still uses it.
🔴 Type Safety — PASS
No type mismatches or coercion issues. The Commute API applies cleanly to E →ₗ[ℂ] E endomorphisms.
🟡 Performance — PASS
The new proof is 6 lines using standard Commute lemmas — no performance concerns.
🟡 Modularity & Duplication — PASS
Correctly uses existing Mathlib Commute API rather than re-proving algebraic identities from scratch.
🟡 Documentation — PASS
Module docstring updated to remove mention of comm_of_complement_comm.
Verdict: APPROVE. No blockers or issues requiring changes found.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
Blueprint ↔ Lean & Prose Review
0 equivalence mismatches · 0 stale tags · 0 prose issues
Category A — Blueprint ↔ Lean equivalence
Only TNLean/MPS/RFP/Decorrelation.lean is changed; no .tex file is touched.
comm_of_complement_comm (removed). grep over blueprint/src/ finds no \lean{comm_of_complement_comm} tag anywhere. Its removal leaves no dangling declaration reference and no stale \leanok behind. ✓
complement_comm_of_comm (proof rewritten, statement unchanged). The signature {P Q : E →ₗ[ℂ] E} (hcomm : P ∘ₗ Q = Q ∘ₗ P) : (id - P) ∘ₗ (id - Q) = (id - Q) ∘ₗ (id - P) is identical before and after the diff. No blueprint tag targets this auxiliary lemma directly. No \leanok status is affected. ✓
A.2 proof \leanok: The rewritten proof is sorry-free; no proof-level status tags require updating. ✓
Category B — Prose quality
The sole prose change deletes one module-docstring bullet (* \comm_of_complement_comm` — ...`). No new prose is introduced. No banned software-engineering terms, no Lean jargon in blueprint prose (no blueprint files are modified), and no word-only proof sketch is added or changed.
There was a problem hiding this comment.
Review: refactor(MPS/RFP): use native commute algebra for complements
Verdict: APPROVE. Clean, minimal refactor with no issues across all review categories.
Category-by-category assessment
🔴 Proof integrity — PASS. No sorry, admit, axiom, native_decide, or unsafeCast anywhere in the diff. The removed lemma comm_of_complement_comm has zero callers in TNLean/, blueprint/, or scripts/ (confirmed by rg). No circular reasoning or ungrounded proof chains.
🔴 Proof correctness — PASS. The rewritten complement_comm_of_comm correctly proves [P, Q] = 0 → [1 − P, 1 − Q] = 0 using Mathlib's Commute subring structure:
hPQ : Commute P QfromhcommviaModule.End.mul_eq_compCommute.one_right PgivesCommute P 1.sub_right hPQyieldsCommute P (id − Q)Commute.one_left (id − Q)givesCommute 1 (id − Q).sub_left hP_compyieldsCommute (id − P) (id − Q)hcomp.eqtranslated back to composition notation closes the goal
Each Commute lemma is verified present in Mathlib (Algebra/Ring/Commute.lean). The proof is mathematically sound and idiomatically delegates to Mathlib's ring-theoretic Commute API rather than re-deriving algebraic identities by hand.
🟡 Mathlib style — PASS. Uses idiomatic Commute subring algebra rather than simp/abel expansion. Variable names are clear. The abel import is retained because frustration_free_ham_eq still uses it.
🔴 Type safety — PASS. No type mismatches or coercion issues. Commute applies cleanly to E →ₗ[ℂ] E endomorphisms via the Ring structure on Module.End.
🟡 Performance — PASS. Six lines of Commute combinators — no heavy tactics or recursion.
🟡 Modularity & duplication — PASS. Correctly uses existing Mathlib Commute API rather than re-proving the complement identity from scratch. The reverse lemma comm_of_complement_comm had no callers and was correctly removed.
🟡 Documentation — PASS. Module docstring accurately updated to drop the removed declaration. No new undocumented declarations.
🟡 Paper-gap notes — N/A. No paper-gap files changed.
Existing feedback
No unresolved review threads exist on this PR. All four prior bot reviews are APPROVED. No PR conversation comment requires follow-up.
There was a problem hiding this comment.
Review: refactor(MPS/RFP): use native commute algebra for complements
Verdict: APPROVE. No 🔴 or 🟡 issues found. Focused, low-risk refactor of one file (TNLean/MPS/RFP/Decorrelation.lean).
Proof integrity 🔴 — clean
No sorry, admit, axiom, native_decide, or unsafeCast introduced; the file remains fully proved.
Proof correctness 🔴 — sound
The rewrite of LinearMap.complement_comm_of_comm ([P, Q] = 0 → [1 − P, 1 − Q] = 0) through the Commute API is correct, and I verified each step against Mathlib v4.31.0:
Module.End.mul_eq_comp : f * g = f.comp g := rfl(Mathlib/Algebra/Module/LinearMap/End.lean:53) justifies translating between*and∘ₗviasimpa.Commute.one_right/Commute.one_left(Mathlib/Algebra/Group/Commute/Defs.lean:125,129) andCommute.sub_right/Commute.sub_left(Mathlib/Algebra/Ring/Commute.lean:97,101) have the exact signatures the proof relies on:(Commute.one_right P).sub_right hPQ : Commute P (1 − Q),(Commute.one_left (id − Q)).sub_left hP_comp : Commute (1 − P) (id − Q).
- The type ascriptions
Commute P (id − Q)andCommute (id − P) (id − Q)typecheck because(1 : Module.End R M) = LinearMap.id := rfl(Module.End.one_eq_id,Mathlib/Algebra/Module/LinearMap/End.lean:51), so1 − Qis definitionallyid − Q. hcomp.eq : (id − P) * (id − Q) = (id − Q) * (id − P)(Commute.eq,Mathlib/Algebra/Group/Commute/Defs.lean:54), andsimpa [Module.End.mul_eq_comp]reduces it to the stated∘ₗgoal.
The mathematical content is unchanged: the conclusion (id − P) ∘ₗ (id − Q) = (id − Q) ∘ₗ (id − P) and the hypothesis P ∘ₗ Q = Q ∘ₗ P are identical to the prior version. The new proof is shorter and more idiomatic than the previous simp + abel expansion.
Modularity & duplication 🟡 — improved
The removed reverse lemma LinearMap.comm_of_complement_comm has no callers anywhere in TNLean/, the blueprint, or docs/ (the only remaining hits are in the .trusted-actions/ snapshot, which is not part of the source tree). Removal is safe and reduces dead surface.
Documentation 🟡 — consistent
The module "Main results" overview is updated to drop the comm_of_complement_comm entry; the surviving complement_comm_of_comm docstring is unchanged and accurate.
Faithfulness / paper-gaps
No docs/paper-gaps/ files touched. The forward direction (the one cited toward arXiv:1606.00608 Appendix D, Proposition D.3) is preserved verbatim; the deletion only drops an unused converse, so the formalization's relationship to the source is unaffected.
Nice cleanup — approving.
2 participants
Motivation
comm_of_complement_commwas a public wrapper with no callers outsideTNLean/MPS/RFP/Decorrelation.lean.Commutealgebra for endomorphisms.Description
comm_of_complement_commfromTNLean/MPS/RFP/Decorrelation.lean.complement_comm_of_commthroughCommute.sub_leftandCommute.sub_right, then translates back to composition notation.[P, Q] = 0 → [1 − P, 1 − Q] = 0remains ascomplement_comm_of_comm, andHasCommutingParentHam.complement_commstill calls the same forward lemma.Testing
lake env lean TNLean/MPS/RFP/Decorrelation.leanlake build TNLean.MPS.RFP.Decorrelationgit diff --checkscripts/blueprint_lean_sync.py --root . --cipython3 scripts/check_reader_facing_prose.pywas run; it reports pre-existing issue-number references outside this file.rg -n "sorry|admit|axiom|native_decide|unsafeCast" TNLean/MPS/RFP/Decorrelation.lean || trueAddresses #234
Note
Low Risk
Local proof refactor in one Lean file; the removed theorem had no callers and the forward result's statement is unchanged.
Overview
Removes the unused reverse lemma
comm_of_complement_command drops it from the module overview.complement_comm_of_commis re-proved via Mathlib'sCommuteAPI (sub_right/sub_lefton complements) instead of expanding(1−P)(1−Q)withsimp/abel.HasCommutingParentHam.complement_commstill calls the same forward lemma; behavior is unchanged.Reviewed by Cursor Bugbot for commit 42edbd5. Bugbot is set up for automated code reviews on this repo. Configure here.