feat(peps): close the injective PEPS Fundamental Theorem (positivity + connectivity faithful)#2406
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6e38963daf
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
Pull request overview
This PR advances the PEPS two-injective tensor insertion comparison formalization (two_injective_tensor_insertion_comparison, issue #1361) by adding sorry-free reduction lemmas and refactoring the main theorem to explicitly split the empty-configuration boundary case from the substantive nonempty-bond case (delegated to a new _core theorem that still contains the remaining sorry).
Changes:
- Added
twoBlockInsertedCoeff_matrixUnit, relating a one-bond matrix-unit insertion to an “open-bond” contraction over configurations. - Added
sameOpenBondContraction, deriving the paper’s first “one-leg-open” reduction fromSameTwoBlockInsertionsvia matrix units. - Refactored
two_injective_tensor_insertion_comparisonto dispatch the empty-config case (vacuous) vs the nonempty-config case (handled by newtwo_injective_tensor_insertion_comparison_corewith a trackedsorry).
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Review:
|
![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
4 missing blueprint entries (Category A) · 4 prose findings (Category B)
Category A — Blueprint ↔ Lean equivalence
The PR adds four new Lean declarations but no corresponding blueprint entries. Per A.4 every new theorem/lemma requires a \begin{theorem/lemma} block with \lean{...}, status tags, and \uses{}.
| Declaration | File line | Status | Finding |
|---|---|---|---|
twoBlockInsertedCoeff_matrixUnit |
239 | sorry-free | Missing entry; generalises thm:peps_twoBlockInsertedCoeff_singletonBond |
twoBlockReciprocalScalarProportional_of_isEmpty_config |
381 | sorry-free | Missing entry; used in the proof of the main theorem |
sameOpenBondContraction |
405 | sorry-free | Missing entry; source-cited first reduction of arXiv:1804.04964 §3 |
two_injective_tensor_insertion_comparison_core |
441 | sorry |
Missing entry; single remaining open case of thm:peps_twoInjectiveTensorInsertionComparison |
The last three of these are all directly cited source steps or load-bearing subcases — none qualify as purely internal implementation details. The \uses{thm:peps_twoInjectiveGaugeScalarReduction} on thm:peps_twoInjectiveTensorInsertionComparison will also need updating once the _core entry exists, to thread the dependency chain through the new intermediates.
Category B — Prose quality
| Location | Finding |
|---|---|
| Line 237 | `twoBlockInsertedCoeff_singletonBond_single` names a Lean declaration in body prose; replace with "the coefficient-extraction theorem for one shared bond" |
| Line 396 | "is equivalent to" overstates the theorem — only the forward direction is proved; replace with "implies equality of" |
| Line 403 | `SameTwoBlockInsertions` and `twoBlockInsertedCoeff_matrixUnit` used as mathematical objects in body prose; replace with mathematical descriptions |
| Line 428 | `threeLeg_residual_forms_scalar` named in body prose (not in the explicitly marked proof-status note); replace with "the residual three-leg comparison theorem" |
There was a problem hiding this comment.
Review Summary
This PR makes genuine progress toward two_injective_tensor_insertion_comparison (#1361), adding three sorry-free lemmas (twoBlockInsertedCoeff_matrixUnit, twoBlockReciprocalScalarProportional_of_isEmpty_config, sameOpenBondContraction) and refactoring the main theorem to dispatch the empty-configuration case. The reduction route is correctly documented and the new proofs are mathematically sound.
However, there are outstanding issues — all already identified by the three bot review comments on this PR — that must be addressed before merge.
🔴 Blocker — Proof Correctness
two_injective_tensor_insertion_comparison_core (line 441) is missing a [Nonempty Bond] hypothesis. The theorem as stated is mathematically false: when Bond is empty, hbond : ∀ b, Nonempty (bondDim b) is vacuously true and SameTwoBlockInsertions is vacuously true, but the reciprocal scalar proportionality conclusion does not hold. A counterexample: single-point external/physical spaces with A₁ ≡ 1, B₁ ≡ 2, A₂ ≡ 1, B₂ ≡ 1. Both injectivity hypotheses hold, both insertion hypotheses hold vacuously, but no nonzero scalar c can satisfy both A₁ = c·B₁ and A₂ = c⁻¹·B₂. Adding [Nonempty Bond] (which is already available in the sole caller, two_injective_tensor_insertion_comparison) makes the statement provable without changing the downstream dispatch.
This was raised by chatgpt-codex-connector[bot] in discussion_r3367464746 and is still unresolved.
🟡 Requires Changes — Documentation
-
sameOpenBondContraction(line 396): The docstring says "The per-bond insertion hypothesis is equivalent to equality of all one-leg-open contractions", but the lemma only proves the forward direction (SameTwoBlockInsertions→ open-leg equality). The reverse direction is not proved. The docstring should say "implies" or "gives."Raised by
Copilotin discussion_r3367465277. -
twoBlockReciprocalScalarProportional_of_isEmpty_config(line 373): The docstring opens with "If some shared virtual bond carries an empty index space", an interpretation of the hypothesis. The hypothesis is directlyIsEmpty (SharedBondConfig bondDim)(the configuration family is empty). The docstring should first state the direct hypothesis before giving the interpretation.Raised by
Copilotin discussion_r3367465290.
ℹ️ Advisory
-
sameOpenBondContractionnaming: TheSameprefix conventionally marks Propositions/predicates in this file (SameAwayFromBond,SameTwoBlockInsertions). This lemma states an equality (Propas conclusion, but an equality statement, not a structural predicate). ConsideropenBondContraction_eq_of_sameInsertionsor similar. -
Unnecessary
open scoped Classical inonsameOpenBondContraction(line 395): The proof is a singlerwathat doesn't need classical reasoning. Harmless but could be removed for cleanliness. -
Documented
sorryon_core: The single remainingsorryis honestly documented with an in-source proof status marker and a precise sketch of the remaining work (the nonlinear inversion ofA₂andB₁to read off the gaugesZ,U,W). Acceptable under the paper-realignment exception inCLAUDE.md. The file builds cleanly with#print axiomsshowing no new axioms.
Verdict
REQUEST_CHANGES — the 🔴 blocker and two 🟡 documentation issues must be resolved before approval. All three are small, well-scoped fixes.
There was a problem hiding this comment.
Review: synchronize — new additions in twoBlockInsertedCoeff_one through twoBlockLeftInverse
Verdict: REQUEST_CHANGES.
No previously raised issues have been addressed. The unresolved threads from the prior review remain: twoBlockInsertedCoeff_matrixUnit (missing blueprint + Lean jargon), twoBlockReciprocalScalarProportional_of_isEmpty_config (missing blueprint + docstring inaccuracy), sameOpenBondContraction (missing blueprint + "equivalent" overstating + Lean jargon), and two_injective_tensor_insertion_comparison_core (missing blueprint + Lean jargon + missing [Nonempty Bond], the last of which is a correctness blocker flagged by the automated reviewer and confirmed in the prior summary). Those threads remain open and are not re-raised here.
This review covers only the newly added declarations: twoBlockInsertedCoeff_one, fullContraction_eq, twoBlockComb, twoBlockLeftInverse (and its auxiliary _comp / _apply wrappers).
New findings: 3 missing blueprint entries (A.4) and 4 Lean-jargon issues (B).
Category A
| Declaration | Issue |
|---|---|
twoBlockInsertedCoeff_one (line 431) |
No blueprint entry; sorry-free theorem cited to arXiv:1804.04964 §3 as "the starting reduction" |
fullContraction_eq (line 467) |
No blueprint entry; sorry-free theorem cited as "the all-identity contraction equality" in the same lemma |
twoBlockLeftInverse (line 507) |
No blueprint definition entry; docstring explicitly names it as the paper's "inverse of an injective tensor" |
Category B
| Line | Issue |
|---|---|
| 428 | `twoBlockInsertedCoeff` Lean identifier used as mathematical reference |
| 464 | `SameTwoBlockInsertions` and `twoBlockInsertedCoeff_one` Lean identifiers used as mathematical references |
| 487 | `Finsupp.linearCombination` namespaced implementation identifier |
| 503 | `twoBlockComb A` Lean expression used as mathematical noun |
There was a problem hiding this comment.
Review: reductions toward two_injective_tensor_insertion_comparison (#1361)
I built the changed file (lake env lean TNLean/PEPS/TwoInjectiveComparison.lean, exit 0): the only sorry warning is at line 566 (two_injective_tensor_insertion_comparison_core), all other new lemmas compile and the Mathlib lemmas they invoke (LinearIndependent.finsuppLinearCombination_injective, LinearMap.exists_leftInverse_of_injective, Classical.nonempty_pi, Function.update_self/update_of_ne) resolve. Net sorry count is unchanged: the old sorry on the main theorem is now discharged via the empty/nonempty dispatch, and the single remaining sorry moved into _core with a clear proof-status marker. The refactor itself is clean.
🔴 Blocker — two_injective_tensor_insertion_comparison_core is false as stated (proof correctness)
two_injective_tensor_insertion_comparison_core (line 556) omits [Nonempty Bond] and instead carries only hbond : ∀ b, Nonempty (bondDim b). That hypothesis set does not force Bond to be inhabited, and when Bond is the empty type the statement is false:
SharedBondConfig bondDim = (b : Bond) → bondDim bis a singleton (the empty dependent function) whenBond = ∅—Classical.nonempty_pigivesNonempty (∀ b, bondDim b)vacuously, so the configuration family is nonempty.hbondis vacuous, andSameTwoBlockInsertions A₁ B₁ A₂ B₂quantifies overb : Bond, sohinsertis also vacuous.- The conclusion
TwoBlockReciprocalScalarProportionalstill demands a single nonzerocwithA₁ = c·B₁andA₂ = c⁻¹·B₂.
Counterexample (all of External₁, External₂, SharedBondConfig, Physical₁, Physical₂ singletons): A₁ = 1, B₁ = 2, A₂ = 1, B₂ = 1. Each tensor is a single nonzero scalar, hence IsTwoBlockInjective; hinsert and hbond hold vacuously; but A₁ = c·B₁ forces c = 1/2 while A₂ = c⁻¹·B₂ forces c = 1 — contradiction. So the sorry at line 566 is unprovable as stated, and _core is a public theorem whose statement is wrong.
This is exactly the unresolved Codex thread (P1 — Require a nonempty shared-bond family) on line 564; I independently confirm it. The defect is contained for now — the only call site (two_injective_tensor_insertion_comparison, line 607) supplies [Nonempty Bond] and derives hbond from a nonempty config, so the main theorem statement remains true and faithful (it is the one-point-external specialization of arXiv:1804.04964 §3 Lemma inj_equal_tensors_2). But a public lemma carrying a load-bearing sorry that can never be discharged must be corrected before merge.
Fix: add [Nonempty Bond] to _core (the source assumes nonzero-dimensional virtual bonds, so this is faithful, and the sole call site already has it in scope). I am leaving the Codex thread unresolved.
🟡 Requires changes — docstring of sameOpenBondContraction overstates the result (documentation)
The docstring (line 398) states the per-bond insertion hypothesis is equivalent to equality of all one-leg-open contractions, but the theorem proves only the forward direction SameTwoBlockInsertions → (one-leg-open equalities). The reverse is not established here. "Equivalent" misrepresents what the declaration proves; it should read "implies". This is already flagged by the Copilot thread and the Claude thread on line 398 — both unresolved and correct; please address one of them.
ℹ️ Advisory — currently-unused scaffolding (modularity)
twoBlockInsertedCoeff_one, fullContraction_eq, twoBlockComb, twoBlockComb_injective, twoBlockLeftInverse, twoBlockLeftInverse_comp, twoBlockLeftInverse_apply, and sameOpenBondContraction are not yet referenced by any proof. This is acceptable given the PR's explicit purpose (reusable reductions toward the _core proof) and each is documented with its intended role, but the dead-code surface should be retired or consumed when the inversion route lands so it does not accumulate.
Out of scope (handled by the Blueprint Sync & Prose Review workflow)
The existing Claude threads requesting blueprint entries (A.4) for twoBlockInsertedCoeff_matrixUnit, twoBlockReciprocalScalarProportional_of_isEmpty_config, sameOpenBondContraction, two_injective_tensor_insertion_comparison_core, and the "Lean identifier in docstring prose" (Category B) notes are blueprint-sync / prose concerns and are not assessed here; I leave them for that workflow.
Paper faithfulness
No docs/paper-gaps/ file is modified in this PR, and the cited note peps_injective_ft_section3_route.tex accurately records the remaining nonlinear inversion obligation (left-inverse of A₂, then B₁, to extract the Z,U,W gauges) — consistent with the _core docstring and the PR's numerical-rank finding. No discrepancy found there.
Verdict
REQUEST_CHANGES. The false _core statement (missing [Nonempty Bond]) is a correctness blocker, and the sameOpenBondContraction "equivalent" overstatement requires a documentation fix. Both are small, mechanical changes.
There was a problem hiding this comment.
Review: feat(peps): reductions toward two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
This is a follow-up review triggered by the synchronize event (new commits pushed after the previous review). The file still compiles (lake build TNLean.PEPS.TwoInjectiveComparison exits 0), and the newly added lemmas in commit 0be58d7 (twoBlockInsertedCoeff_one, fullContraction_eq, twoBlockComb, twoBlockComb_injective, twoBlockLeftInverse, twoBlockLeftInverse_comp, twoBlockLeftInverse_apply) are mathematically correct and properly grounded in Mathlib. However, none of the issues from the previous review cycle have been addressed. The same 🔴 blocker and two 🟡 issues remain.
🔴 Proof correctness — two_injective_tensor_insertion_comparison_core (line 566) is false as stated
The theorem lacks [Nonempty Bond]. When Bond is empty, hbond : ∀ b, Nonempty (bondDim b) and hinsert : SameTwoBlockInsertions … are both vacuous, but the conclusion TwoBlockReciprocalScalarProportional A₁ B₁ A₂ B₂ is not forced — a concrete counterexample with External₁ = External₂ = Physical₁ = Physical₂ = Unit, A₁ ≡ 1, B₁ ≡ 2, A₂ ≡ 1, B₂ ≡ 1 satisfies all hypotheses while the conclusion demands contradictory scalars (c = ½ and c = 1).
Fix: add [Nonempty Bond] to _core. The only call site (in two_injective_tensor_insertion_comparison, line 607) already has [Nonempty Bond] in scope, so the fix passes through with no downstream friction. With this hypothesis the statement becomes true and the documented Z, U, W inversion route is a viable proof target. Until fixed, the sorry on this theorem is not an honest placeholder — it marks an unprovable statement.
(Previously flagged by both the automated reviewer and claude[bot]; still unresolved.)
🟡 Mathlib naming — sameOpenBondContraction (line 407)
This is a theorem but is named in camelCase, reading like a definition. The file consistently uses camelCase/PascalCase for defs and predicates (SameTwoBlockInsertions, SameAwayFromBond, IsTwoBlockInjective) and snake_case for theorems (two_injective_tensor_insertion_comparison_singletonBond, fullContraction_eq, twoBlockInsertedCoeff_one). Rename to a snake_case form, e.g. openBondContraction_of_sameInsertions or same_openBondContraction.
(Previously flagged; still unresolved.)
🟡 Documentation — sameOpenBondContraction docstring (line 398)
The docstring states the per-bond insertion hypothesis "is equivalent to" equality of all one-leg-open contractions, but the theorem only proves the forward direction (SameTwoBlockInsertions → open-bond equality). The reverse direction (which would hold by linearity of X in the matrix insertions) is not proved. Replace "is equivalent to" with "implies" / "gives", or add the reverse lemma.
(Previously flagged; still unresolved.)
ℹ️ Advisory
-
twoBlockReciprocalScalarProportional_of_isEmpty_configdocstring (line 375): Describes the case where "some shared virtual bond carries an empty index space" while the hypothesis is the equivalent but more directIsEmpty (SharedBondConfig bondDim). Stating the hypothesis form would read more cleanly. (Previously flagged; still unresolved.) -
New code quality: The new lemmas in commit 0be58d7 are well-structured.
twoBlockComb_injectivecorrectly dispatches through Mathlib'sLinearIndependent.finsuppLinearCombination_injective(which is definitional —Iff.rfl).twoBlockLeftInverseproperly usesLinearMap.exists_leftInverse_of_injectivefromMathlib/LinearAlgebra/Basis/VectorSpace. The@[simp]lemmastwoBlockLeftInverse_compandtwoBlockLeftInverse_applygive the defining equations. All new proofs are sorry-free and#print axioms-clean. -
The
sorryon_coreis acceptable as a tracked research obligation under the repo's honest-sorry pattern — once the[Nonempty Bond]fix makes the statement true. The net sorry count is unchanged from before this PR (the previous direct sorry in the main theorem is now discharged for the empty-config branch and delegated to_core).
There was a problem hiding this comment.
Review summary (synchronize — new commits)
No issues from the previous round have been fixed; those threads remain open. The new commits add seven source-cited theorems with no blueprint entries and four prose violations.
Category A — Blueprint ↔ Lean equivalence
7 new missing blueprint entries (all in ch13a_peps_ft.tex):
| Declaration | Line | Blueprint action required |
|---|---|---|
twoBlockComb |
488 | \begin{definition} + statement \leanok |
IsTwoBlockInjective.config_linearIndependent |
553 | \begin{lemma} + statement + proof \leanok |
exists_dual_isolating |
592 | \begin{lemma} + statement + proof \leanok |
gauge_eq1 |
621 | \begin{lemma} + statement + proof \leanok |
gauge_eq2 |
656 | \begin{lemma} + statement + proof \leanok |
gauge_inv |
702 | \begin{lemma} + statement + proof \leanok |
exists_bondGauge_of_fullContraction |
777 | \begin{theorem} + statement + proof \leanok |
These are all sorry-free and source-cited to arXiv:1804.04964, Section 3, lines 1157–1204. Each needs \uses{} referencing its dependencies once those entries exist.
7 from previous round still open: twoBlockInsertedCoeff_matrixUnit, twoBlockReciprocalScalarProportional_of_isEmpty_config, sameOpenBondContraction, two_injective_tensor_insertion_comparison_core, twoBlockInsertedCoeff_one, fullContraction_eq, twoBlockLeftInverse.
Category B — Prose quality
4 new prose violations:
| Line | Issue |
|---|---|
| 549 | "bridge" — banned §2 → "connection" |
| 650 | `gauge_eq1` as mathematical reference — banned §1 |
| 764 | `fullContraction_eq` as mathematical reference — banned §1 |
| 771 | "at the heart of" — banned §3 → "central to" |
8 from previous round still open: Lean identifiers in docstrings of twoBlockInsertedCoeff_matrixUnit, sameOpenBondContraction, two_injective_tensor_insertion_comparison_core, twoBlockInsertedCoeff_one, fullContraction_eq, twoBlockComb, twoBlockLeftInverse; "equivalent" overstating sameOpenBondContraction.
There was a problem hiding this comment.
Review (synchronize): feat(peps): reductions toward two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
I checked out the latest commit (4f81a63) and ran lake env lean TNLean/PEPS/TwoInjectiveComparison.lean: it exits 0 with exactly one sorry warning at line 860 (two_injective_tensor_insertion_comparison_core) and no other sorry/axiom/native_decide/admit. The new operator-Schmidt / bond-gauge infrastructure (twoBlockInsertedCoeff_matrixUnit, sameOpenBondContraction, twoBlockInsertedCoeff_one, fullContraction_eq, twoBlockComb, twoBlockLeftInverse, IsTwoBlockInjective.config_linearIndependent, exists_dual_isolating, gauge_eq1/gauge_eq2/gauge_inv, exists_bondGauge_of_fullContraction) all type-check and are sorry-free.
🔴 Proof integrity / correctness — two_injective_tensor_insertion_comparison_core (line 860) is false as stated
This is the merge blocker. It is already raised on the open inline thread from chatgpt-codex-connector (line 868) and in the prior claude[bot] summary; the latest push added [Nonempty External₁] [Nonempty External₂] and (hbond : ∀ b, Nonempty (bondDim b)) but did not add the missing [Nonempty Bond], so the obstruction is unchanged.
When Bond is empty, SharedBondConfig bondDim = ((b : Bond) → bondDim b) is the unique empty function, so it is a singleton (Nonempty holds), while hbond and hinsert : SameTwoBlockInsertions … are both vacuous (they quantify over b : Bond). Take External₁ = External₂ = Physical₁ = Physical₂ = Unit, A₁ ≡ 1, B₁ ≡ 2, A₂ ≡ 1, B₂ ≡ 1. All four are IsTwoBlockInjective (the single index (η, μ) carries the nonzero vector σ ↦ 1), and every hypothesis holds. But TwoBlockReciprocalScalarProportional (def, line 120) requires one c ≠ 0 with TwoBlockScalarProportional A₁ B₁ c and TwoBlockScalarProportional A₂ B₂ c⁻¹, forcing c = ½ and c = 1 simultaneously — contradiction.
Because the statement is false, the sorry at line 860 is not an honest placeholder for a true-but-hard result: it can never be discharged, and any direct downstream use of _core (not routed through the main theorem) would be unsound. This is exactly why fullContraction_eq — the intended first step of the eventual proof — itself carries [Nonempty Bond] (it picks Classical.arbitrary Bond); _core cannot reach it without the same hypothesis.
Fix: add [Nonempty Bond] to two_injective_tensor_insertion_comparison_core. The sole caller two_injective_tensor_insertion_comparison (line 896) already has [Nonempty Bond] in scope, so the instance passes through with zero friction, and with it the documented Z, U, W route becomes a valid proof target for the retained sorry.
🟡 Mathlib naming — sameOpenBondContraction (line 407)
Pure-camelCase theorem name; see the inline comment. Rename to snake_case (e.g. openBondContraction_of_sameInsertions).
ℹ️ Advisory
set_option maxHeartbeats 400000onexists_bondGauge_of_fullContraction(line 757): perdocs/PROOF_INTEGRITY.mdthis is a warning, not a blocker, and it carries an inline justification (noncomputableFintype (SharedBondConfig bondDim)unification across the four gauge-extraction calls). Acceptable.set_option linter.unusedFintypeInType falseonIsTwoBlockInjective.config_linearIndependent: justified inline (theFintypeinstances are used in the proof but not the statement). Acceptable.- Modularity:
exists_dual_isolating,gauge_eq1,gauge_eq2, andgauge_invare fully general linear-algebra facts (operator-Schmidt uniqueness over arbitraryK,V1,V2) with no PEPS content. Consider hoisting them to aTNLean/Algebra/module (or upstreaming) rather than leaving them in a PEPS leaf file. Not blocking. exists_bondGauge_of_fullContractionis sorry-free but currently unused; it is the staged operator-Schmidt step for the eventual_coreproof, so keeping it is reasonable.
Out of scope here (deferred to Blueprint Sync & Prose Review)
The open claude-authored threads requesting blueprint \begin{theorem}/\begin{lemma}/\begin{definition} entries (Category A.4) and the Category B "Lean identifier in docstring prose" threads fall under the Blueprint-Sync/Prose workflow and are not assessed in this review. They were not addressed by the latest push, so I have left them unresolved rather than re-raising them.
No files under docs/paper-gaps/ are changed in this PR, so that review category does not apply.
There was a problem hiding this comment.
Review: feat(peps): reductions toward two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
This is a synchronize-triggered review of commit 4f81a63. The file compiles, the new sorry-free lemmas are mathematically correct, and the operator-Schmidt gauge infrastructure (gauge_eq1, gauge_eq2, gauge_inv, exists_bondGauge_of_fullContraction) is well-structured and properly grounded in Mathlib. However, none of the 🔴 blocker or 🟡 issues from the prior five review cycles have been addressed.
🔴 Blocker — Proof correctness
two_injective_tensor_insertion_comparison_core (line 860) is false as stated — missing [Nonempty Bond]. When Bond is empty, hbond and hinsert are vacuously true and Nonempty (SharedBondConfig bondDim) holds, but the conclusion fails: A₁=1, B₁=2, A₂=1, B₂=1 on singletons forces contradictory scalars (c = 1/2 and c = 1). The sorry on this theorem is not an honest placeholder — it marks an unprovable statement.
Fix: add [Nonempty Bond] to _core. The sole caller (line 911) already has [Nonempty Bond] in scope.
This was raised by chatgpt-codex-connector[bot] in discussion_r3367464746 and confirmed independently in every subsequent review cycle. Must be fixed before merge.
🟡 Mathlib style — sameOpenBondContraction (line 407)
Named in camelCase but is a theorem. The file convention is camelCase/PascalCase for defs/predicates and snake_case for theorems. Rename to e.g. openBondContraction_of_sameInsertions. Previously flagged by claude[bot] across multiple cycles. Must be fixed before approval.
🟡 Documentation — sameOpenBondContraction docstring (line 398)
States the per-bond insertion hypothesis "is equivalent to" open-leg equalities, but only the forward direction (SameTwoBlockInsertions → open-bond equality) is proved. Replace "equivalent" with "implies." Previously flagged by copilot-pull-request-reviewer[bot] in discussion_r3367465277. Must be fixed before approval.
ℹ️ Advisory
-
twoBlockReciprocalScalarProportional_of_isEmpty_configdocstring (line 375): Opens with an interpretation rather than the direct hypothesisIsEmpty (SharedBondConfig bondDim). Advisory only. -
maxHeartbeats 400000(line 757): Justified byClassical-derivedFintypeinstances but consider sharing the instance across the four gauge calls. Advisory only. -
All new sorry-free proofs are mathematically sound (
gauge_eq1,gauge_eq2,gauge_inv,exists_bondGauge_of_fullContraction,config_linearIndependent,exists_dual_isolating,twoBlockInsertedCoeff_matrixUnit,twoBlockInsertedCoeff_one,fullContraction_eq,twoBlockComb,twoBlockLeftInverse). The operator-Schmidt gauge extraction correctly applies dual functionals to linear independent families. -
The documented
sorryon_coreis acceptable as a tracked research obligation — once the[Nonempty Bond]fix makes the statement true. Net sorry count is unchanged from before this PR. The Z, U, W inversion route is a viable proof target.
Out of scope
Blueprint ↔ Lean sync and prose quality issues (previously flagged Category A/B threads) are not assessed here per review instructions.
LionSR
changed the title
There was a problem hiding this comment.
Blueprint ↔ Lean & Prose Review (synchronize)
4 missing blueprint entries (Category A) · 4 prose findings (Category B)
Resolved from prior rounds
Two open threads are now settled:
[Nonempty Bond]missing in_core(chatgpt-codex-connectorthread, previously a 🔴 correctness blocker):two_injective_tensor_insertion_comparison_corenow carries[Nonempty Bond]in its signature. ✅ Thread resolved.`threeLeg_residual_forms_scalar`in prose (claude thread): the old proof sketch was replaced entirely. ✅ Thread resolved (outdated).
Category A — Blueprint ↔ Lean equivalence
A.2 — Proof \leanok on thm:peps_twoInjectiveTensorInsertionComparison ✅
The \leanok added to \begin{proof} is valid: the Lean proof of two_injective_tensor_insertion_comparison is now fully sorry-free (it dispatches to two_injective_tensor_insertion_comparison_core and twoBlockReciprocalScalarProportional_of_isEmpty_config, both sorry-free). No action required here.
A.4 — New missing blueprint entries (this synchronize)
Four new sorry-free source-cited theorems have no blueprint entry (inline comments posted):
| Declaration | Line | Required entry |
|---|---|---|
bilinear_coeff_zero |
849 | \begin{lemma} + statement \leanok + proof \leanok |
reindex_update |
886 | \begin{lemma} + statement \leanok + proof \leanok |
bondGauge_master_constraint |
925 | \begin{theorem} + statement \leanok + proof \leanok |
bondGauge_scalar_of_master |
1042 | \begin{theorem} + statement \leanok + proof \leanok |
A.4 — Update required on existing open thread
The existing thread on two_injective_tensor_insertion_comparison_core (PRRT_kwDORK8b986Hkg0Y) noted that the blueprint entry should not include a proof \leanok (proof was sorry). The proof is now sorry-free. The blueprint entry, when added, must include proof \leanok as well.
A.4 — Prior missing entries (from review bodies, still open)
The following entries were flagged in the bodies of prior reviews but have not been added. They must still be addressed:
| Declaration | Round first raised |
|---|---|
twoBlockInsertedCoeff_matrixUnit |
Round 1 |
twoBlockReciprocalScalarProportional_of_isEmpty_config |
Round 1 |
sameOpenBondContraction |
Round 1 |
two_injective_tensor_insertion_comparison_core |
Round 1 |
twoBlockInsertedCoeff_one |
Round 2 |
fullContraction_eq |
Round 2 |
twoBlockLeftInverse |
Round 2 |
IsTwoBlockInjective.config_linearIndependent |
Round 3 |
exists_dual_isolating |
Round 3 |
gauge_eq1 |
Round 3 |
gauge_eq2 |
Round 3 |
gauge_inv |
Round 3 |
exists_bondGauge_of_fullContraction |
Round 3 |
Category B — Prose quality
New inline comments posted for four issues:
| Location | Issue |
|---|---|
| Lean line 915 | `sameOpenBondContraction` as mathematical reference (§1) |
| Lean line 1039 | "packages" — banned §2 term |
| Lean lines 1127–1134 | Four Lean identifiers as mathematical references in _core docstring (§1) |
| Blueprint line 2418 | "packaged" in proof sketch — banned §2 term |
Prior prose issues raised in review bodies (still unaddressed):
| Location | Issue | Round |
|---|---|---|
| Lean line 549 | "bridge" — banned §2 | Round 3 |
| Lean line 650 | `gauge_eq1` as mathematical reference (§1) |
Round 3 |
| Lean line 771 | "at the heart of" — banned §3 | Round 3 |
Summary: 4 new A.4 entries missing · 1 A.4 entry needing proof \leanok update · 13 prior A.4 entries still missing · 4 new prose findings · 3 prior prose findings unaddressed. REQUEST_CHANGES.
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
The main theorem two_injective_tensor_insertion_comparison is now fully proven — the sorry is gone, #print axioms is clean, and the proof strategy (operator-Schmidt uniqueness on the fully contracted state → bond gauge → master per-bond constraint → scalar-diagonal gauge → reciprocal proportionality) is mathematically sound and well-structured. This is a substantial achievement and closes #1361.
However, three 🟡 issues remain, two of which were flagged in previous review cycles and are still unfixed.
🟡 Mathlib naming — sameOpenBondContraction (line 407)
This theorem is named in pure camelCase with no snake_case structure, so it reads like a def/predicate. The file convention is camelCase/PascalCase for definitions/predicates (SameTwoBlockInsertions, SameAwayFromBond, IsTwoBlockInjective) and snake_case for theorems (fullContraction_eq, gauge_eq1, bilinear_coeff_zero, bondGauge_master_constraint). All other new theorems in this PR follow snake_case.
Rename to a snake_case form such as openBondContraction_of_sameInsertions.
Flagged in the previous review cycle and remains unfixed. Must be fixed before approval.
🟡 Documentation accuracy — sameOpenBondContraction docstring (line 398)
The docstring says:
The per-bond insertion hypothesis is equivalent to equality of all one-leg-open contractions
But the Lean theorem only proves the forward direction: SameTwoBlockInsertions → (equal one-leg-open contractions). Writing "equivalent" overstates the result. Change "is equivalent to" to "implies" or state the proved direction explicitly.
Flagged in the previous review cycle and remains unfixed. Must be fixed before approval.
🟡 Dead code — twoBlockLeftInverse machinery (lines 483–532)
The five declarations twoBlockComb, twoBlockComb_injective, twoBlockLeftInverse, twoBlockLeftInverse_comp, and twoBlockLeftInverse_apply are unused in the final proof. Grep confirms that twoBlockComb and twoBlockLeftInverse are referenced only in their own definitions and companion theorems — never in two_injective_tensor_insertion_comparison_core or anywhere else in the file (or codebase).
The PR description acknowledges the proof strategy shifted from the left-inverse-of-A₂ approach to operator-Schmidt uniqueness (gauge_eq1/gauge_eq2/gauge_inv → exists_bondGauge_of_fullContraction). These five declarations (~45 lines) are legacy from the abandoned approach and should be removed, or a comment must document the planned future use.
Must be resolved before approval.
ℹ️ Advisory
maxHeartbeats 400000(line 757): Well-documented, modest raise, acceptable. TheClassical-derived noncomputableFintypeinstances forSharedBondConfig bondDimcause unification overhead across the four gauge-extraction calls inexists_bondGauge_of_fullContraction.exists_dual_isolating(line 592) andbilinear_coeff_zero(line 849): These are general lemmas about linear independence in complex vector spaces that could be upstreamed to Mathlib. Fine for now.- No paper-gap files are modified in this PR, so that review category does not apply.
- The blueprint ↔ Lean and prose review categories are handled by the dedicated workflow and are not covered here.
There was a problem hiding this comment.
Blueprint ↔ Lean sync and prose review — synchronize round
Summary of new findings (this round only; prior unresolved threads still stand):
Category A — equivalence and status: 3 issues
| # | Kind | Location | Issue |
|---|---|---|---|
| A1 | A.4 missing entry | TwoInjectiveComparison.lean:777 |
exists_bondGauge_of_fullContraction — the key operator-Schmidt uniqueness step. The new blueprint proof sketch directly corresponds to it but has no blueprint node. |
| A2 | A.4 missing entries | TwoInjectiveComparison.lean:621–702 |
gauge_eq1, gauge_eq2, gauge_inv — three source-cited (arXiv:1804.04964, lines 1157–1204), sorry-free sub-lemmas of the operator-Schmidt argument, with no blueprint entries. |
| A3 | A.4 missing entries | TwoInjectiveComparison.lean:925, 1042 |
bondGauge_master_constraint and bondGauge_scalar_of_master — the master constraint equation labeled \eqref{eq:peps_residual_equality} in the new blueprint proof and the "Hence |
Note (not a new finding, stale comment): The proof body of gaugeConsistency (FundamentalTheorem.lean, line 599) still says "two_injective_tensor_insertion_comparison, still sorry, #1361". That sorry was removed by this PR. The comment should be updated to reflect the new status.
Category B — prose: 5 issues
| # | Kind | Location | Issue |
|---|---|---|---|
| B1 | §2 banned term | TwoInjectiveComparison.lean:549 |
"bridge" as a noun for a connection → "connection" or restate mathematically. |
| B2 | §3 banned phrase | TwoInjectiveComparison.lean:771 |
"at the heart of" → "central to". |
| B3 | §1 Lean identifiers | TwoInjectiveComparison.lean:1127–1135 |
Five Lean declaration names used as mathematical references in the two_injective_tensor_insertion_comparison_core docstring. |
| B4 | §1 Lean identifiers | TwoInjectiveComparison.lean:1195–1203 |
Three Lean declaration names used as proof-structure description in the two_injective_tensor_insertion_comparison docstring. |
| B5 | §prose formula | blueprint/ch13a_peps_ft.tex:2397–2398 |
"equates the two fully contracted states" is a word-only description of the key contraction identity |
| B6 | §1 Lean identifier | TwoInjectiveComparison.lean:915 |
`sameOpenBondContraction` in the bondGauge_master_constraint docstring. |
Count: 3 equivalence/status issues (A1–A3), 6 prose issues (B1–B6). Existing unresolved threads from the prior round remain open.
| The fully contracted identity supplies a bond gauge `g` with `A₁ = g · B₁` and | ||
| `B₂ = g · A₂` (`exists_bondGauge_of_fullContraction`). Substituting both gauge | ||
| equations into each one-leg-open contraction (`sameOpenBondContraction`) and | ||
| separating the two injective families `B₁` and `A₂` yields the master per-bond | ||
| constraint `bondGauge_master_constraint`. Iterating that constraint over all | ||
| shared bonds forces `g` to be a nonzero scalar multiple of the identity | ||
| (`bondGauge_scalar_of_master`), which is exactly the source statement that the | ||
| residual gauges on the freed leg groups are scalar. Reinserting `g = lam · 1` | ||
| into the gauge equations gives `A₁ = lam · B₁` and `A₂ = lam⁻¹ · B₂`. -/ |
There was a problem hiding this comment.
Category B — Lean identifiers as mathematical references in docstring (§1)
The proof-sketch portion of this docstring uses five backtick-quoted Lean declaration names as if they were mathematical objects:
`exists_bondGauge_of_fullContraction`,`sameOpenBondContraction`,`bondGauge_master_constraint`,`bondGauge_scalar_of_master`,`g = lam · 1`
Per §1 backticks in Lean docstrings are permitted only "when explaining how to use the API of this declaration." A proof-by-name sketch is not explaining the API; it is narrating the proof. Replace with mathematical phrasing, for example:
The fully contracted identity — contracting all shared bonds by the identity and equating the two states — yields an invertible gauge matrix
$g$ with$A_1 = g \cdot B_1$ and$B_2 = g \cdot A_2$ . Substituting both gauge equations into the one-bond-open contraction and separating the linearly independent Schmidt families forces, for every bond$b$ and endpoints$p,q$ , the master constraint$[\rho_b=q],g_{\rho^{b\to p},\nu}=[\nu_b=p],g_{\rho,\nu^{b\to q}}$ . Iterating over all shared bonds forces$g=\lambda I$ for some scalar$\lambda\neq 0$ . Reinserting gives$A_1=\lambda B_1$ and$A_2=\lambda^{-1}B_2$ .
| When the shared-bond configuration family is nonempty the result is the | ||
| substantive case `two_injective_tensor_insertion_comparison_core`: the fully | ||
| contracted identity yields a bond gauge that the one-leg-open contractions force | ||
| to be a nonzero scalar multiple of the identity, giving $A_1=\lambda B_1$ and | ||
| $A_2=\lambda^{-1}B_2$ (arXiv:1804.04964, Section 3, lines 1157--1204). The | ||
| single-shared-bond specialization is `two_injective_tensor_insertion_comparison_singletonBond`. | ||
| When some shared bond carries an empty index space the configuration family is | ||
| empty and the conclusion holds vacuously | ||
| (`twoBlockReciprocalScalarProportional_of_isEmpty_config`). -/ |
There was a problem hiding this comment.
Category B — Lean declaration names used as mathematical references in docstring (§1)
Lines 1195–1203 reference three Lean declaration names as mathematical descriptions of the proof structure:
two_injective_tensor_insertion_comparison_core…two_injective_tensor_insertion_comparison_singletonBond…twoBlockReciprocalScalarProportional_of_isEmpty_config
Per §1, backtick references in Lean docstrings are permitted only when explaining how to use the API of this declaration. A proof-structure summary is not API documentation. These three sentences (lines 1195–1203) could be dropped entirely — the proof is now sorry-free and the structure is visible from the Lean body — or replaced with a one-sentence mathematical summary of the two cases:
When every shared bond has a nonempty index space the result follows from operator-Schmidt uniqueness; when some bond's index space is empty the conclusion holds vacuously.
| Putting $X=I_{D_b}$ on every shared bond contracts all bonds diagonally and, | ||
| by the insertion equality, equates the two fully contracted states. Writing |
There was a problem hiding this comment.
Category B — word-only description of a contraction identity; formula required
Putting
$X=I_{D_b}$ on every shared bond contracts all bonds diagonally and,
by the insertion equality, equates the two fully contracted states.
This is a verbal description of the key contraction identity without displaying it. Per the prose-style rule for tensor-network arguments, the contraction equality must be written out. The identity being asserted is
Replace the verbal phrase with a display, for example:
Putting $X=I_{D_b}$ on every shared bond in the insertion equality gives, for
every $(\eta_1,\sigma_1,\eta_2,\sigma_2)$,
\[
\sum_{\mu} A_1(\eta_1,\mu,\sigma_1)\,A_2(\eta_2,\mu,\sigma_2)
= \sum_{\nu} B_1(\eta_1,\nu,\sigma_1)\,B_2(\eta_2,\nu,\sigma_2).
\]
Writing each side as a bipartite operator with the linearly independent Schmidt
families supplied by injectivity, the operator-Schmidt uniqueness of
\cite[Section~3]{Molnar2018NormalPEPS} produces …
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
Three 🟡 issues must be addressed before approval. The mathematical content is solid, the main theorem is fully proven (sorry-free, #print axioms clean), and the proof strategy (operator-Schmidt uniqueness → bond gauge → master constraint → scalar reduction) correctly follows arXiv:1804.04964, Section 3, Lemma inj_equal_tensors_2.
Summary of findings
🟡 Blocking issues (must fix before approval):
-
Mathlib naming (
sameOpenBondContraction, line 407): Theorem named in pure camelCase. Should be snake_case perdocs/MATHLIB_naming.md— the file uses camelCase for definitions/predicates (SameTwoBlockInsertions) and snake_case for theorems (fullContraction_eq,twoBlockInsertedCoeff_one). SuggestopenBondContraction_of_sameInsertions. -
Documentation accuracy (line 398): Docstring says the insertion hypothesis is "equivalent" to one-leg-open equality, but the theorem only proves the forward implication. Change "equivalent" to "implies".
-
Modularity (line 621): Five operator-Schmidt lemmas (
gauge_eq1,gauge_eq2,gauge_inv,exists_dual_isolating,bilinear_coeff_zero) are generic linear algebra with no PEPS content. At minimum, add a sectioning comment marking them as general linear algebra (not PEPS-specific) so future clients (MPS, channel theory) can discover them.
ℹ️ Advisory (acceptable with justification):
-
Documentation (line 375):
twoBlockReciprocalScalarProportional_of_isEmpty_configdocstring should state the direct hypothesis (IsEmpty (SharedBondConfig bondDim)) before its interpretation. -
Performance (line 757):
maxHeartbeats 400000is explained and modest — acceptable.
What's good:
- The main theorem
two_injective_tensor_insertion_comparison(arXiv:1804.04964, Lemma inj_equal_tensors_2) is now fully proven —sorry-free,#print axiomsclean. bondDim_eq_of_matrixAlgEquivcloses the bond-dimension equalitysorryinfundamentalTheorem_PEPS(issue #874) using theedgeTransferAlgEquivdimension count.- The proof strategy is faithful to the source paper.
- Both files compile cleanly (
lake env lean TNLean/PEPS/TwoInjectiveComparison.leanandlake env lean TNLean/PEPS/FundamentalTheorem.leanboth exit 0). - The chatgpt-codex-connector's
[Nonempty Bond]concern from a prior review is resolved —_corenow carrieshbond : ∀ b, Nonempty (bondDim b).
Out of scope (handled by Blueprint Sync & Prose Review workflow):
- Missing blueprint entries and Lean-identifier-in-prose findings — these have been flagged in separate prior review rounds and remain tracked there.
There was a problem hiding this comment.
Code review — feat(peps): close two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES (mathematical core is verified and correct; the blocking items are in-scope 🟡 style/modularity/doc-accuracy already raised in the prior cycle and still unaddressed).
I checked out the merge commit, fetched the Mathlib cache, and verified everything below directly.
✅ Proof integrity — clean
lake env lean TNLean/PEPS/TwoInjectiveComparison.lean→ exit 0.lake build TNLean.PEPS.FundamentalTheorem→ success.- Axiom check on the headline results:
two_injective_tensor_insertion_comparison→[propext, Classical.choice, Quot.sound]two_injective_tensor_insertion_comparison_core→[propext, Classical.choice, Quot.sound]
NosorryAxin either. The PR body's "Remaining (precise)" section (claiming_coreretains an honestsorry) is stale — later commits (5d57e2c,4e7a946) closed it. Worth correcting the description, but not a blocker.
- The three
sorrywarnings remaining inFundamentalTheorem.lean(lines 554post_absorption_edge_insertion_equality#1364, 577gaugeConsistency, 1032gauge_unique_mod_edge_scalars) are pre-existing theorems outside this PR's diff — acceptable known TODOs.
✅ Proof correctness — verified
The new proof replaces the planned three-leg Z,U,W/threeLeg_residual_forms_scalar route with a direct operator–Schmidt uniqueness argument, and it is sound:
exists_bondGauge_of_fullContractionbuilds an invertible bond gaugeg(with explicit inverseg',g*g'=1) from the fully contracted identity viagauge_eq1/gauge_eq2and config-indexed linear independence (IsTwoBlockInjective.config_linearIndependent).gauge_invcorrectly yieldsg·g' = 1.- I hand-checked
bondGauge_scalar_of_master:hoffdiag(instantiating the master constraint atp=q=μ b,ρ=μ) forcesg μ ν = 0whenμ b ≠ ν b;hconst1(atp=ν b,ρ=update ν b q) gives diagonal invariance under single-bond edits; theFinset.inductionhagreepropagates this tog = λ·I, andg*g'=1forcesλ ≠ 0. Correct. - Faithfulness: the public signature of
two_injective_tensor_insertion_comparisonis unchanged — the fourIsTwoBlockInjectivehypotheses andSameTwoBlockInsertionsmatch the pre-existing statement and arXiv:1804.04964 §3 Lemmainj_equal_tensors_2. No hypothesis was smuggled in; the[Nonempty …]instances are structural. The empty-SharedBondConfigbranch is discharged vacuously (twoBlockReciprocalScalarProportional_of_isEmpty_config), matching the source's nonzero-bond setting.
✅ Bond-dimension equality (#874) — honestly closed
The new hDim proof in fundamentalTheorem_PEPS discharges the old sorry via edgeTransferAlgEquiv + bondDim_eq_of_matrixAlgEquiv. I confirmed the supporting chain is itself axiom-clean: IsVertexInjective.edgeBlockedThreeSiteInjective, edgeTransferAlgEquiv, and bondDim_eq_of_matrixAlgEquiv each print [propext, Classical.choice, Quot.sound]. So the bond-dim closure is not resting on a hidden sorry. bondDim_eq_of_matrixAlgEquiv itself is a clean Module.finrank_matrix + Nat.mul_self_inj argument.
🟡 Items that must be addressed before approval (already on record from the prior cycle)
- Naming —
sameOpenBondContractionis atheorem(Prop-valued equality) with a pure-camelCase name, unlike its siblingsfullContraction_eq,twoBlockInsertedCoeff_one,twoBlockComb_injective. Perdocs/MATHLIB_naming.md, theorems takesnake_case(e.g.open_bond_contraction_eq/…_of_sameInsertions). (Existing thread on line 407.) - Documentation accuracy —
sameOpenBondContraction's docstring says the per-bond insertion hypothesis is "equivalent" to the one-leg-open equalities, but the lemma proves only the forward implication (SameTwoBlockInsertions →open-leg equality). Change "equivalent" to "implies". (Existing threads on line 398.) - Modularity —
gauge_eq1,gauge_eq2,gauge_inv,exists_dual_isolating, andbilinear_coeff_zeroare fully general operator-Schmidt / linear-algebra lemmas ({K V1 V2 : Type*}, no PEPS content) living in a PEPS application file. They should be relocated to anAlgebra/-layer module (and are plausibly upstreamable). (Existing thread on line 621.)
ℹ️ Advisory
- Performance:
set_option maxHeartbeats 400000 inonexists_bondGauge_of_fullContractionis justified by the noncomputableClassical-derivedFintype (SharedBondConfig …)unification across the four gauge-extraction calls, and is documented inline. Acceptable; a more targeted instance fix would be preferable long-term. (Existing thread on line 757.) - Stale comment: in
gaugeConsistency(FundamentalTheorem.lean:595–599, outside the diff hunks) the dependency note still callstwo_injective_tensor_insertion_comparison"stillsorry, #1361". This PR makes that false — after merge the only open dependency ofgaugeConsistencyispost_absorption_edge_insertion_equality(#1364). Please refresh that comment.
The Category A (blueprint \lean/\leanok/missing-entry) and Category B (Lean identifiers / banned phrasing in docstrings and .tex) threads are handled by the dedicated Blueprint Sync & Prose Review workflow and are out of scope here; I have not duplicated or resolved them.
Overall: excellent, genuinely sorry-free and axiom-clean mathematics on the injective-PEPS path. The remaining blockers are the naming, docstring-accuracy, and lemma-placement cleanups above.
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
The PR makes substantial mathematical progress: two_injective_tensor_insertion_comparison is now sorry-free (0 sorries in TwoInjectiveComparison.lean), the fundamentalTheorem_PEPS bond-dimension equality hDim is discharged via bondDim_eq_of_matrixAlgEquiv with edgeTransferAlgEquiv (closing #874), and the open-edge gauge machinery in TNLean/PEPS/FundamentalTheorem.lean (edgeInsertedCoeff_applyGauge et al.) is complete. The _core theorem now correctly carries [Nonempty Bond], fixing the falsity identified in the previous review. The proof route — operator-Schmidt uniqueness via bipartite decompositions, a bond gauge g, a per-bond master constraint, and scalar-diagonality of g — is the paper-faithful route described in docs/paper-gaps/peps_injective_ft_section3_route.tex. I build-checked the branch: lake build TNLean.PEPS.TwoInjectiveComparison and lake build TNLean.PEPS.FundamentalTheorem both succeed, and the only remaining sorries in the touched files are the pre-existing obligations gaugeConsistency and post_absorption_edge_insertion_equality.
However, six 🟡 issues remain from the previous review, none of which were addressed in this push:
🟡 Mathlib naming — sameOpenBondContraction (line 407)
Named in pure camelCase (reads like a def/predicate). The file convention is snake_case for theorems. Rename to e.g. openBondContraction_of_sameInsertions.
🟡 Documentation accuracy — "equivalent" overstatement (line 398)
The docstring for sameOpenBondContraction claims the per-bond insertion hypothesis is "equivalent" to the one-leg-open equalities, but the Lean theorem only proves the forward direction (SameTwoBlockInsertions → equality). Write "implies" or state the proved direction explicitly.
🟡 Modularity — operator-Schmidt lemmas in PEPS file
gauge_eq1, gauge_eq2, gauge_inv, exists_dual_isolating, and bilinear_coeff_zero (lines 592–849) are generic linear-algebra results stated over abstract {K V1 V2 : Type*} with no PEPS content. They should be relocated to a shared algebra module or at minimum have a section comment marking them as general linear algebra.
🟡 Documentation — banned terms
- "bridge" (line 549, §2 of
docs/prose_style.md) - "at the heart of" (line 771, §3 of
docs/prose_style.md)
🟡 Blueprint — missing entries
Eleven new sorry-free theorems (twoBlockInsertedCoeff_matrixUnit, sameOpenBondContraction, fullContraction_eq, twoBlockLeftInverse, exists_bondGauge_of_fullContraction, gauge_eq1/eq2/inv, bondGauge_master_constraint, bondGauge_scalar_of_master, two_injective_tensor_insertion_comparison_core) lack corresponding \begin{theorem}/\begin{lemma} blocks with \lean{...}/\leanok tags in ch13a_peps_ft.tex.
ℹ️ Advisory (do not block approval)
- The
maxHeartbeats 400000onexists_bondGauge_of_fullContractionis explained and modest. - The
twoBlockReciprocalScalarProportional_of_isEmpty_configdocstring describes an interpretation of the hypothesis ("some shared virtual bond carries an empty index space") rather than the hypothesis itself (IsEmpty (SharedBondConfig bondDim)). State the hypothesis form first. - Several docstrings contain backtick-quoted Lean identifiers in prose (Category B from previous review). While these should be fixed per
docs/prose_style.md§1, these are handled by the dedicated Blueprint Sync & Prose Review workflow and are not separately enforced here.
What was fixed since the last review
- ✅
two_injective_tensor_insertion_comparison_corenow has[Nonempty Bond]— the falsity identified in the previous review is resolved. - ✅
two_injective_tensor_insertion_comparison_coreis now proof-complete (wassorry). - ✅
two_injective_tensor_insertion_comparisonis now sorry-free (0 sorries inTwoInjectiveComparison.lean). - ✅
fundamentalTheorem_PEPS'shDimsorry is discharged viabondDim_eq_of_matrixAlgEquiv+edgeTransferAlgEquiv.
| first block, | ||
| \leanok | ||
| Putting $X=I_{D_b}$ on every shared bond contracts all bonds diagonally and, | ||
| by the insertion equality, equates the two fully contracted states. Writing |
There was a problem hiding this comment.
🟡 Blueprint — missing entries for new sorry-free Lean theorems.
The following new theorems in this PR (all sorry-free) contribute steps to the proof of thm:peps_twoInjectiveTensorInsertionComparison but lack corresponding \begin{theorem}/\begin{lemma} blocks with \lean{...} and \leanok tags:
twoBlockInsertedCoeff_matrixUnit— generalizes_singletonBond_singleto a multi-bond family; cited as "the matrix-unit coefficient-extraction result"twoBlockReciprocalScalarProportional_of_isEmpty_config— the vacuous empty-config casesameOpenBondContraction— the first reduction:SameTwoBlockInsertions⟹ one-leg-open equalitiestwoBlockInsertedCoeff_one— the identity-insertion specializationfullContraction_eq— the all-identity contraction equalitytwoBlockLeftInverse— the chosen left inverse of the injective linear-combination mapexists_bondGauge_of_fullContraction— the operator-Schmidt uniqueness stepgauge_eq1,gauge_eq2,gauge_inv— the individual operator-Schmidt equationsbondGauge_master_constraint— the per-bond master constraint equation \eqref{eq:peps_residual_equality}bondGauge_scalar_of_master— the scalar-diagonality conclusiontwo_injective_tensor_insertion_comparison_core— the substantive nonempty-bond case, to which the new\leanokproof sketch in this file corresponds
Each entry needs \lean{...}, statement \leanok, proof \leanok (for sorry-free theorems), and appropriate \uses{} references. The existing \uses{} on thm:peps_twoInjectiveTensorInsertionComparison should gain these entries.
This was flagged in the previous review cycle and remains unresolved. Must be fixed before approval.
There was a problem hiding this comment.
Blueprint ↔ Lean review (synchronize)
Positive changes
The proof \leanok added to \begin{proof} of thm:peps_twoInjectiveTensorInsertionComparison is now correctly placed: two_injective_tensor_insertion_comparison is fully sorry-free in this push (delegating to the new two_injective_tensor_insertion_comparison_core and twoBlockReciprocalScalarProportional_of_isEmpty_config, both sorry-free). No issue there.
Category A — Blueprint ↔ Lean equivalence
1 new finding (A.4) — missing blueprint entry on line 1163 of TNLean/PEPS/FundamentalTheorem.lean:
edgeInsertedCoeff_applyGaugeis a public, sorry-free theorem explicitly cited to arXiv:1804.04964, Section 3. It is the key open-edge gauge-action identity that feeds into the still-openpost_absorption_edge_insertion_equality. A\begin{lemma}block with\lean{...}, statement\leanok, proof\leanok, and\uses{...}is required. (Inline comment at line 1163.)
All other Category A issues from prior rounds (missing blueprint entries for twoBlockInsertedCoeff_matrixUnit, sameOpenBondContraction, fullContraction_eq, twoBlockInsertedCoeff_one, twoBlockLeftInverse, exists_bondGauge_of_fullContraction, gauge_eq1/2, gauge_inv, bondGauge_master_constraint, bondGauge_scalar_of_master, two_injective_tensor_insertion_comparison_core) remain unresolved.
Category B — Prose quality
7 new findings — all in TNLean/PEPS/FundamentalTheorem.lean, all are §1 Lean-identifier-as-mathematical-reference violations in the new open-edge gauge section:
| Line | Declaration | Identifier |
|---|---|---|
| 487 | section comment | `applyGauge_stateCoeff` |
| 515 | insertedOpenConfigEquiv |
`virtualConfigEquivEdgeBoundary` |
| 808 | edgeInsertedCoeff_eq_sum_local |
`sum_local_with_edge_deltas` |
| 900 | prod_gaugeVertex_eq_sum_local_open |
`prod_gaugeVertex_eq_sum_local` |
| 954 | open_gauge_sum_over_outer |
`gauge_sum_over_virtual` |
| 1163 | edgeInsertedCoeff_applyGauge |
`applyGauge_stateCoeff` (+ A.4) |
| 1390 | bondDim_eq_of_matrixAlgEquiv |
`fundamentalTheorem_PEPS_of_bondDim` |
| 1421 | fundamentalTheorem_PEPS |
`gaugeConsistency` |
All other Category B issues from prior rounds remain unresolved.
Summary: 1 Category A equivalence finding (A.4), 8 Category B prose findings (new). REQUEST_CHANGES.
| square of its index size. | ||
|
|
||
| Source: standard dimension count; used to discharge the bond-dimension equality | ||
| hypothesis of `fundamentalTheorem_PEPS_of_bondDim` (issue #874). -/ |
There was a problem hiding this comment.
Category B — Lean identifier in docstring prose (§1)
Source: standard dimension count; used to discharge the bond-dimension equality hypothesis of
`fundamentalTheorem_PEPS_of_bondDim`(issue #874).
`fundamentalTheorem_PEPS_of_bondDim` names a Lean theorem in a maintainer note rather than describing mathematics. Replace with a mathematical description, e.g.:
Source: standard dimension count. This equality is used to discharge the bond-dimension hypothesis in the fundamental theorem for injective PEPS (issue #874).
There was a problem hiding this comment.
Review — re-review on synchronize
I rebuilt the PR head and verified the proof-integrity claims directly. This is genuine, verified mathematical progress: two sorrys are closed, axiom-clean. The blockers to approval are the outstanding 🟡 issues from the previous review cycle, which the latest push has not addressed (so they remain unresolved, not re-posted here).
Proof integrity & correctness — verified ✅ (🔴 category clean)
lake build TNLean.PEPS.TwoInjectiveComparison TNLean.PEPS.FundamentalTheorem → exit 0. #print axioms on the newly closed declarations returns only [propext, Classical.choice, Quot.sound] — no sorryAx:
two_injective_tensor_insertion_comparison(#1361,lem:inj_equal_tensors_2) — the formersorryis gone; the theorem statement is unchanged from the priorsorryversion, so no hypothesis was smuggled in (faithfulness rule satisfied). The whole operator-Schmidt support chain (exists_dual_isolating,gauge_eq1/gauge_eq2/gauge_inv,bilinear_coeff_zero,bondGauge_master_constraint,bondGauge_scalar_of_master,exists_bondGauge_of_fullContraction) is therefore sorry-free.two_injective_tensor_insertion_comparison_core— axiom-clean. The empty/nonempty dispatch is sound: with[Nonempty Bond],Bond = ∅cannot reach the empty branch (thenSharedBondConfigis a singleton), so the empty branch fires only when somebondDim bis empty, whereTwoBlockReciprocalScalarProportionalholds vacuously overμ : SharedBondConfig. This correctly discharges the previously-raised P1 (the[Nonempty Bond]hypothesis is now present on_core).fundamentalTheorem_PEPSbond-dimension equality — thehDimsorryis genuinely discharged edgewise viabondDim_eq_of_matrixAlgEquiv(a cleanModule.finrank_matrix+Nat.mul_self_injdimension count) composed withedgeTransferAlgEquiv; both are axiom-clean.bondDim_eq_of_matrixAlgEquivandedgeInsertedCoeff_applyGaugeprint clean axioms.
Remaining sorrys in FundamentalTheorem.lean (lines 1284 post_absorption_edge_insertion_equality, 1331 gaugeConsistency, 1749 gauge_unique_mod_edge_scalars) are all pre-existing, untouched by this PR, and documented in docs/paper-gaps/peps_injective_ft_section3_route.tex — acceptable under paper-realignment mode.
Outstanding 🟡 issues — block approval (already on record, not re-posted)
These were raised in the prior cycle and are still present in the head, so I am not resolving the corresponding threads:
- 🟡 Naming —
TwoInjectiveComparison.lean:407sameOpenBondContractionis atheoremnamed in pure camelCase, reading like adef/predicate. The file convention (and Mathlib) usessnake_casefor theorems (fullContraction_eq,twoBlockInsertedCoeff_onein this same PR). Rename, e.g.openBondContraction_of_sameInsertions. - 🟡 Modularity —
gauge_eq1/gauge_eq2/gauge_inv,exists_dual_isolating,bilinear_coeff_zeroare stated over abstract{K V1 V2 : Type*}with noBond/TwoBlockTensorcontent. As pure operator-Schmidt / dual-functional facts they belong in a shared linear-algebra module (or at minimum need a sectioning comment marking them PEPS-free);exists_dual_isolatingis a plausible Mathlib-upstream candidate. - 🟡 Documentation accuracy —
TwoInjectiveComparison.lean:398: the docstring calls the per-bond insertion hypothesis equivalent to the one-leg-open contractions, but only the forward implication (SameTwoBlockInsertions → equal open-leg contractions) is proved. Change "equivalent" to "implies".
ℹ️ Advisory
maxHeartbeats 400000(TwoInjectiveComparison.lean:757) is documented and modest — acceptable; monitor if it recurs.- The dependency comment inside
gaugeConsistency(FundamentalTheorem.lean:1349–1353) still describestwo_injective_tensor_insertion_comparisonas "stillsorry, #1361". This PR closes #1361, so that annotation is now stale (the line is outside the diff, but the PR makes it false).
Out of scope (handled by the Blueprint Sync & Prose Review workflow)
The numerous prior claude/copilot threads tagged "Category A — missing blueprint entry" and "Category B — Lean identifier / banned phrasing in docstring prose" concern \lean/\leanok/\uses sync and prose quality and are not reviewed here; I have neither re-raised nor resolved them.
Verdict: REQUEST_CHANGES — proof integrity and correctness are excellent and verified, but the 🟡 naming, modularity, and documentation-accuracy items remain unaddressed.
Review:
|
There was a problem hiding this comment.
Review Summary
Verdict: REQUEST_CHANGES — three 🟡 issues must be fixed before approval. No 🔴 blockers.
The previous 🔴 blocker (two_injective_tensor_insertion_comparison_core missing [Nonempty Bond]) is resolved: _core now carries [Nonempty Bond] and hbond : ∀ b, Nonempty (bondDim b), and its proof is complete. No new sorry is introduced. Both TwoInjectiveComparison.lean and FundamentalTheorem.lean compile cleanly.
🟡 Must fix
-
Mathlib naming —
sameOpenBondContraction(TNLean/PEPS/TwoInjectiveComparison.lean:407): Theorem named incamelCase; the file's convention usessnake_casefor theorems. Rename toopenBondContraction_of_sameInsertionsor similar. -
Documentation accuracy — "equivalent" vs "implies" (
TNLean/PEPS/TwoInjectiveComparison.lean:398): Docstring says the insertion hypothesis "is equivalent to" the one-leg-open contraction equalities, but only forward direction is proved. Change to "implies" or "gives." -
Stale comments in
gaugeConsistency(TNLean/PEPS/FundamentalTheorem.lean:1388–1398): Comments saytwo_injective_tensor_insertion_comparisonis "stillsorry" and #1361 is "opensorry" — both are now proved. Update to reflect current status.
ℹ️ Advisory
maxHeartbeats 400000in two locations, explained by noncomputableClassical-derivedFintypeinstances. Acceptable.
What's impressive
- Closes #1361:
two_injective_tensor_insertion_comparisonfully proved (operator-Schmidt → gauge → master constraint → scalar diagonality → proportionality). - Closes #1364:
post_absorption_edge_insertion_equalityproved. - 22 new sorry-free theorems/lemmas across three modules.
fundamentalTheorem_PEPShDim now proved viabondDim_eq_of_matrixAlgEquiv.- The route is mathematically faithful to the paper-gap analysis confirming the obstruction is nonlinear.
Resolution of previous threads
The 🔴 blocker from the prior review is resolved. The 🟡 naming and docstring issues remain — the new push added the missing proofs but did not address the style/docstring items identified earlier.
Blueprint sync and prose quality are out of scope (handled by the dedicated workflow). No paper-gap files are modified.
There was a problem hiding this comment.
Re-review (synchronize): feat(peps): close two_injective_tensor_insertion_comparison (#1361)
Verdict: REQUEST_CHANGES.
I built the changed modules from the merge commit (lake build TNLean.PEPS.TwoInjectiveComparison TNLean.PEPS.FundamentalTheorem TNLean.PEPS.EdgeGaugeFamily → exit 0). Confirmed:
TwoInjectiveComparison.leanandEdgeGaugeFamily.leanbuild clean and sorry-free.two_injective_tensor_insertion_comparison,two_injective_tensor_insertion_comparison_core, andone_vertex_complement_comparisonare now fully proved — #1361 is closed. The empty-config branch dispatches vacuously viatwoBlockReciprocalScalarProportional_of_isEmpty_config; the substantive case runs the operator-Schmidt route (exists_bondGauge_of_fullContraction→bondGauge_master_constraint→bondGauge_scalar_of_master). The proofs are well-structured (Fintype.sum_equiv,Finset.prod_univ_sum, explicitcalc/Finset.sum_congrchains), not brute-forced.- The previously-flagged 🔴 (missing
[Nonempty Bond]on_core) is resolved:_corenow carries[Nonempty Bond]plushbond : ∀ b, Nonempty (bondDim b). - No new
sorry. The onlysorrys in the touched files are pre-existing and separately tracked:gaugeConsistency(line 1399) andgauge_unique_mod_edge_scalars(line 1823), both with proof-status markers and paper-gap references. Acceptable under the repo's scaffolding convention.
🟡 New finding — unscoped maxHeartbeats lint warning (FundamentalTheorem.lean:424)
The build emits a linter.style.setOption warning:
warning: TNLean/PEPS/FundamentalTheorem.lean:424:0: Unscoped option maxHeartbeats is not allowed
The section LargeBudget + bare set_option maxHeartbeats 400000 (lines 423–424) raises the budget for a whole section rather than for the two declarations that need it (prod_gaugeVertex_eq_sum_local, prod_gaugeVertex_eq_sum_local_open). Mathlib style disallows this. The same PR already uses the correct per-declaration set_option maxHeartbeats 400000 in form (before exists_bondGauge_of_fullContraction, and at TwoInjectiveComparison.lean:757), so this is an internal inconsistency. Fix: remove the section/end LargeBudget wrapper and prefix each of the two lemmas with its own set_option maxHeartbeats 400000 in (keeping the explanatory comment). The previous review cycle classified maxHeartbeats as acceptable advisory and missed that this particular form is a build warning — it is a 🟡 style item, not advisory.
Still-open 🟡 items from the prior review cycle (this push did not address them)
These were correctly raised in the previous summary and inline threads and remain unresolved in the current head — they continue to block approval:
- Naming —
sameOpenBondContraction(TwoInjectiveComparison.lean:407) is a theorem named in purecamelCase; the file's theorems usesnake_case(fullContraction_eq,twoBlockInsertedCoeff_one). Rename, e.g.openBondContraction_of_sameInsertions. - Documentation accuracy —
sameOpenBondContractiondocstring (line 398) says the insertion hypothesis "is equivalent to" the one-leg-open contractions, but only the forward implication is proved. Use "implies"/"gives". - Documentation accuracy — stale proof-status comment in
gaugeConsistency(FundamentalTheorem.lean:1388–1398): lines 1389–1390 still calltwo_injective_tensor_insertion_comparison"stillsorry, #1361" and line 1396 says "the one remaining load-bearing dependency (#1361) is an opensorry". This PR closes #1361, so the comment now misstates the status; the genuine remaining obstacle ingaugeConsistencyis the cross-edge assembly step.
ℹ️ Advisory (non-blocking): the general operator-Schmidt lemmas (gauge_eq1/gauge_eq2/gauge_inv/exists_dual_isolating/bilinear_coeff_zero) are stated over abstract {K V1 V2} with no PEPS content and could be upstreamed/relocated — flagged earlier, acceptable here.
No paper-gap files are modified in this PR. Blueprint sync and prose quality are out of scope for this review (handled by the dedicated workflow).
🤖 Generated with Claude Code
There was a problem hiding this comment.
Blueprint ↔ Lean & Prose Review (synchronize)
Verdict: REQUEST_CHANGES. 1 new Category A finding · 1 new Category B finding · all prior unresolved threads remain open.
What this synchronize got right
post_absorption_edge_insertion_equalityis now sorry-free; the\begin{proof}\leanokat line 2069 is valid from A.2 (nosorryin that proof).two_injective_tensor_insertion_comparisonis now sorry-free; the\leanokon the proof is valid from A.2.- The rewritten proof sketch for
thm:peps_twoInjectiveTensorInsertionComparisonnow contains display equations — a substantial improvement over the previous word-only text. - The blueprint statement for
thm:peps_postAbsorptionEdgeInsertionEqualitycorrectly adds the positive-bond hypothesis to match the newhposparameter in the Lean signature.
New findings (this round)
Category A — 1 issue
| # | File | Lines | Issue |
|---|---|---|---|
| A1 | ch13a_peps_ft.tex |
2412–2413 | Proof \leanok for thm:peps_twoInjectiveTensorInsertionComparison has no \uses{}. The Lean proof calls two_injective_tensor_insertion_comparison_core and twoBlockReciprocalScalarProportional_of_isEmpty_config; both lack blueprint entries (prior threads), making \uses temporarily unpopulatable — but that means those entries must be added before this proof \leanok is admissible, not that \uses may be omitted. |
Category B — 1 issue
| # | File | Lines | Issue |
|---|---|---|---|
| B1 | ch13a_peps_ft.tex |
2072–2079 | Proof sketch for thm:peps_postAbsorptionEdgeInsertionEquality is entirely verbal; the key identity "$Z_e^\top = R(X_e)$, hence |
Prior unresolved threads (unchanged)
No previously raised threads are resolved by this synchronize. The following remain open and are not re-raised here:
PRRT_kwDORK8b986HkghT,PRRT_kwDORK8b986HkgqG,PRRT_kwDORK8b986HkglS,PRRT_kwDORK8b986Hkgn9,PRRT_kwDORK8b986Hkg0Y,PRRT_kwDORK8b986HkpBs,PRRT_kwDORK8b986HkpFp,PRRT_kwDORK8b986HkpIR,PRRT_kwDORK8b986HkpK1,PRRT_kwDORK8b986HkpNt,PRRT_kwDORK8b986HkpQo,PRRT_kwDORK8b986HkpUr— missing blueprint entries and Lean-identifier-in-prose issues inTwoInjectiveComparison.lean.PRRT_kwDORK8b986HlkVj,PRRT_kwDORK8b986HlkZ5,PRRT_kwDORK8b986HlkgP,PRRT_kwDORK8b986Hlkih,PRRT_kwDORK8b986HlklC,PRRT_kwDORK8b986Hlkqb,PRRT_kwDORK8b986HlkwL,PRRT_kwDORK8b986HlkyZ— missing blueprint entries and Lean-identifier-in-prose issues inFundamentalTheorem.lean.PRRT_kwDORK8b986HlMcy— word-only "equates the two fully contracted states" (the opening sentence of thethm:peps_twoInjectiveTensorInsertionComparisonproof still lacks the contraction equality).PRRT_kwDORK8b986HlMLN,PRRT_kwDORK8b986HlMTS,PRRT_kwDORK8b986HlMi2,PRRT_kwDORK8b986HlMrW,PRRT_kwDORK8b986HlMxO,PRRT_kwDORK8b986HlM37— Lean identifiers in new docstrings and missing blueprint entries inTwoInjectiveComparison.lean.PRRT_kwDORK8b986HljsF— grouped missing-entry thread at old blueprint line 2415.
Additionally, note that the comment at FundamentalTheorem.lean line 1390 ("two_injective_tensor_insertion_comparison, still sorry") is now stale — the sorry was removed. That comment should be deleted or updated.
| open-edge gauge action then conjugates each inserted matrix by the transpose | ||
| of the absorbed gauge, while the insertion-algebra transport conjugates by | ||
| $X_e$; the two conjugations agree because the absorbed gauge is the transpose | ||
| of $X_e$, giving the post-absorption insertion equality. |
There was a problem hiding this comment.
Category B — word-only proof sketch; display equation required (§ "Source-faithful terminology and formulas")
The open-edge gauge action then conjugates each inserted matrix by the transpose of the absorbed gauge, while the insertion-algebra transport conjugates by
$X_e$ ; the two conjugations agree because the absorbed gauge is the transpose of$X_e$ , giving the post-absorption insertion equality.
The entire proof block (lines 2069–2080) has no display equation. The claim that the two conjugation actions agree is the load-bearing step; it should be shown as an identity. The Lean proof establishes
where
Display at least one of these identities — the prose "the two conjugations agree because…" is a word-only description of a contraction/conjugation identity and must be replaced by the formula per the style guide.
| endomorphisms $Z$, $U$, and $W$ such that, for every external index | ||
| $\eta$, shared-boundary index $\mu$, and physical index $\sigma$ of the | ||
| first block, | ||
| \leanok |
There was a problem hiding this comment.
Category A — A.4: proof \leanok has no \uses{}
The \begin{proof}\leanok for thm:peps_twoInjectiveTensorInsertionComparison has no \uses{...} tag. The Lean proof of two_injective_tensor_insertion_comparison invokes exactly two dependencies:
two_injective_tensor_insertion_comparison_core— the nonempty-bond substantive case, andtwoBlockReciprocalScalarProportional_of_isEmpty_config— the vacuous empty-bond case.
Per A.4, the proof \uses must list the lemmas the Lean proof actually invokes. Both of these declarations currently lack blueprint entries (flagged in earlier threads), so \uses cannot be populated yet — but that makes adding the blueprint entries for those two declarations a prerequisite for marking this proof \leanok, not a reason to leave \uses empty. Once those entries exist the proof \uses must be:
\begin{proof}
\leanok
\uses{<label for two_injective_tensor_insertion_comparison_core>,
<label for twoBlockReciprocalScalarProportional_of_isEmpty_config>}
...
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361) (synchronize)
Verdict: REQUEST_CHANGES.
The 🔴 blocker from the prior review cycle (_core missing [Nonempty Bond]) is resolved, and the stale comments in gaugeConsistency have been updated. The proof of two_injective_tensor_insertion_comparison is now complete and mathematically correct. However, 🟡 issues from prior reviews remain unaddressed, and one new 🟡 modularity issue is found.
🟡 Mathlib naming — sameOpenBondContraction (TwoInjectiveComparison.lean, line 407)
This theorem is named in pure camelCase, reading like a def/predicate. The file's convention is snake_case for theorems (fullContraction_eq, twoBlockInsertedCoeff_one, two_injective_tensor_insertion_comparison_core). Rename to openBondContraction_of_sameInsertions or similar.
Previously flagged in discussion_r3367465505, discussion_r3367468153, discussion_r3367469662. Remains unresolved.
🟡 Documentation accuracy — "equivalent" vs "implies" (TwoInjectiveComparison.lean, line 398)
The docstring states "The per-bond insertion hypothesis is equivalent to equality of all one-leg-open contractions" but only the forward direction (SameTwoBlockInsertions → equality) is proved. Change to "implies" or "gives."
Previously flagged in discussion_r3367465290, discussion_r3367468163. Remains unresolved.
🟡 Performance/linter — unscoped maxHeartbeats (FundamentalTheorem.lean, lines 422–425)
The section LargeBudget + set_option maxHeartbeats 400000 triggers linter.style.setOption. Must use the per-declaration form set_option maxHeartbeats 400000 in before each of the two affected lemmas (prod_gaugeVertex_eq_sum_local, prod_gaugeVertex_eq_sum_local_open), matching the form already used elsewhere in this PR (e.g., TwoInjectiveComparison.lean line 1523).
Previously flagged in discussion_r3367469570. Remains unresolved.
🟡 Modularity — dead code: twoBlockLeftInverse/twoBlockComb unused (TwoInjectiveComparison.lean, lines 488–532)
twoBlockLeftInverse, twoBlockComb, twoBlockComb_injective, twoBlockLeftInverse_comp, and twoBlockLeftInverse_apply are not called by any theorem in this PR, nor anywhere else in the project (grep -r across all .lean files returns no hits outside this file). They were prepared for a left-inverse-based proof approach, but the final proof of two_injective_tensor_insertion_comparison_core uses exists_dual_isolating and the gauge equations instead.
Either remove these unused definitions or add a comment explaining they are infrastructure for the remaining gaugeConsistency work (to be used in a follow-up PR). New finding in this review cycle.
🟡 Modularity — general operator-Schmidt lemmas in PEPS file (TwoInjectiveComparison.lean, lines ~592–870)
exists_dual_isolating, gauge_eq1, gauge_eq2, gauge_inv, and bilinear_coeff_zero are stated over abstract {K V1 V2 : Type*} with no TwoBlockTensor or Bond content. They are generic linear-algebra results invisible to other modules. At minimum, add a sectioning comment marking them as general linear algebra.
Previously flagged in discussion_r3367467510, discussion_r3367468173, discussion_r3367469684. Remains unresolved.
✅ What was fixed since the previous review cycle
- 🔴
two_injective_tensor_insertion_comparison_corenow carries[Nonempty Bond]and the proof is complete — the blocking false-statement issue is resolved. - 🟡 Stale comments in
gaugeConsistency(previously referencing #1361 and #1364 as "stillsorry") have been updated to reflect the new state.
ℹ️ Advisory
- The
maxHeartbeats 400000inTwoInjectiveComparison.lean(line 1523) uses the correct per-declaration form with an explanatory comment. Acceptable. - The
sorryongaugeConsistencyis pre-existing and documented with precise remaining steps. Not introduced by this PR. - Blueprint sync and prose quality (Category A/B) are out of scope for this review; those are handled by the dedicated workflow.
🤖 Generated with Claude Code
|
@claude review |
|
Claude finished @LionSR's task —— View job
|
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361) (synchronize)
Verdict: APPROVE. All 🔴 and 🟡 issues from prior review cycles have been addressed in this push. The remaining unresolved threads are either ℹ️ advisory or concern blueprint/prose categories that are out of scope for this review (handled by the dedicated Blueprint Sync & Prose Review workflow).
What was resolved in this push
Every previously-flagged in-scope issue has been fixed:
- ✅ Mathlib naming —
sameOpenBondContractionrenamed toopenBondContraction_of_sameInsertions(TwoInjectiveComparison/Basic.lean:407). Followssnake_caseconvention for theorems. - ✅ Documentation accuracy — docstring now says "implies" rather than "is equivalent to" for the one-leg-open contraction theorem (line 398).
- ✅ Unscoped
maxHeartbeats— bareset_option maxHeartbeats 400000removed fromFundamentalTheorem.lean; the only remaining heartbeat raise is properly scoped (set_option maxHeartbeats 400000 in,Basic.lean:712). - ✅ Dead code — the
twoBlockComb/twoBlockLeftInversecluster removed. - ✅ Unused imports — removed from
GaugeAction.leanandVertexComplement/Basic.lean. - ✅ Modularity — sectioning comment added at
TwoInjectiveComparison/Basic.lean:528-534marking the general operator-Schmidt lemmas for eventual relocation toTNLean/Algebra/OperatorSchmidt.lean.
Build & integrity
lake build TNLean.PEPS.TwoInjectiveComparison TNLean.PEPS.VertexComplement.KernelDescent TNLean.PEPS.GaugeConsistencyConnectivityCounterexample→ 2668 jobs, 0 errors, 0 warnings- Two pre-existing
sorrys remain in the orphan capstoneFundamentalTheorem.lean(gaugeConsistencyat line 321,gauge_unique_mod_edge_scalarsat line 766), both documented with proof-status markers and tracked indocs/paper-gaps/. No newsorryoraxiomis introduced. #print axiomswould be clean for all new theorems.
What's solid
two_injective_tensor_insertion_comparison(#1361) is genuinely closed, sorry-free. Proof chain: operator-Schmidt uniqueness (exists_bondGauge_of_fullContraction) → per-bond master constraint (bondGauge_master_constraint) → scalar diagonality (bondGauge_scalar_of_master) → reciprocal proportionality. Faithful to arXiv:1804.04964, Section 3, Lemma inj_equal_tensors_2.bondDim_eq_of_matrixAlgEquivcorrectly discharges the bond-dimensionsorryinfundamentalTheorem_PEPS(#874): finrank ofM_n(ℂ)isn²,AlgEquivpreserves finrank,Nat.mul_self_injforces equality.VertexComplement/*kernel-descent architecture is sorry-free and correct, includingvertexComplementKernelCondition_empty_eq_zero(the priord=0false-positive has been re-examined and confirmed not a bug).GaugeConsistencyConnectivityCounterexampleis a valid, machine-checked refutation: empty graph onBool,A=(2,3), B=(6,1), states agree but no edge gauge relates them.- The paper-gap note
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.texis self-contained perpolicy.tex: states the assertion, isolates the obstruction, gives the witness, states the correct hypothesis, and distinguishes from the separatepeps_gauge_edge_scalarsgap.
ℹ️ Advisory (not blocking)
maxHeartbeats 400000onexists_bondGauge_of_fullContraction(Basic.lean:712) is aPROOF_INTEGRITY.mdwarning with inline justification (unifyingClassical-derivedFintypeinstances). Acceptable.glTransposeinEdgeGaugeFamily.leanis stated only forGL (Fin m) ℂ— clean upstreaming candidate, but not blocking.- Unresolved Category A/B threads (blueprint entries, prose quality, docstring style) are out of scope for this review; they should be resolved by the dedicated Blueprint Sync & Prose Review workflow before merge.
🤖 Generated with Claude Code
There was a problem hiding this comment.
Review (proof integrity, correctness, style, types, performance, modularity, documentation, paper-gap notes)
Scope note. Blueprint↔Lean sync (\lean/\leanok/\uses) and prose/banned-language review are handled by the dedicated Blueprint Sync & Prose Review workflow and are excluded here. Several existing claude threads fall under that exclusion; I have not re-raised or resolved them.
Verification performed
lake build TNLean.PEPS.TwoInjectiveComparison— succeeds.lake build TNLean.PEPS.FundamentalTheorem TNLean.PEPS.GaugeConsistencyConnectivityCounterexample TNLean.PEPS.VertexComplement.KernelDescent— succeeds; the onlysorrywarnings are the two pre-existing obligations atFundamentalTheorem.lean:302(gaugeConsistency) and:729(gauge_unique_mod_edge_scalars).#print axiomsontwo_injective_tensor_insertion_comparison,two_injective_tensor_insertion_comparison_core,bondGauge_master_constraint,bondGauge_scalar_of_master,one_vertex_complement_comparison— all[propext, Classical.choice, Quot.sound], nosorryAx.
Proof integrity 🔴 — clean
This PR removes 2 sorrys and introduces none (net 4 → 2 in FundamentalTheorem.lean). The two remaining sorrys are the pre-existing gaugeConsistency and gauge_unique_mod_edge_scalars, both acknowledged in the PR description, both carrying detailed docstrings with the elimination plan and paper-gap citations. Consistent with paper-realignment mode. The single set_option maxHeartbeats 400000 (on exists_bondGauge_of_fullContraction) is a PROOF_INTEGRITY.md warning, already noted in a prior advisory thread.
Proof correctness 🔴 — sound
The headline result two_injective_tensor_insertion_comparison is a faithful, genuinely structured operator-Schmidt uniqueness argument: exists_bondGauge_of_fullContraction (via gauge_eq1/gauge_eq2/gauge_inv) produces an invertible bond gauge g; bondGauge_master_constraint separates the one-leg-open identities over the two linearly independent families B₁, A₂ (bilinear_coeff_zero); bondGauge_scalar_of_master forces g = λ·1 with λ ≠ 0. The supporting Basic.lean definitions (IsTwoBlockInjective, SameTwoBlockInsertions, TwoBlockReciprocalScalarProportional) match arXiv:1804.04964 §3 Lemma inj_equal_tensors_2. The public statement is a faithful generalization (nonempty spectator boundaries; the paper's one-point case is recovered) — no source hypothesis is dropped, all four injectivity hypotheses are present.
Faithfulness of the added hypotheses — correctly handled
The PR adds G.Connected and hpos : ∀ e, 0 < A.bondDim e to gaugeConsistency/fundamentalTheorem_PEPS. This is the right handling of a genuine source gap, not a smuggled hypothesis: GaugeConsistencyConnectivityCounterexample machine-checks (axiom-clean) that the connectivity-free statement is false — empty graph on Bool, A=(2,3), B=(6,1), 2·3 = 6 = 6·1 but A₀ = 2 ≠ 6 = B₀. The deviation is documented in docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex, whose argument (oriented incidence product of edge scalars is 1 per component, so the λ_v are absorbable only when their reciprocal product is 1 per component) is mathematically correct, and the source citation paper_normal.tex:1207 is accurate.
Paper-gap notes 🟡 — reviewed against policy.tex
Both note changes are self-contained and faithful. One minor point inline on the connectivity note (quotation substitutes λ_v for the source's λ_i). The section3_route.tex addition is consistent with the note's established route-tracking style.
Remaining categories
Style, type safety, performance, modularity: no in-scope blockers. glTranspose upstreamability is already covered by a prior advisory thread.
Verdict
No blocking (🔴/🟡) issues within this review's scope. Two advisory items are noted inline. I am submitting as a comment rather than an approval because out-of-scope blueprint/prose threads from the sibling workflow remain open; this assessment covers only proof integrity, correctness, style, types, performance, modularity, documentation, and the paper-gap notes.
| after the equation labelled \path{eq:inj_equal_edge}: blocking one vertex against | ||
| its complement gives, for each vertex, a scalar proportionality | ||
| $A_v=\lambda_v\,\widetilde B_v$, and the source then says ``the constants | ||
| $\lambda_v$ can be incorporated into the gauge |
There was a problem hiding this comment.
ℹ️ Paper-gap note quotation (advisory). This sentence quotes the source as “the constants Papers/1804.04964/paper_normal.tex:1207 writes GaugeConsistencyConnectivityCounterexample and in gaugeConsistency.
There was a problem hiding this comment.
Review summary
Threads resolved (5)
| Thread | Fix |
|---|---|
PRRT_kwDORK8b986HmtxL |
Blueprint entry for vertexComplementTensorInjective_of_isVertexInjective now present (thm:peps_vertexComplementTensorInjective). |
PRRT_kwDORK8b986HmUeH |
"equivalent" → "implies" in openBondContraction_of_sameInsertions docstring. |
PRRT_kwDORK8b986Hmtpk |
def:peps_complementTwoBlock \uses{} no longer lists def:peps_vertexTwoBlock. |
PRRT_kwDORK8b986Hmts3 |
|
PRRT_kwDORK8b986Hmt0X |
"absolute-scalar specialization of twoBlockReciprocalScalarProportional" text is gone. |
Equivalence and status (Category A) — 1 new issue
blueprint line 2707 — \begin{proof}\leanok for thm:peps_isTwoBlockInjective_complementTwoBlock has no \uses{thm:peps_vertexComplementTensorInjective}, despite the Lean proof calling vertexComplementTensorInjective_of_isVertexInjective directly.
Prose quality (Category B) — 1 new issue
GaugeAction.lean lines 35–41 — paper-internal labels inj_isomorph, eq:inj_equal_edge, inj_equal_tensors_2 used as backtick shorthand in the module docstring. §1 requires full citations instead.
Carry-over issues still open (not re-raised)
All prior unresolved threads authored by claude that are not outdated remain open (see thread list). The most significant carry-overs:
- Category A: proof
\leanokforthm:peps_twoInjectiveTensorInsertionComparisonhas no\uses{}(threadsPRRT_kwDORK8b986Hluy1,PRRT_kwDORK8b986HmUh-); missing blueprint entries forbondGauge_master_constraint,bondGauge_scalar_of_master(PRRT_kwDORK8b986HlMxO); and several other missing entries for sorry-free internal lemmas (PRRT_kwDORK8b986HljsF). - Category B: "bridge" at
TwoInjectiveComparison/Basic.lean:496(PRRT_kwDORK8b986Hmi-A); "at the heart of" at line 726 (PRRT_kwDORK8b986Hmi_9); Lean identifiers in multiple docstrings (PRRT_kwDORK8b986HlMLN,PRRT_kwDORK8b986HmjC9,PRRT_kwDORK8b986HmjHm,PRRT_kwDORK8b986HlkwL); word-only proof sketches in the blueprint (PRRT_kwDORK8b986Hluwl,PRRT_kwDORK8b986HlzR1,PRRT_kwDORK8b986HlMcy).
Count: 1 new equivalence issue, 1 new prose issue.
| form a three-site injective MPS. Lemma `inj_isomorph` then assigns an edge gauge. | ||
| After repeating this for every edge and absorbing the gauges into the second | ||
| tensor family, the proof obtains the equality labelled `eq:inj_equal_edge`: | ||
| for every edge and every matrix `X`, inserting `X` on that edge in the first | ||
| PEPS gives the same state as inserting `X` on the same edge in the modified | ||
| second PEPS. Blocking one vertex against its complement and applying | ||
| `inj_equal_tensors_2` then gives $A_v = \lambda_v \cdot \tilde{B}_v$; the |
There was a problem hiding this comment.
Category B — §1 source-reference shorthand: paper-internal labels in module docstring prose
Lines 35–41 use paper-internal lemma and equation labels as backtick-quoted shorthand:
Lemma
`inj_isomorph`then assigns an edge gauge.
the proof obtains the equality labelled
`eq:inj_equal_edge`
Blocking one vertex against its complement and applying
`inj_equal_tensors_2`then gives…
Per docs/prose_style.md §1, source-reference shorthand such as "source label propsimple" is banned from docstrings. The identifiers inj_isomorph, eq:inj_equal_edge, and inj_equal_tensors_2 are internal labels from Papers/1804.04964/paper_normal.tex, not Lean declarations, but the same prohibition applies: they should be replaced by complete descriptions citing the source.
Fix: replace the three occurrences with prose citations, e.g.:
the injective-chain isomorphism lemma of arXiv:1804.04964, Section 3 (lines 1037–1065)
assigns an edge gauge.
After repeating this for every edge and absorbing the gauges, the proof obtains the
post-absorption insertion equality of arXiv:1804.04964, eq:inj_equal_edge.
Blocking one vertex against its complement and applying the two-injective comparison
(arXiv:1804.04964, Lemma inj_equal_tensors_2, lines 1068–1204) then gives
$A_v = \lambda_v \cdot \widetilde B_v$; the scalars $\lambda_v$ are absorbed into the edge gauges.
|
@claude review |
Introduce the oriented incidence product of an edge-scalar family on a simple graph (edgeScalarUnit / orientedIncidence) and prove the necessity direction of the absorption solvability condition: the product of the oriented incidences over all vertices is 1 (prod_orientedIncidence_eq_one), since each edge cancels its own scalar against its inverse across its two endpoints. This is the consistency obstruction recorded in docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex and the foundation for the spanning-tree edge-scalar existence step of gaugeConsistency.
Add the combinatorial infrastructure for the induction step of the spanning-tree
edge-scalar existence proof: lift/restrict edges between G and G.induce {v0}ᶜ
(liftEdge / restrictEdge), the incidence bijection incEquiv between v0-avoiding
incident edges of a vertex w in G and the incident edges of w in the deleted
subgraph, and prod_free_eq showing the v0-free part of w's oriented incidence
product equals the deleted-subgraph oriented incidence of the lifted scalars.
These are the load-bearing helpers for the vertex-deletion recursion of
gaugeConsistency's absorption step.
Prove exists_edgeScalars_of_connected: on a connected simple graph, any
vertex-scalar family t : V → ℂˣ with ∏ t = 1 is the oriented incidence product
of an edge-scalar family. This is the spanning-tree coboundary step of the
absorption argument in the injective PEPS Fundamental Theorem
(arXiv:1804.04964 §3), documented in
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex.
The proof is by induction on the number of vertices, removing a non-cut vertex
v₀ (SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial),
folding v₀'s target into a neighbor, recursing on the deleted subgraph, and
absorbing v₀'s scalar into the single edge {v₀,w₀}. Axiom-clean
(propext, Classical.choice, Quot.sound).
…tency Add two sorry-free lemmas toward closing gaugeConsistency: - isVertexInjective_reindexTensor: bond-dimension reindexing preserves vertex injectivity (the local family precomposed with an injective index recast). - perVertexScalar: at every vertex with a nonempty incident-edge set, the post-absorption edge-insertion equality plus the four two-block injectivity facts and one_vertex_complement_comparison yield a nonzero c with A_v = c · gaugeVertex B Z v. This realizes the per-vertex scalar step of arXiv:1804.04964 §3 documented in docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex. gaugeConsistency itself remains sorry pending the gauge-inversion / edge-scalar assembly.
Update the gaugeConsistency proof-status comment to reference the now-available perVertexScalar and exists_edgeScalars_of_connected, and to name the two remaining obligations precisely: (1) ∏ c_v = 1 via gauge-state invariance, and (2) the gauge-inversion product-kernel collapse packaging X_e = s_e·(Z_e)⁻¹.
|
Claude finished @LionSR's task in 5m 43s —— View job Review:
|
|
@claude review |
There was a problem hiding this comment.
Review Summary — PR #2406
feat(peps): close two_injective_tensor_insertion_comparison (#1361)
This review covers 15 changed files (+5243/−871) across the PEPS capstone, gauge pipeline, connectivity counterexample, and the operator-Schmidt comparison. The review is conducted under the code-review categories listed in the PR instructions; blueprint-sync and prose-quality issues are excluded (handled by the dedicated workflow).
Per-category findings
🔴 Proof integrity (no issues found)
- No
sorry,axiom,native_decide, orunsafeCastappear in the diff. The two remainingsorrys —gaugeConsistencyandgauge_unique_mod_edge_scalars— are pre-existing, documented in the PR body, and tracked indocs/paper-gaps/peps_injective_ft_section3_route.tex. This is acceptable under paper-realignment mode.
🔴 Proof correctness (no issues found)
exists_edgeScalars_auxinEdgeScalarSolve.leanis a clean induction on|V|with a spanning-tree coboundary construction. The identitystepAcorrectly handles the transitive evaluation oft''s product.post_absorption_edge_insertion_equalitychainsexists_edgeGaugeFamily→hΦcoeff/hΦconj→edgeInsertedCoeff_applyGaugecorrectly; the reindex-transpose lemmas (hZt,hZit) close the matrix-level equality.exists_bondGauge_of_fullContractioninTwoInjectiveComparison/Basic.leaninstantiatesgauge_eq1/gauge_eq2/gauge_invwith the config-indexed linear independence fromhA₁.config_linearIndependentet al., producing the invertible bond gauge. The operator-Schmidt uniqueness argument is correctly translated to the abstract two-block setting.- The connectivity counterexample in
GaugeConsistencyConnectivityCounterexample.leanis mathematically correct: the empty graph on two vertices withA=(2,3),B=(6,1)satisfiesSameState(both products are 6), vertex injectivity, and vacuous positivity, yetgaugeConsistencyfails becauseA₀=2≠6=B₀.
🔴 Type safety (no issues found)
- No universe polymorphism issues or missing
DecidableEq/Fintypeinstances. Type coercions throughFin.cast,glReindex,finCongr, andMatrix.reindexAlgEquivare correctly threaded.
🟡 Mathlib style (acceptable)
- Naming follows conventions (
camelCasefor defs,snake_casefor theorems). The handful ofv0Inc_*lemma names mix the predicate identifierv0Inc(camelCase) into theorem names — not a linter violation but slightly inconsistent. No action required.
🟡 Performance (acceptable)
set_option maxHeartbeats 400000atTwoInjectiveComparison/Basic.leanline 712 is correctly scoped toexists_bondGauge_of_fullContractionviaset_option … inchained withopen scoped Classical in. The raise is explained by the four noncomputableFintypeunifications acrossgauge_eq1/gauge_eq2calls. No timeout risk.- No
decideon large types, no unboundedsimpsets.
🟡 Modularity & duplication (acceptable)
- General linear-algebra lemmas (
exists_dual_isolating,gauge_eq1,gauge_eq2,gauge_inv) inTwoInjectiveComparison/Basic.leancarry docstring notes acknowledging they belong inTNLean/Algebra/OperatorSchmidt.lean. glTransposeandreindexAlgEquiv_transposeinEdgeGaugeFamily.leanare smallGL/matrix utility lemmas that could be upstreamed, but their local placement is acceptable for now.
🟡 Documentation — one issue (must fix)
⚠️ vcExtraIndicator_split(VertexComplement/KernelDescent.leanline 169) is the one new top-level theorem in this PR that lacks a/--docstring. All new declarations should carry docstrings. An inline comment has been posted with the suggested content. This must be fixed before approval.
🟡 Paper-gap notes (acceptable)
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex(new) followsdocs/paper-gaps/policy.tex: it states the assertion, isolates the obstruction (oriented incidence product forces product 1 per component), gives a concrete counterexample with machine-checked refutation, identifies the correct hypothesis (G.Connected), and states what is established vs. remaining. The constructionA₂,B₂is explicit and checked in Lean. The note is self-contained for a mathematical reader.docs/paper-gaps/peps_injective_ft_section3_route.tex(+19 lines) updates the remaining-obligations ledger to reflect newly proved results (post_absorption_edge_insertion_equality,perVertexScalar,two_injective_tensor_insertion_comparison) without altering the mathematical accounting.
Verdict: REQUEST_CHANGES
One 🟡 issue must be fixed:
- Add a
/--docstring tovcExtraIndicator_splitinTNLean/PEPS/VertexComplement/KernelDescent.lean.
This is a well-structured, mathematically careful PR. The new EdgeScalarSolve.lean provides a clean combinatorial lemma; the file splits improve modularity; and the connectivity counterexample gives an attested fix for a faithfulness gap. Once the missing docstring is added, this is ready to merge.
🤖 Generated with Claude Code
Follow-up to the
|
|
@claude review |
|
@claude review |
|
Claude finished @LionSR's task in 4m 55s —— View job Review:
|
There was a problem hiding this comment.
Review summary — APPROVE
I reviewed this PR against the in-scope categories (proof integrity, proof correctness, Mathlib style, type safety, performance, modularity, documentation, and paper-gap notes). Blueprint ↔ Lean sync and prose/banned-language checks are excluded here per the dedicated Blueprint Sync & Prose Review workflow.
Proof integrity 🔴 — clean
- The diff introduces zero new
sorry/admit/axiom/native_decideand in fact removes threesorrys (the previously-open proof oftwo_injective_tensor_insertion_comparison). - The two
sorrys remaining inTNLean/PEPS/FundamentalTheorem.lean(gaugeConsistencyat line 401,gauge_unique_mod_edge_scalarsat line 846) are pre-existing assembly obligations, unchanged by this PR, explicitly disclaimed in the PR body and documented indocs/paper-gaps/peps_injective_ft_section3_route.texanddocs/paper-gaps/peps_gauge_edge_scalars.tex. Acceptable under CLAUDE.md paper-realignment mode. - The one
set_option maxHeartbeats 400000(exists_bondGauge_of_fullContraction,TwoInjectiveComparison/Basic.lean:712) is adocs/PROOF_INTEGRITY.mdwarning, not a blocker, and carries an inline justification.
Proof correctness 🔴 — verified by compilation
The three genuinely new proof files compile cleanly under lake env lean (exit 0 each):
TNLean/PEPS/EdgeScalarSolve.lean— the spanning-tree coboundary / edge-scalar solve. The orientation convention inedgeScalarUnit(scalars eat the lower endpoint,(s e)⁻¹at the upper) is consistent across the necessity direction (prod_orientedIncidence_eq_one, cancelling each edge against its inverse over its two endpoints viaprod_incVertex_endpoint) and the existence direction (exists_edgeScalars_auxby strong induction onFintype.card V, deleting a vertex whose removal preserves connectivity). The base case correctly forcest v = 1from∏ t = 1on a subsingleton.TNLean/PEPS/VertexComplement/KernelDescent.lean— the star-boundary kernel descent establishingVertexComplementTensorInjective.TNLean/PEPS/GaugeConsistencyConnectivityCounterexample.lean— a Lean-checked refutation of the connectivity-free statements.
Faithfulness of the new connectivity hypothesis — exemplary
Adding hconn : G.Connected to gaugeConsistency (threaded into fundamentalTheorem_PEPS) is a hypothesis-strengthening change, which CLAUDE.md's faithfulness rule requires to be documented. It is handled correctly: GaugeConsistencyConnectivityCounterexample.lean proves that the connectivity-free statement is false (empty graph on two vertices, A₀A₁ = 6 = B₀B₁ but A₀ = 2 ≠ 6 = B₀), so the added hypothesis is the source's implicit assumption rather than a smuggled-in restriction. The witness keeps positivity to isolate connectivity as the missing assumption.
Paper-gap notes 🟡 — pass against docs/paper-gaps/policy.tex
peps_gaugeConsistency_connectivity_gap.texis self-contained: it states the cited assertion (paper_normal.tex:1207, "the constants λ can be incorporated into the gauge transformations"), isolates the structural obstruction (oriented incidence products have per-component product 1), gives a concrete witness, and renders a clear verdict (add a connectivity hypothesis; existence-vs-uniqueness gap distinguished frompeps_gauge_edge_scalars.tex). The note's substitution ofλ_vfor the source'sλ_iis a harmless notational alignment (already flagged advisory in a prior thread).- The
peps_injective_ft_section3_route.texaddition is a coherent ledger item recording the now-formalized vertex-complement injectivity block.
Documentation 🟡 — resolved
The previous review cycle's in-scope documentation findings (missing docstrings on prod_incident_eq_prod_edge, gauge_sum_left_right_matrix_inv, and vcExtraIndicator_split) were addressed by the recent doc(peps) commits; I resolved those three threads.
Remaining open threads — out of scope here
All other unresolved threads are Category A (blueprint sync) and Category B (prose / Lean-identifiers-in-docstrings), which belong to the Blueprint Sync & Prose Review workflow and are not evaluated here.
Advisory (non-blocking)
EdgeScalarSolve.lean:227v0Inc_subsingletonis declaredinstancebut cannot be synthesized (explicithwhypothesis); it is only used explicitly. Prefer a plaintheorem. Inline comment posted.EdgeGaugeFamily.lean:59glTransposeisℂ/Fin m-specific but field- and index-agnostic; a candidate for generalization/upstreaming (prior advisory thread).
No in-scope 🔴 or 🟡 issues remain outstanding. Approving.
|
|
||
| /-- The edges of `G` incident to both `w` and `v₀` (with `w ≠ v₀`) form a | ||
| subsingleton. -/ | ||
| instance v0Inc_subsingleton (v₀ w : V) (hw : w ≠ v₀) : |
There was a problem hiding this comment.
ℹ️ Advisory (Mathlib style — instance keyword on a non-synthesizable declaration).
v0Inc_subsingleton is declared as an instance, but its explicit hypothesis hw : w ≠ v₀ cannot be supplied by typeclass synthesis, so this instance can never fire during resolution. The single use site (line 295) already invokes it explicitly: have : Subsingleton ... := v0Inc_subsingleton (G := G) v₀ w₀ hw₀ne. Since it is only ever applied by hand, prefer a theorem/lemma returning Subsingleton {ie : IncidentEdge G w // v0Inc v₀ ie.1} over instance, to avoid registering a never-matching candidate in the instance cache.
Non-blocking; correctness is unaffected.
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361) (synchronize)
Verdict: APPROVE. No 🔴 or 🟡 issues remain that must block merge.
Scope: proof integrity, correctness, Mathlib style, type safety, performance, modularity, documentation, paper-gap notes. (Blueprint sync and prose quality are handled by the dedicated workflow.)
What was reviewed
This is a stacked PR (#2403→this) that closes two_injective_tensor_insertion_comparison (the generalized two-injective comparison, core of #1361) and modularizes the PEPS Fundamental Theorem into GaugeAction, EdgeInsertion, and OneVertexComparison. The PR adds 5250 lines and deletes 871 across 15 files. I built every changed module locally.
🔴 Proof integrity
The two remaining sorry markers (gaugeConsistency at FundamentalTheorem.lean:1451, gauge_unique_mod_edge_scalars at FundamentalTheorem.lean:825) are pre-existing obligations, explicitly documented in docs/paper-gaps/peps_injective_ft_section3_route.tex, and not claimed by this PR. Each carries a proof-status docstring listing the remaining assembly steps. No axiom, admit, native_decide, unsafeCast, or circular reasoning is present.
🔴 Proof correctness
All new sorry-free theorems are mathematically sound:
-
two_injective_tensor_insertion_comparison_core(TwoInjectiveComparison.lean:4390) — follows the operator-Schmidt route ofdocs/paper-gaps/peps_injective_ft_section3_route.tex: the fully contracted identityfullContraction_eqsupplies a bond gauge viaexists_bondGauge_of_fullContraction, the one-leg-open identitiesopenBondContraction_of_sameInsertionsforce the master per-bond constraintbondGauge_master_constraint, and iterating that constraint forcesgto be a nonzero scalar multiple of the identity (bondGauge_scalar_of_master). The empty-config vacuous case is handled bytwoBlockReciprocalScalarProportional_of_isEmpty_config. The main theoremtwo_injective_tensor_insertion_comparisondispatches to these two cases. -
exists_edgeScalars_of_connected(EdgeScalarSolve.lean:570) — spanning-tree coboundary proof by induction onFintype.card V. The base case (card < 2, at most one vertex) is handled by the product-one condition. The induction step removes one vertexv₀whose deletion keeps the graph connected, sets the scalar on{v₀, w₀}to absorb the product discrepancy, and assembles the edge-scalar family from the induction hypothesis on the vertex-deleted subgraph. The necessity directionprod_orientedIncidence_eq_oneconfirms the product-one condition is exactly the solvability criterion. -
post_absorption_edge_insertion_equality(FundamentalTheorem.lean:1289) — obtains edge gauges fromexists_edgeGaugeFamily, reindexes and transposes them to matchB's bond spaces, and appliesedgeInsertedCoeff_applyGaugefor the open-edge conjugation. -
bondDim_eq_of_matrixAlgEquiv(FundamentalTheorem.lean:1485) — standard dimension-count viaModule.finrank. Correctly dispatches the bond-dimension equality previously gated bysorryinfundamentalTheorem_PEPS. -
vertexComplementTensorInjective_of_isVertexInjective(VertexComplement/KernelDescent.lean) — finite kernel descent adapted to the vertex star. ThevertexComplementKernelCondition_empty_eq_zeroproof's derivation ofNonempty (Fin d)fromIsVertexInjectiveis sound: ifFin dwere empty,Fin d → ℂis a subsingleton, soA.component v η₀ ≠ 0(fromLinearIndependent.ne_zero) would be contradictory.
🟡 Mathlib style
Naming follows conventions: snake_case for theorems (bondDim_eq_of_matrixAlgEquiv, prod_orientedIncidence_eq_one), camelCase for definitions (glTranspose, edgeScalarUnit). The previously-flaggged private lemmas gauge_sum_left_right_matrix_inv and prod_incident_eq_prod_edge now carry docstrings as promoted lemmas.
🟡 Performance
set_option maxHeartbeats 400000 in on exists_bondGauge_of_fullContraction (TwoInjectiveComparison/Basic.lean:5242) is properly scoped with in and carries an explanatory comment about the noncomputable Fintype instance. The linter should not flag it.
🟡 Modularity
General lemmas (glTranspose, linindep_recombine, piProductKernel_mul, piProductKernel_isUnit, bilinear_coeff_zero, reindex_update) remain in PEPS application files with docstring notes suggesting future upstreaming to Algebra/ modules. This is acceptable for now; these are well-isolated and their current locations match the import graph.
🟡 Documentation
All new top-level declarations carry docstrings. The file-split modules (GaugeAction.lean, EdgeInsertion.lean, OneVertexComparison.lean, VertexComplement/Basic.lean, VertexComplement/KernelDescent.lean, EdgeScalarSolve.lean, GaugeConsistencyConnectivityCounterexample.lean) each have module-level doc comments explaining their mathematical role and paper source.
🟡 Paper-gap notes
The new note docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex is self-contained: it introduces notation, states the source assertion (arXiv:1804.04964, line 1207), isolates the connectivity obstruction, provides a concrete machine-checked counterexample (empty graph on two vertices, 2·3=6=6·1 but 6≠2), gives the correct hypothesis (G.Connected), and distinguishes this existence gap from the balanced-edge-scalar uniqueness gap of peps_gauge_edge_scalars.tex. The prose is mathematical, not implementation-diary.
The update to docs/paper-gaps/peps_injective_ft_section3_route.tex adds a status entry documenting the vertex-complement injectivity infrastructure and accurately states what remains (the coefficient identity feeding one-bond insertions into the abstract comparison).
ℹ️ Advisory (import hygiene)
Mathlib.Combinatorics.SimpleGraph.Acyclic is imported in TNLean/PEPS/EdgeScalarSolve.lean but no lemma or definition from that module appears to be used in the file body. If the lemma exists_connected_induce_compl_singleton_of_finite_nontrivial is defined in Acyclic rather than Connected, the import is needed; otherwise it may be a stale leftover. Worth a quick check but not a merge blocker.
There was a problem hiding this comment.
Review: feat(peps): close two_injective_tensor_insertion_comparison (#1361) (synchronize)
Verdict: REQUEST_CHANGES — three newly-introduced 🟡 Mathlib-style build warnings. The mathematics is sound and the headline result (two_injective_tensor_insertion_comparison, closing #1361) is genuinely proved. The three issues below are small mechanical fixes.
Scope
Proof integrity, proof correctness, Mathlib style, type safety, performance, modularity, documentation, and paper-gap notes. Blueprint ↔ Lean \lean{}/\leanok/\uses{} sync and prose quality are out of scope (handled by the dedicated Blueprint Sync & Prose Review workflow).
Build & integrity — verified
lake build TNLean.PEPS.TwoInjectiveComparison TNLean.PEPS.FundamentalTheorem TNLean.PEPS.VertexComplement.KernelDescent TNLean.PEPS.EdgeScalarSolve TNLean.PEPS.GaugeConsistencyConnectivityCounterexample → Build completed successfully (2701 jobs).
- Net −2
sorry: the base branchfeat/peps-gaugeconsistencycarried 4sorrys in changed files; this PR removestwo_injective_tensor_insertion_comparison(#1361,lem:inj_equal_tensors_2, arXiv:1804.04964 lines 1067–1204) andpost_absorption_edge_insertion_equality, leaving only the pre-existinggaugeConsistencyandgauge_unique_mod_edge_scalars(both documented indocs/paper-gaps/peps_injective_ft_section3_route.tex). - No new
sorryoraxiomis introduced. - The
Nonempty (Fin d)derivation invertexComplementKernelCondition_empty_eq_zero(KernelDescent.lean:344) — previously flagged and re-reviewed as a false positive — is indeed sound:IsVertexInjectivegives a nonzero component inFin d → ℂ, and an emptyFin dwould make that space a unit type, contradicting the nonzero.
🔴 Proof integrity & correctness — OK
two_injective_tensor_insertion_comparisonfollows the operator-Schmidt route: fully contracted equality → bond gauge → master per-bond constraint → scalar diagonal form →A₁ = λ·B₁,A₂ = λ⁻¹·B₂. The proof structure matches the paper-gap analysis.EdgeScalarSolve(exists_edgeScalars_of_connected) is a clean induction onFintype.card V, handling edge transfer through vertex deletion and oriented incidence products.GaugeConsistencyConnectivityCounterexampleis a tight refutation: the empty graph on two vertices with scalar tensorsA=(2,3),B=(6,1)satisfies all hypotheses except connectivity, yet no gauge equivalence exists.VertexComplement/KernelDescentuses a finite descent (erase one complement vertex at a time) with a clear factorization of the exposed indicator.
🟡 Mathlib style — must fix (3 issues)
-
linter.style.showinEdgeScalarSolve.lean:368,371,374—showis used to change the goal;changemust be used instead per Mathlib convention. Three occurrences in theunit_at_w0proof. -
linter.unusedSectionVars+linter.unusedFintypeInTypeinFundamentalTheorem.lean:281,285—isVertexInjective_reindexTensorautomatically includes[Fintype V]from the sectionvariableblock. Other theorems in the same file already useomit [Fintype V] into suppress this. The fix is to addomit [Fintype V] inbefore the theorem. -
Unused import in
FundamentalTheorem/GaugeAction.lean:3—TNLean.PEPS.EdgeGaugeFamilyis imported but no symbol from it (glTranspose,exists_edgeGaugeFamily, etc.) is referenced in the file body.
ℹ️ Advisory (non-blocking)
set_option maxHeartbeats 400000 inonexists_bondGauge_of_fullContraction(TwoInjectiveComparison/Basic.lean:712) — properly scoped within, acceptable per Mathlib conventions.glTransposeinEdgeGaugeFamily.lean:59— specialized toFin moverℂ; appropriate for the PEPS domain.- Two pre-existing
sorrysites inFundamentalTheorem.lean(gaugeConsistencyat line 371,gauge_unique_mod_edge_scalarsat line 809) — both documented in paper-gap notes and not claimed closed by this PR.
Resolved from prior cycles
The following issues from previous review cycles have been correctly addressed in this push or earlier pushes on this branch:
sameOpenBondContractionrenamed toopenBondContraction_of_sameInsertions(naming convention) ✓- Unscoped
maxHeartbeatsinFundamentalTheorem.leanremoved ✓ - Unused imports
TwoInjectiveComparisonandKernelDescentinGaugeAction.leanremoved ✓ - Unused import
TwoInjectiveComparisoninVertexComplement/Basic.leanremoved ✓ - "equivalent" → "implies" docstring accuracy fix ✓
- Dead-code cluster (
twoBlockComb,twoBlockLeftInverse, etc.) removed ✓ glTranspose/glTranspose_inv_coeadded for transpose-of-gauge conjugation ✓
Mathematics assessment
The mathematical content of this PR is substantial and correct. two_injective_tensor_insertion_comparison (arXiv:1804.04964, Lemma inj_equal_tensors_2) is now fully proved in Lean, and the proof route matches the source paper's operator-Schmidt uniqueness argument. The EdgeScalarSolve development (exists_edgeScalars_of_connected) resolves the spanning-tree coboundary step recorded in docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex, and the counterexample file confirms that connectivity is genuinely required for gaugeConsistency and fundamentalTheorem_PEPS. The new paper-gap note peps_gaugeConsistency_connectivity_gap.tex is self-contained, notationally clear, and follows docs/paper-gaps/policy.tex.
| edgeScalarUnit (G := G) s w₀ ⟨edge0 (G := G) v₀ w₀ hadj, hinc⟩ = (t v₀)⁻¹ := by | ||
| have hne : v₀ ≠ w₀ := G.ne_of_adj hadj | ||
| rw [edgeScalarUnit, hs0] | ||
| show (if (edge0 (G := G) v₀ w₀ hadj).1.1 = w₀ then _ else _) = (t v₀)⁻¹ |
There was a problem hiding this comment.
🟡 Mathlib style — show used where change is required.
The show tactic here changes the goal rather than describing it for readability. The Mathlib linter linter.style.show requires change in these cases.
| show (if (edge0 (G := G) v₀ w₀ hadj).1.1 = w₀ then _ else _) = (t v₀)⁻¹ | |
| change (if (edge0 (G := G) v₀ w₀ hadj).1.1 = w₀ then _ else _) = (t v₀)⁻¹ |
Same issue applies at the next two show calls (current lines 371 and 374 in the inner have blocks). Replace all three show calls with change.
| injectivity: the local coefficient family of the reindexed tensor is the | ||
| original family precomposed with the bondwise index recast, an injective | ||
| reindexing of the configuration type. -/ | ||
| theorem isVertexInjective_reindexTensor (B : Tensor G d) {bd : Edge G → ℕ} |
There was a problem hiding this comment.
🟡 Mathlib style — unused section variable triggers linter.unusedSectionVars and linter.unusedFintypeInType.
The theorem isVertexInjective_reindexTensor automatically includes [Fintype V] from the section variable block at line 32, but the linter cannot see that IsVertexInjective (which appears in the conclusion) transitively requires it. Other theorems in this file already use omit [Fintype V] in to suppress this warning (e.g., lines 173, 186, 521, 535, 549).
Fix: Add omit [Fintype V] in before the theorem:
| theorem isVertexInjective_reindexTensor (B : Tensor G d) {bd : Edge G → ℕ} | |
| omit [Fintype V] in | |
| theorem isVertexInjective_reindexTensor (B : Tensor G d) {bd : Edge G → ℕ} |
This is the standard Mathlib idiom when section typeclasses are needed only in the proof body, not in the statement's explicit argument list.
| @@ -0,0 +1,934 @@ | |||
| import TNLean.PEPS.Blocking | |||
| import TNLean.PEPS.InsertionAlgebra | |||
| import TNLean.PEPS.EdgeGaugeFamily | |||
There was a problem hiding this comment.
🟡 Mathlib style — unused import.
TNLean.PEPS.EdgeGaugeFamily is imported but no symbol from it is used in this file. The file references edgeGaugeAt, edgeLeftIncident, edgeRightIncident (from LocalGauge), edgeInsertedCoeff (from InsertionAlgebra), and GL/matrix operations (from Mathlib). No glTranspose, reindexAlgEquiv_finCongr_symm_round, exists_edgeGaugeFamily, or any other EdgeGaugeFamily symbol appears in the file body beyond the import line itself.
Remove this import line.
There was a problem hiding this comment.
Review — feat(peps): close two_injective_tensor_insertion_comparison (#1361)
Scope: proof integrity, proof correctness, Mathlib style, type safety, performance, modularity, documentation, and the in-scope paper-gap notes. Blueprint↔Lean tag sync and prose/banned-term review of .tex/Lean docstrings are handled by the dedicated Blueprint Sync & Prose Review workflow and are excluded here (this exclusion does not cover the paper-gap notes, which I reviewed below).
Proof integrity 🔴 — clean
No new sorry/admit/axiom/native_decide. This PR reduces the sorry count in TNLean/PEPS/FundamentalTheorem.lean from 4 (base feat/peps-gaugeconsistency) to 2. The two remaining (gaugeConsistency, line 401, and gauge_unique_mod_edge_scalars, line 846) are pre-existing assembly obligations, each source-cited (arXiv:1804.04964 §3) and referred to docs/paper-gaps/peps_injective_ft_section3_route.tex / peps_gauge_edge_scalars.tex, consistent with paper-realignment mode. The bond-dimension equality previously left as sorry is now discharged via bondDim_eq_of_matrixAlgEquiv. The set_option maxHeartbeats 400000 on exists_bondGauge_of_fullContraction (TwoInjectiveComparison/Basic.lean:712) is a PROOF_INTEGRITY.md warning, justified inline (sharing the Classical-derived Fintype (SharedBondConfig …) across four extraction calls) and acceptable.
Proof correctness 🔴 — sound
The operator-Schmidt route for two_injective_tensor_insertion_comparison is logically sound. The empty-bond/empty-config edge case that a prior reviewer found false (twoBlockReciprocalScalarProportional with empty Bond) is correctly handled: bondGauge_scalar_of_master carries [Nonempty (SharedBondConfig bondDim)] (load-bearing, used to produce a nonzero lam), and the public theorem case-splits on Nonempty (SharedBondConfig bondDim), routing the vacuous side to twoBlockReciprocalScalarProportional_of_isEmpty_config. The scope-stronger twoBlockReciprocalScalarProportional_of_pointwise_mul_eq is confined to the single-shared-bond path and carries a **Scope restriction** marker. No dangling hypotheses in bondGauge_master_constraint, _core, or exists_bondGauge_of_fullContraction. The GaugeConsistencyConnectivityCounterexample arithmetic (gaugeConsistency conclusion (statement shape matches FundamentalTheorem.lean:377-380), not a strawman. The EdgeScalarSolve necessity (prod_orientedIncidence_eq_one) and the spanning-tree sufficiency induction (reusing Mathlib's Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial) are correct. The vertex-complement kernel-descent chain is sound. All files build.
Type safety 🔴 — no issues
Fin.cast/finCongr/reindexAlgEquiv transports across bond-dimension equalities are direction-correct; Subsingleton.elim on ℕ-equality proofs is legitimate proof irrelevance; Fintype/DecidableEq instances synthesize.
Mathlib style 🟡 — must address before approval
- Redundant
Fintypeinstance —instFintypeVertexComplementPhysicalConfig(VertexComplement/Basic.lean:78), inline comment posted.inferInstanceover a reducibleabbrevPi type that already synthesizes itsFintype; recommend deletion or an inline justification. instancethat can never fire —v0Inc_subsingleton(EdgeScalarSolve.lean:227) is declaredinstancebut carries an explicithw : w ≠ v₀that typeclass synthesis cannot supply, and is only ever applied explicitly (line 295). It should be atheorem/def. This was already raised in an unresolved review thread and has not been addressed in the latest push; flagging that it remains open.
Performance 🟡 / Modularity ℹ️
No timeout risks beyond the single justified maxHeartbeats override. Advisory upstreaming/dedup, non-blocking: glTranspose (EdgeGaugeFamily.lean:59) generalizes verbatim to GL n R over any CommRing and is a clean Mathlib candidate; the delta-collapse + reindex-to-doubled boilerplate is repeated across GaugeAction.lean:835, EdgeInsertion.lean:80, OneVertexComparison.lean:313 and could share a helper.
Paper-gap notes (in scope, reviewed against docs/paper-gaps/policy.tex)
Both changed notes are self-contained mathematical accounts. peps_gaugeConsistency_connectivity_gap.tex states the assertion, isolates the obstruction (oriented-incidence product is 1 per connected component, so the reciprocal vertex-scalar family is absorbable only when its per-component product is 1), gives a concrete machine-checked witness, and gives a clear verdict that G.Connected is the faithful repair. The new obligation item in peps_injective_ft_section3_route.tex is accurate; all cited Lean declarations exist.
One citation issue (already raised, still unresolved): the connectivity-gap note quotes the source as “the constants Papers/1804.04964/paper_normal.tex:1207 writes
Verdict
REQUEST_CHANGES. The mathematics is strong: the capstone lemma is closed without new sorry, the connectivity-gap reasoning is correct and well-documented, and the proofs are sound and type-safe. The only blockers are the two minor-but-genuine Mathlib-style instance-keyword issues above (one new, one pre-existing-unaddressed), plus the still-open paper-gap quotation fix. All are mechanical; once resolved this is ready to approve.
|
|
||
| instance instFintypeVertexComplementPhysicalConfig (v : V) : | ||
| Fintype (VertexComplementPhysicalConfig (V := V) (d := d) v) := |
There was a problem hiding this comment.
🟡 Mathlib style — redundant Fintype instance.
instFintypeVertexComplementPhysicalConfig is declared as an instance whose body is inferInstance, but VertexComplementPhysicalConfig v is the reducible abbrev (w : {w : V // w ≠ v}) → Fin d. Typeclass synthesis already produces its Fintype directly via Pi.fintype (the subtype {w // w ≠ v} is a Fintype with DecidableEq, and Fin d is a Fintype). The explicit declaration adds a second, definitionally-identical candidate to synthesis without providing anything inferInstance would not already find at every use site.
Recommend deleting the instance. If it was added to work around a synthesis failure or to pin a specific term, please document that reason inline so the redundancy is justified. Minor, but should be resolved before merge.
There was a problem hiding this comment.
Synchronize review — PR #2406
Resolved this cycle
PRRT_kwDORK8b986Hm24K(resolved): The proof block ofthm:peps_isTwoBlockInjective_complementTwoBlocknow correctly carries\uses{thm:peps_vertexComplementTensorInjective}. Resolved.
Prior unresolved threads still open
The following threads from earlier review cycles were not addressed in this synchronize and remain open:
| Thread | Issue |
|---|---|
PRRT_kwDORK8b986HljsF |
Missing blueprint entries for sorry-free theorems in TwoInjectiveComparison/Basic.lean |
PRRT_kwDORK8b986HlMcy |
Word-only contraction identity in proof of thm:peps_twoInjectiveTensorInsertionComparison (line 2585) |
PRRT_kwDORK8b986Hluwl |
Word-only proof sketch |
PRRT_kwDORK8b986Hluy1 |
Proof \leanok with no \uses{} block |
PRRT_kwDORK8b986HlzR1 |
Word-only conjugation identity in proof of thm:peps_postAbsorptionEdgeInsertionEquality (line 2237) |
PRRT_kwDORK8b986HmUh- |
Proof \leanok with no \uses{} block |
PRRT_kwDORK8b986HmjF8 |
Word-only proof sketch; conjugation identity (line 2237) |
PRRT_kwDORK8b986Hm26j |
Source-reference shorthand in GaugeAction.lean module docstring |
PRRT_kwDORK8b986HmdeO |
Missing docstring (advisory) |
PRRT_kwDORK8b986Hmi-A |
Banned term "bridge" in TwoInjectiveComparison/Basic.lean line 496 |
PRRT_kwDORK8b986Hmi_9 |
Banned phrase "at the heart of" in TwoInjectiveComparison/Basic.lean line 726 |
PRRT_kwDORK8b986HmjC9 |
Lean identifiers in prose, TwoInjectiveComparison/Basic.lean line 406 |
PRRT_kwDORK8b986HmjHm |
Lean identifier in docstring prose, VertexComplement/Basic.lean line 87 |
New finding this cycle
One new Category A issue found (inline comment posted above):
- Incomplete proof
\uses{}inthm:peps_postAbsorptionEdgeInsertionEquality(blueprint lines 2231–2232):edgeInsertedCoeff_applyGauge(FundamentalTheorem/EdgeInsertion.lean:255) is the key computational step in the now-proven Lean proof and is cited to arXiv:1804.04964, Section 3,eq:inj_equal_edge. It has no blueprint entry, so it cannot appear in\uses{}. A new entrythm:peps_edgeInsertedCoeff_applyGaugeis needed.
Summary: 1 equivalence issue (incomplete \uses{}), 13 prose/status issues from prior cycles unresolved.
| \uses{thm:peps_exists_edgeGaugeFamily, thm:peps_edge_gauge_absorption, | ||
| def:peps_postAbsorptionEdgeInsertionEquality} |
There was a problem hiding this comment.
Category A — proof \uses{} incomplete: edgeInsertedCoeff_applyGauge has no blueprint entry
The new \begin{proof}\leanok block lists
\uses{thm:peps_exists_edgeGaugeFamily, thm:peps_edge_gauge_absorption,
def:peps_postAbsorptionEdgeInsertionEquality}but the Lean proof (FundamentalTheorem.lean, line 262) invokes edgeInsertedCoeff_applyGauge (defined in FundamentalTheorem/EdgeInsertion.lean, line 255) as the key computation:
rw [hΦcoeff e σ M, hΦconj e M, edgeInsertedCoeff_applyGauge]edgeInsertedCoeff_applyGauge states the open-edge version of the gauge-insertion identity:
$$
\mathrm{edgeInsertedCoeff}(B^Z, e, \sigma, N)
= \mathrm{edgeInsertedCoeff}(B, e, \sigma,; Z_e^T N (Z_e^{-1})^T),
$$
and its docstring cites arXiv:1804.04964, Section 3, eq:inj_equal_edge. This is a mathematically substantive, sorry-free, source-cited result — not a trivial auxiliary lemma. Because it has no blueprint entry, it cannot appear in \uses{} and the proof dependency graph is incomplete.
Fix: add a new blueprint entry (e.g.\ thm:peps_edgeInsertedCoeff_applyGauge) with \lean{TNLean.PEPS.edgeInsertedCoeff_applyGauge}, \leanok, and proof \leanok, then add it to this \uses{} block.
(Note: thm:peps_edge_gauge_absorption — which records that (absorbEdgeGauges B X).component = gaugeVertex — is a trivial rfl and is not directly invoked in the Lean proof; the substantive step is edgeInsertedCoeff_applyGauge.)
LionSR
changed the title
Closes the injective PEPS Fundamental Theorem
fundamentalTheorem_PEPS(arXiv:1804.04964, Theorem 2) is proved sorry-free,#print axioms-clean ([propext, Classical.choice, Quot.sound], nosorryAx) on the source-faithful statement:Two faithfulness defects found and corrected
The chain was originally doubly false — silently missing two of the source's standing assumptions, each now restored and justified by a machine-checked counterexample:
∀ e, 0 < bondDim e): without it a zero-dimensional edge makesSameStatevacuous (PositivityCounterexamples, fix(peps): physical_to_virtual_insertion is false without positive bonds (#1370) #2392/fix(peps): the injective PEPS FT chain (incl. the headline theorem) is false without positive bonds #2394).G.Connected): without it the per-vertex gauge scalarsc_vneed not form a coboundary, so no single gauge exists (GaugeConsistencyConnectivityCounterexample, this PR).The proof chain (all axiom-clean)
edgeBlockedThreeSiteInjective(#1366) ·physical_to_virtual_insertion(#1370) ·isEdgeBlockedInsertionAlgebraIsomorphism(#1367) ·two_injective_tensor_insertion_comparison(#1361, the operator-Schmidt comparison) ·one_vertex_complement_comparison· vertex-complement region injectivity (VertexComplement/) ·edgeInsertedCoeff_applyGauge(open-edge gauge cancellation) ·post_absorption_edge_insertion_equality(#1364) ·bondDim_eq_of_matrixAlgEquiv(#874) · the coefficient identity +SameTwoBlockInsertions·exists_bondGauge_of_fullContraction(operator-Schmidt uniqueness) ·exists_edgeScalars_of_connected(spanning-tree edge-scalar solve) ·perVertex_gauge_identity(gauge inversion) ·exists_stateCoeff_ne_zero(state nonvanishing via the vertex-complement split).Scope note
This closes the existence / gauge-equivalence clause (Theorem 2). The separate uniqueness-modulo-balanced-edge-scalars clause (
gauge_unique_mod_edge_scalars) retains its own pre-existingsorryand is NOT in this theorem's dependency chain (confirmed by the clean axiom print).Deeply stacked (#2396←#2399←#2400←#2403←this). Closes #128 (existence clause); refs #1252, #1360, #1361, #1364, #874.