feat(peps): per-edge gauge family from the insertion isomorphism (toward gaugeConsistency)#2403
Conversation
…itivity Restore the source's positive-bond standing assumption across the injective PEPS gauge-consistency chain (matching merged #2394), and assemble the per-edge gauge family from #1367 as a sorry-free helper. STEP 0 (statement correction): this branch predates #2394, so `gaugeConsistency` LACKED `hpos : ∀ e, 0 < A.bondDim e` and was FALSE (a zero-dimensional edge empties the virtual configuration, making `SameState` vacuous while the gauge-equivalence conclusion stays a genuine constraint). Adds `hpos` to `gaugeConsistency` and threads it through `fundamentalTheorem_PEPS_of_bondDim` (+`hpos`) and the headline `fundamentalTheorem_PEPS` (+`hposA`/`hposB`), with the faithfulness-fix docstring note. The hpos-free version is never closed. New file `TNLean/PEPS/EdgeGaugeFamily.lean` (root-imported, sorry-free): - `glReindex` / `glReindex_coe` — transport an invertible matrix across an index-size equality, with the matrix-coercion identity. - `reindexAlgEquiv_finCongr_symm_round` — the reindex round-trip identity. - `exists_edgeGaugeFamily` — for each edge, the edge-blocked three-site chains are injective (positive bonds), #1367 gives the algebra iso `Φ_e`, Skolem--Noether (`edgeGaugeFromInsertionAlgebraIsomorphism`) realizes it as conjugation by an invertible bond matrix, and transport across `hDim` assembles one global gauge family `X` with the per-edge inserted-coefficient identity and conjugation form. `#print axioms` = [propext, Classical.choice, Quot.sound], no sorryAx. `gaugeConsistency` itself remains `sorry`: the cross-edge assembly into the per-vertex formula `B_v = gaugeVertex A X v` runs through the post-absorption insertion identity `eq:inj_equal_edge` (`post_absorption_edge_insertion_equality`, #1364) and the one-vertex-versus-complement comparison (`two_injective_tensor_insertion_comparison`, #1361), both still open `sorry`s. The `sorry` body now documents this precise obstruction. Refs #1367, #1364, #1361, #874.
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Blueprint ↔ Lean Review — PR 2403
3 equivalence mismatches, 1 missing blueprint entry, 0 prose issues.
Category A — Blueprint ↔ Lean equivalence
A.1 Hypothesis mismatches (three theorems)
All three modified theorems gain a new hpos / hposA / hposB positivity hypothesis that is absent from their blueprint statements. Since the .tex file is not touched in this PR, the \lean{...} tags now point to Lean declarations that are strictly stronger than what the blueprint describes.
| Lean declaration | Blueprint label | New hypothesis absent from blueprint |
|---|---|---|
gaugeConsistency |
thm:gaugeConsistency (line 2092) |
hpos : ∀ e, 0 < A.bondDim e |
fundamentalTheorem_PEPS_of_bondDim |
thm:fundamentalTheorem_PEPS_of_bondDim (line 2527) |
hpos : ∀ e, 0 < A.bondDim e |
fundamentalTheorem_PEPS |
thm:fundamentalTheorem_PEPS (line 2540) |
hposA, hposB : ∀ e, 0 < *.bondDim e |
All three entries carry \notready, so there is no false \leanok to remove. But the \lean{...} link is still a mathematical claim: "this blueprint statement describes that Lean declaration." All three are currently false in that sense. The fundamentalTheorem_PEPS case is the most visible — it is presented as Theorem 2 of [Molnar2018NormalPEPS], which carries no positivity clause.
Required fix in ch13a_peps_ft.tex: for each of the three entries, either (a) add the positivity hypothesis explicitly to the blueprint statement and mark it as a deviation from the source via a LaTeX comment citing the paper-gap document, or (b) drop the \lean{...} tag until a source-faithful (positivity-free) Lean version exists.
A.4 Missing blueprint entry
exists_edgeGaugeFamily is the principal sorry-free result of this PR. No \begin{theorem} block for it exists in the blueprint. A new entry is needed in ch13a_peps_ft.tex with \lean{TNLean.PEPS.exists_edgeGaugeFamily}, \leanok on both statement and proof, and \uses{...} for at least the edge-blocked isomorphism (#1367) and the Skolem–Noether step.
Category B — Prose quality
No violations found in the changed Lean docstrings or comments.
Replace `B̃_v` (B + combining tilde U+0303) with `B'_v` in a comment on line 600 of TNLean/PEPS/FundamentalTheorem.lean. The style linter (ERR_UNICODE) rejects U+0303 as it is not on the allowlist. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
🔧 Auto-fix: style linter (ERR_UNICODE)The CI failure was a style-linter error, not a proof failure: Cause: A comment on line 600 used Fix: Replaced Pushed as |
There was a problem hiding this comment.
Review summary — APPROVE
This is a clean, well-scoped PR that adds a sorry-free helper and applies a documented faithfulness correction. I found no 🔴 blockers and no 🟡 requires-changes issues; the three notes below are ℹ️ advisory.
1. Proof integrity (🔴) — pass
- The new headline result
exists_edgeGaugeFamily(TNLean/PEPS/EdgeGaugeFamily.lean) issorry-free, and every dependency it invokes is itselfsorry-free and used with a matching signature:isEdgeBlockedInsertionAlgebraIsomorphism(InsertionAlgebra.lean:951),edgeGaugeFromInsertionAlgebraIsomorphism(EdgeGaugeExtraction.lean:30),IsVertexInjective.edgeBlockedThreeSiteInjective(EdgeMiddlePhysical/KernelDescent.lean:689), andedgeInsertedCoeff(Blocking.lean:797). The PR's#print axioms = [propext, Classical.choice, Quot.sound]claim is consistent with this. gaugeConsistencyremainssorry, but this is a pre-existingsorryin the exploratory PEPS capstone (deliberately excluded from the default root perTNLean.lean), and the body now documents the precise obstruction. I confirmed its two cited load-bearing dependencies are genuinely still open:post_absorption_edge_insertion_equality(FundamentalTheorem.lean:554,sorry, #1364) andtwo_injective_tensor_insertion_comparison(TwoInjectiveComparison.lean:336,sorry, #1361). The comment is accurate. No new unmarkedsorryis introduced.
2. Proof correctness (🔴) — pass
I traced the exists_edgeGaugeFamily proof by hand. The construction X_e := glReindex (hEdge e).symm (Z e) has the right type (GL (Fin (B.bondDim e)) → GL (Fin (A.bondDim e))). After rw [hZ e, hXcoe, hXinvcoe], simp only [map_mul, reindexAlgEquiv_finCongr_symm_round …] pushes the outer reindexAlgEquiv (finCongr (congr_fun hDim e)) through the triple product; the Z e / Z e⁻¹ factors collapse via the round-trip lemma (applied with h = congr_fun hDim e, h' = hEdge e, both proofs of A.bondDim e = B.bondDim e), and the middle reindexAlgEquiv (finCongr (hEdge e)) M vs reindexAlgEquiv (finCongr (congr_fun hDim e)) M discrepancy closes by definitional proof irrelevance. The logic is sound. I could not run a full lake build (no Mathlib oleans / cache in this environment), so I am relying on CI to confirm the final simp only discharges; the structure is correct.
3. Type safety (🔴) — pass
The Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) form is correct: reindexAlgEquiv takes R A as explicit leading arguments (confirmed via reindexAlgEquiv_apply in Mathlib/LinearAlgebra/Matrix/Reindex.lean), and the same pattern is already used in merged code (InsertionAlgebra.lean:924, EdgeGaugeExtraction.lean:37). The AlgEquiv → toRingEquiv → toMulEquiv → Units.mapEquiv chain in glReindex is well-typed.
4. Faithfulness of the hpos correction
The PR adds hpos/hposA/hposB to gaugeConsistency, fundamentalTheorem_PEPS_of_bondDim, and fundamentalTheorem_PEPS (arXiv:1804.04964 Thm 2). Per the CLAUDE.md faithfulness rule this would normally be scrutinized as a hypothesis addition, but here it is a faithfulness restoration, not smuggling: the docstring's counterexample is mathematically correct — a zero-dimensional edge empties the virtual configuration, so both stateCoeffs vanish and SameState holds vacuously while GaugeEquiv stays a genuine constraint — and positive bond dimension is the source's standing assumption for injective PEPS. This matches the merged #2394 correction and cites docs/paper-gaps/peps_injective_ft_section3_route.tex. I confirmed no external call sites break (all callers are inside FundamentalTheorem.lean and were updated).
5–7. Style / performance / documentation — pass
Naming follows conventions (glReindex def camelCase; glReindex_coe, reindexAlgEquiv_finCongr_symm_round theorems snake_case; exists_edgeGaugeFamily uses the standard exists_ prefix). No lines exceed 100 chars. No heavy decide/simp sets. Module docstring and per-declaration docstrings are present and explain the mathematics, with accurate cross-references to all named lemmas (verified each exists).
Advisory (ℹ️, non-blocking)
fundamentalTheorem_PEPS_of_bondDim's docstring doesn't mention its newhposhypothesis (rationale is one declaration below).hposBinfundamentalTheorem_PEPSis currently unused (deliberate placeholder for thesorry'dhDimstep).glReindexand friends areℂ-specialized but fully general; candidates for generalization/upstreaming if reused.
Approving. The two sorrys touched/retained (gaugeConsistency, the hDim step) are pre-existing, documented, paper-gap-tracked obligations in the exploratory capstone; this PR strictly reduces the sorry surface by adding a verified helper.
| (hAB : SameState A B) : | ||
| (hAB : SameState A B) | ||
| (hposA : ∀ e : Edge G, 0 < A.bondDim e) | ||
| (hposB : ∀ e : Edge G, 0 < B.bondDim e) : |
There was a problem hiding this comment.
ℹ️ Advisory. hposB is currently unused in the proof body: the only call is fundamentalTheorem_PEPS_of_bondDim A B hA hB hAB hDim hposA, which threads only hposA, and hposB is not consumed elsewhere (the place it belongs is the hDim derivation, which is still sorry). This is the right symmetric, source-faithful statement to keep — dropping hposB would likely make the eventual hDim : A.bondDim = B.bondDim proof unprovable — so I am not requesting its removal. Flagging only so the unused-binder is a deliberate placeholder for the hDim step, not an oversight; the Lean unused-variable linter may emit a warning here.
| theorem reindexAlgEquiv_finCongr_symm_round {m n : ℕ} (h h' : m = n) | ||
| (N : Matrix (Fin n) (Fin n) ℂ) : | ||
| Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) | ||
| (Matrix.reindexAlgEquiv ℂ ℂ (finCongr h'.symm) N) = N := by |
There was a problem hiding this comment.
ℹ️ Advisory (modularity). glReindex, glReindex_coe, and reindexAlgEquiv_finCongr_symm_round are stated only over ℂ, but nothing in them is ℂ-specific — glReindex works for any [Field R]/[CommRing R] (transporting GL (Fin m) R across m = n), and the round-trip lemma holds for reindexAlgEquiv R A over any [CommSemiring R] [Semiring A]. If a second GL-reindex consumer appears, consider generalizing these and hoisting them out of PEPS/ (a Matrix/GeneralLinearGroup helper, or even an upstream Mathlib candidate). Acceptable as local helpers for now.
Review Summary — PR #2403Verdict: REQUEST_CHANGES 🟡 One 🟡 issue must be fixed before approval (see inline comment). What this PR does
🟡 Requires change
🔴 Proof integrity — PASSNo 🔴 Proof correctness — PASSThe construction of Existing review commentsSeven unresolved comments exist from a previous review cycle. Comments 1-4 (blueprint sync) are out of scope for this review. Comments 5-7 (advisory: docstring cross-reference, unused binder, modularity) remain applicable but non-blocking. |
There was a problem hiding this comment.
Review Summary — PR #2403
Verdict: REQUEST_CHANGES 🟡
🟡 Requires change — see inline comment
fundamentalTheorem_PEPS docstring, line 648: "The theorem is stated with the source's hypothesis set" contradicts the newly added hposA/hposB hypotheses. The docstring must be reworded. See inline comment for details.
🔴 Proof integrity — PASS
No sorry/axiom/admit/native_decide in the new file EdgeGaugeFamily.lean.
🔴 Proof correctness — PASS
exists_edgeGaugeFamily is mathematically sound: hpos → edge-blocked three-site injectivity → #1367 algebra isomorphism → Skolem-Noether conjugation → transport to A-side bonds.
Other categories — PASS
Type safety, performance, modularity, paper-gap notes all pass. Pre-existing advisory comments remain applicable but non-blocking.
There was a problem hiding this comment.
Pull request overview
Adds a new per-edge gauge-family construction for injective PEPS (derived from the edge-blocked insertion algebra isomorphism + Skolem–Noether) and threads explicit positive-bond hypotheses through the PEPS Fundamental Theorem API to rule out the zero-bond “vacuous SameState” counterexample.
Changes:
- Introduces
exists_edgeGaugeFamily, producing a global edge gauge familyX : (e : Edge G) → GL (Fin (A.bondDim e)) ℂwith per-edge conjugation and inserted-coefficient identities. - Strengthens
gaugeConsistency/fundamentalTheorem_PEPS_of_bondDim/fundamentalTheorem_PEPSstatements by adding explicit positivity hypotheses on bond dimensions. - Updates the root
TNLean.leanimports to include the new edge-gauge-family module.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| TNLean/PEPS/FundamentalTheorem.lean | Adds explicit positive-bond hypotheses to the main PEPS FT statements and updates proof-status commentary accordingly. |
| TNLean/PEPS/EdgeGaugeFamily.lean | New module constructing the per-edge/global edge gauge family from insertion algebra isomorphisms. |
| TNLean.lean | Imports the new PEPS.EdgeGaugeFamily module. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Blueprint ↔ Lean Review — PR 2403 (synchronize, commit 2c483ab)
4 equivalence mismatches / missing entries still open; 0 new issues; 1 thread resolved.
Resolved by this commit
The fundamentalTheorem_PEPS "Proof status" paragraph previously claimed "the theorem is stated with the source's hypothesis set," which contradicted the new hposA/hposB positivity hypotheses. The synchronize commit rewrites it to "The conclusion is the source gauge-equivalence conclusion, with positive bond dimension made explicit to exclude the zero-bond vacuous-state case above." The contradiction is gone; thread PRRT_kwDORK8b986HccLv resolved.
Category A — still open (from prior review)
The blueprint/src/chapter/ch13a_peps_ft.tex file is unchanged in this PR. All four Category A issues raised in the prior REQUEST_CHANGES review remain open:
| Thread | Issue |
|---|---|
PRRT_kwDORK8b986HcWi0 |
thm:gaugeConsistency blueprint lacks the new hpos hypothesis |
PRRT_kwDORK8b986HcWo_ |
thm:fundamentalTheorem_PEPS_of_bondDim blueprint lacks the new hpos hypothesis |
PRRT_kwDORK8b986HcWzs |
thm:fundamentalTheorem_PEPS blueprint lacks hposA/hposB |
PRRT_kwDORK8b986HcW-1 |
No blueprint entry (\lean{}, \leanok, \uses{}) for the sorry-free exists_edgeGaugeFamily |
Category B — no new issues
No new prose violations in the updated docstring or in any other changed text.
There was a problem hiding this comment.
Review Summary — PR #2403 (re-review on synchronize)
Verdict: APPROVE ✅
The one in-scope blocking 🟡 from the previous cycle has been addressed in the latest push. No new 🔴/🟡 issues found within this review's scope.
Previous blocking issue — resolved
The earlier 🟡 (contradictory faithfulness claim) flagged that the fundamentalTheorem_PEPS "Proof status" paragraph read "The theorem is stated with the source's hypothesis set" while the signature adds hposA/hposB. The latest push reworded it (lines 648–650) to "The conclusion is the source gauge-equivalence conclusion, with positive bond dimension made explicit to exclude the zero-bond vacuous-state case above," which no longer contradicts the preceding "Positive-bond hypothesis" paragraph. I resolved that bot thread.
🔴 Proof integrity — PASS
exists_edgeGaugeFamily (TNLean/PEPS/EdgeGaugeFamily.lean:79) is sorry/axiom-free. The sorrys in gaugeConsistency (FundamentalTheorem.lean:608) and the hDim step of fundamentalTheorem_PEPS (FundamentalTheorem.lean:666) are pre-existing, consistent with paper-realignment mode, and carry paper-gap citations plus tracked obligations (#1364, #1361).
🔴 Proof correctness — PASS
The construction of exists_edgeGaugeFamily is mathematically sound: from hpos (and hposB, derived by rw [← congr_fun hDim e]), IsVertexInjective.edgeBlockedThreeSiteInjective gives three-site injective chains; isEdgeBlockedInsertionAlgebraIsomorphism (#1367) yields the per-edge Φ_e; edgeGaugeFromInsertionAlgebraIsomorphism (Skolem–Noether) realizes each as conjugation by an invertible B-side Z_e. The transport to the A-side via glReindex is justified, and reindexAlgEquiv_finCongr_symm_round correctly bridges the two distinct proofs of A.bondDim e = B.bondDim e (hEdge e from Skolem–Noether vs congr_fun hDim e); the closing simp only [map_mul, …] discharges the remainder by proof-irrelevance of those two equality terms.
🔴 Type safety / 🟡 Performance — PASS
Coercions through Units.mapEquiv/reindexAlgEquiv are handled explicitly via glReindex_coe and map_inv. The proof is short with no timeout risk.
Faithfulness of the positivity hypothesis
The hpos/hposA/hposB additions are not smuggled hypotheses — without them the theorem is false (the zero-bond vacuous-SameState counterexample). The deviation is recorded in docs/paper-gaps/peps_injective_ft_section3_route.tex (lines 188–202: "The implication from vertex injectivity to middle-block injectivity is false without a positivity hypothesis … The source avoids this because injective PEPS have nonzero-dimensional virtual bond spaces"), and the docstrings cite it accurately. This satisfies the CLAUDE.md faithfulness rule's paper-gap-note requirement.
Out of scope (handled by the Blueprint Sync & Prose Review workflow)
The unresolved A.1/A.4 threads concern blueprint \lean{}/\leanok/\uses{} sync (positivity hypotheses absent from ch13a_peps_ft.tex; missing blueprint entry for exists_edgeGaugeFamily). Not re-raised here; left for the dedicated workflow.
ℹ️ Advisory (non-blocking, unchanged)
fundamentalTheorem_PEPS_of_bondDimdocstring could add a one-line cross-reference to the positivity rationale.hposBis an unused binder (deliberate placeholder for the futurehDimproof; may trigger the unused-variable linter).glReindex/glReindex_coe/reindexAlgEquiv_finCongr_symm_roundare stated only overℂthough nothing isℂ-specific — fine as local helpers.
These do not block approval.
There was a problem hiding this comment.
Review Summary — PR #2403 (synchronize, commit 2c483ab)
Verdict: APPROVE ✅
This is a re-review on a synchronize trigger. The head commit (2c483ab) is unchanged from the previous review cycle, which was also approved. No new 🔴 or 🟡 issues found in the code changes.
What was reviewed
New file TNLean/PEPS/EdgeGaugeFamily.lean — sorry-free, #print axioms-clean, builds successfully:
glReindex/glReindex_coe/reindexAlgEquiv_finCongr_symm_round: small auxiliary lemmas for transportingGLmatrices across bond-dimension equalities. All have docstrings. The ℹ️ advisory about ℂ-specificity (flagging for potential future generalization) remains noted.exists_edgeGaugeFamily(line 79): the main sorry-free result. For vertex-injectiveA,BwithSameState, matching bond dimensions, and positive bond dimensions, it assembles a global edge-gauge familyX_e ∈ GLon the A-side bonds, together with the per-edge insertion algebra isomorphismΦ_eand proofs thatΦ_epreserves inserted coefficients and equals conjugation byX_e(up to thehDimreindexing). The proof chainsedgeBlockedThreeSiteInjective→isEdgeBlockedInsertionAlgebraIsomorphism(#1367) →edgeGaugeFromInsertionAlgebraIsomorphism(Skolem–Noether) →glReindex(transport back to A-side). The finalsimpstep handles the algebra-homomorphism distribution and round-trip identity correctly.
Modified TNLean/PEPS/FundamentalTheorem.lean:
gaugeConsistency(line 577): addshpos : ∀ e, 0 < A.bondDim ehypothesis. Proof body stillsorry— both dependencies (#1364 post-absorption, #1361 two-injective comparison) are tracked open issues, and the updated comment clearly documents the remaining obligations. Pre-existingsorry, consistent with paper-realignment mode.fundamentalTheorem_PEPS_of_bondDim(line 623): addshposhypothesis, threads it through togaugeConsistency. Docstring updated to remove the stale "stated with the source's hypothesis set" claim (fixes the issue fromPRRT_kwDORK8b986HccLv, now outdated).fundamentalTheorem_PEPS(line 653): addshposA/hposBhypotheses. Docstring now includes a dedicated "Positive-bond hypothesis (faithfulness fix)" section explaining why positivity is required (zero-bond vacuousSameStatecounterexample). ThehDimderivation is stillsorry(pre-existing, tracked).
Category-by-category findings
| Category | Severity | Findings |
|---|---|---|
| Proof integrity | 🔴 | EdgeGaugeFamily.lean is sorry/axiom-free. Pre-existing sorrys in gaugeConsistency and fundamentalTheorem_PEPS are documented and consistent with paper-realignment mode. |
| Proof correctness | 🔴 | exists_edgeGaugeFamily proof is well-structured: the algebraic step correctly uses reindexAlgEquiv_finCongr_symm_round to resolve the round-trip identity. No correctness issues. |
| Mathlib style | 🟡 | Naming follows conventions. glReindex uses lowercase gl — acceptable as a local convention. Variable names are consistent with surrounding code. No violations. |
| Type safety | 🔴 | No type mismatches, universe issues, or coercion problems. noncomputable marker on glReindex is correct (involves ℂ and AlgEquiv). |
| Performance | 🟡 | No heavy decide, unbounded simp, or deep rw chains. The choose tactic is used on Fintype-indexed families — appropriate. |
| Modularity | 🟡 | ℹ️ advisory (pre-existing): glReindex and helpers are ℂ-specific; could be generalized to [CommRing R] for upstream Mathlib candidacy. Acceptable as local helpers. |
| Documentation | 🟡 | All new declarations have docstrings. Module-level docstring present for EdgeGaugeFamily.lean. Source citations (arXiv:1804.04964, Section 3, lines 560–586) are provided. Updated docstrings in FundamentalTheorem.lean are thorough. |
| Paper-gap notes | 🟡 | No paper-gap files changed in this PR. |
Out of scope (Blueprint ↔ Lean sync)
Per the review instructions, blueprint ↔ Lean equivalence checks (\lean{...} / \leanok / \uses{...} tags) are handled by a dedicated workflow. The previously-flagged blueprint-level tracking items (positivity hypothesis documentation in ch13a_peps_ft.tex, blueprint entry for exists_edgeGaugeFamily) are not re-raised here.
There was a problem hiding this comment.
Review summary (synchronize event) — categories A and B only.
Category A — Blueprint ↔ Lean equivalence: 4 open issues (all carry-over)
The four A-category issues flagged in the previous review remain unresolved because this synchronize made no blueprint .tex changes:
- A.1
gaugeConsistency(thread PRRT_kwDORK8b986HcWi0): blueprint has nohposhypothesis; Lean now requires∀ e, 0 < A.bondDim e. - A.1
fundamentalTheorem_PEPS_of_bondDim(thread PRRT_kwDORK8b986HcWo_): same — blueprint has no positivity clause. - A.1
fundamentalTheorem_PEPS(thread PRRT_kwDORK8b986HcWzs): blueprint has nohposA/hposB; Lean now has both. - A.4
exists_edgeGaugeFamily(thread PRRT_kwDORK8b986HcW-1): no blueprint entry (\begin{theorem}+\lean{...}+\leanokon statement and proof +\uses{...}) for the new sorry-free theorem.
Category B — Prose: 1 carry-over + 1 new
- Carry-over (copilot thread PRRT_kwDORK8b986HkX_e, open): "packages" and "assembly" in the
exists_edgeGaugeFamilytheorem docstring. - New (inline comment above): three occurrences of "assembles"/"assembly" as organizational process language in the module docstring of
EdgeGaugeFamily.lean(lines 10, 19, 24) — distinct location from the copilot thread.
Counts: 4 A-category carry-over mismatches (3 × hypothesis mismatch, 1 × missing blueprint entry), 2 B-category prose issues (1 carry-over, 1 new).
There was a problem hiding this comment.
Review Summary — PR #2403 (synchronize, commit bc0350d)
Verdict: APPROVE ✅
No new 🔴 or 🟡 issues found within this review's scope. The synchronize push (merge from base branch + minor doc adjustment) does not introduce regressions.
🔴 Proof integrity — PASS
EdgeGaugeFamily.lean (new file) is sorry/axiom/admit/native_decide-free. All its transitive dependencies (isEdgeBlockedInsertionAlgebraIsomorphism in InsertionAlgebra.lean, edgeGaugeFromInsertionAlgebraIsomorphism in EdgeGaugeExtraction.lean, IsVertexInjective.edgeBlockedThreeSiteInjective in KernelDescent.lean) are themselves sorry-free. The pre-existing sorrys in gaugeConsistency (line 580) and the hDim step of fundamentalTheorem_PEPS (line 638) are unchanged, documented with paper-gap citations, and consistent with paper-realignment mode as described in CLAUDE.md.
🔴 Proof correctness — PASS
The construction of exists_edgeGaugeFamily (line 79) is mathematically sound:
hpos → hposB(viarw [← congr_fun hDim e])edgeBlockedThreeSiteInjectiveat each edge (using positivity)isEdgeBlockedInsertionAlgebraIsomorphism(#1367) → per-edgeΦ_e+ inserted-coefficient identityedgeGaugeFromInsertionAlgebraIsomorphism(Skolem–Noether) →hEdge,Z e, and the conjugation identity- Transport to A-side bonds via
glReindex
The key algebraic step uses reindexAlgEquiv_finCongr_symm_round to bridge the two different equality proofs (hEdge e and congr_fun hDim e), which is the correct approach. Compilation is confirmed by CI.
🔴 Type safety — PASS
The coercion chain Units.mapEquiv (Matrix.reindexAlgEquiv ℂ ℂ (finCongr h)).toRingEquiv.toMulEquiv in glReindex is well-typed. glReindex_coe and the map_inv usage in hXinvcoe handle the GL → Matrix coercion correctly. The Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) pattern is consistent with existing usage in InsertionAlgebra.lean and EdgeGaugeExtraction.lean.
🟡 Mathlib style — PASS
Naming follows conventions: definitions camelCase (glReindex), theorems snake_case (glReindex_coe, reindexAlgEquiv_finCongr_symm_round, exists_edgeGaugeFamily). Variable names are consistent with surrounding code. The noncomputable and classical markers are correctly placed.
🟡 Performance — PASS
No decide, omega, or unbounded simp sets. The choose tactic operates on a Fintype-indexed family (Edge G is finite), and the final simp only uses exactly two lemmas. No timeout risk.
🟡 Documentation — PASS
- Module docstring for
EdgeGaugeFamily.lean: present, explains the mathematical context and relationship togaugeConsistencyand the paper-gap document. - All four new declarations have docstrings.
exists_edgeGaugeFamilyhas an extensive docstring with source citation (arXiv:1804.04964, Section 3, lines 560–586), explanation of the construction, and cross-reference togaugeConsistency.- The
fundamentalTheorem_PEPSdocstring includes a "Positive-bond hypothesis (faithfulness fix)" section explaining the zero-bond counterexample and citing the paper-gap document. - ℹ️ Advisory (from prior review, still applicable):
fundamentalTheorem_PEPS_of_bondDim's docstring does not explicitly mention its newhposhypothesis, though the rationale is fully explained one declaration below infundamentalTheorem_PEPS.
🟡 Modularity & duplication — PASS
ℹ️ Advisory (from prior review, unchanged): glReindex, glReindex_coe, and reindexAlgEquiv_finCongr_symm_round are stated only over ℂ though nothing in them is ℂ-specific. Acceptable as local helpers; candidates for generalization if a second consumer appears.
🟡 Paper-gap notes — N/A
No files under docs/paper-gaps/ are changed in this PR. Citations to docs/paper-gaps/peps_injective_ft_section3_route.tex in the docstrings accurately reference that document's discussion of the positivity hypothesis (lines 189–214).
Out of scope (handled by the dedicated Blueprint Sync & Prose Review workflow)
Four unresolved blueprint sync threads and two prose-quality threads from prior review cycles remain open — these are not re-raised here.
Previous bot threads
The one previously-blocking thread (PRRT_kwDORK8b986HccLv — contradictory faithfulness claim in fundamentalTheorem_PEPS docstring) was resolved by commit 2c483ab. The remaining unresolved bot threads are either out-of-scope (blueprint sync, prose style) or ℹ️ advisory (documentation, unused binder, modularity) and do not block approval.
There was a problem hiding this comment.
Review summary (synchronize)
Resolved from previous round: 6 claude threads resolved — positivity hypotheses added to blueprint for gaugeConsistency, fundamentalTheorem_PEPS_of_bondDim, and fundamentalTheorem_PEPS; blueprint entry for exists_edgeGaugeFamily added with \leanok on statement and proof; fundamentalTheorem_PEPS_of_bondDim docstring advisory addressed; stale "assembles" thread (outdated) resolved.
New findings: 3 category-A, 2 category-B.
A — Blueprint ↔ Lean equivalence
3 × A.3 stale \notready: All three theorems now have Lean declarations whose signatures match the updated blueprint statements, so \notready should be replaced with \leanok on each statement (no \leanok on the proof in any case, since the proofs are sorry or call a sorry-d dependency). See inline comments at lines 2254, 2693, and 2707.
exists_edgeGaugeFamily (new entry, \leanok on statement and proof): Confirmed sorry-free. Dependencies isEdgeBlockedInsertionAlgebraIsomorphism and edgeGaugeFromInsertionAlgebraIsomorphism both carry zero sorry. Blueprint statement matches Lean signature on all hypotheses, quantifier structure, and conjugation formula. ✓
B — Prose quality
2 × B §1 Lean hypothesis names in docstrings. hDim (EdgeGaugeFamily.lean:66) and hposA/hposB (FundamentalTheorem.lean:613) are Lean hypothesis variable names used in backticks rather than mathematical descriptions. See inline comments.
There was a problem hiding this comment.
Review Summary — PR #2403 (re-review on synchronize)
Verdict: APPROVE ✅
The blocking issue from the previous cycle has been fixed and no in-scope 🔴/🟡 issues remain.
Resolution of the prior blocker
The previous cycle's 🟡 was a contradictory faithfulness claim in the fundamentalTheorem_PEPS docstring ("stated with the source's hypothesis set" while it adds hposA/hposB). The current docstring (TNLean/PEPS/FundamentalTheorem.lean:623) now reads "The conclusion is the source gauge-equivalence conclusion, with positive bond dimension made explicit to exclude the zero-bond vacuous-state case," which is consistent with the preceding "Positive-bond hypothesis (faithfulness fix)" paragraph. The contradiction is gone.
🔴 Proof integrity — PASS
TNLean/PEPS/EdgeGaugeFamily.lean is sorry-free (PR reports #print axioms = [propext, Classical.choice, Quot.sound], no sorryAx). The sorrys in gaugeConsistency, fundamentalTheorem_PEPS_of_bondDim's consumers, fundamentalTheorem_PEPS (the hDim step), and post_absorption_edge_insertion_equality are all pre-existing, sit in the exploratory PEPS capstone (deliberately excluded from the default root per TNLean.lean), and each documents its precise obstruction (#1364, #1361) under paper-realignment mode. No new sorry is introduced.
🔴 Proof correctness — PASS
exists_edgeGaugeFamily is mathematically sound. The chain hpos → IsVertexInjective.edgeBlockedThreeSiteInjective for both A/B → isEdgeBlockedInsertionAlgebraIsomorphism (#1367) giving Φ_e with matching inserted coefficients → edgeGaugeFromInsertionAlgebraIsomorphism (Skolem–Noether) realizing Φ_e X = Z · reindex X · Z⁻¹, then transport of Z to the A-side bond via glReindex (hEdge e).symm. The closing step is correct: reindexAlgEquiv_finCongr_symm_round cancels the inner finCongr (hEdge e).symm against the outer finCongr (congr_fun hDim e) on Z and Z⁻¹, and the residual reindex(finCongr (congr_fun hDim e)) M vs reindex(finCongr (hEdge e)) M are defeq by proof-irrelevance of the two A.bondDim e = B.bondDim e proofs. Stating the round-trip lemma with two independent equality proofs (h, h') is exactly what makes this cancellation go through.
The source citation arXiv:1804.04964, Section 3, lines 560–586 is accurate: Papers/1804.04964/paper_normal.tex:560–586 is the proof that the per-bond map is an algebra isomorphism of conjugation form Y = ZXZ⁻¹ with equal bond dimensions — precisely the per-edge content this theorem records. The cross-edge blocking step (route note :981–1065) is correctly deferred to gaugeConsistency.
Faithfulness (positivity hypotheses) — sound
Adding hpos/hposA/hposB is the correct scope-restriction fix: a zero-dimensional edge empties the virtual configuration, vanishing both state coefficients and making SameState vacuous while GaugeEquiv stays a real constraint, so the positivity-free statement is false. The deviation is documented in docs/paper-gaps/peps_injective_ft_section3_route.tex (which records the elimination plan: derive positivity from injectivity), the docstrings cite it, and the blueprint carries a % Scope restriction comment that no longer presents fundamentalTheorem_PEPS as verbatim Theorem 2. This matches CLAUDE.md §Locally-fixable deviations / §Faithfulness rule.
ℹ️ Advisory (non-blocking)
fundamentalTheorem_PEPS:hposBis currently unused in the proof body (onlyhposAis threaded intofundamentalTheorem_PEPS_of_bondDim); it is the correct symmetric placeholder for the openhDimderivation. Keep it — the unused-binder linter warning is expected. (Existing thread.)glReindex/glReindex_coe/reindexAlgEquiv_finCongr_symm_roundare stated only overℂthough nothing isℂ-specific; acceptable as local helpers, worth generalizing/hoisting if a second consumer appears. (Existing thread.)
Out of scope (handled by the Blueprint Sync & Prose Review workflow)
The \notready → \leanok status on thm:gaugeConsistency, the new thm:peps_exists_edgeGaugeFamily blueprint entry, and \lean/\uses tags are not assessed here. Two now-outdated copilot prose threads (process-language in docstrings) were addressed by the new commits and have been resolved.
There was a problem hiding this comment.
Review Summary — PR #2403
Verdict: REQUEST_CHANGES 🔴
One 🔴 proof-correctness issue must be fixed before merge: the simp only call at line 132–133 of TNLean/PEPS/EdgeGaugeFamily.lean does not close the goal. See the inline comment for the detailed analysis.
What this PR does
- Adds
TNLean/PEPS/EdgeGaugeFamily.lean: theoremexists_edgeGaugeFamilyassembling per-edge gauge families from the insertion-algebra isomorphism (#1367) and Skolem-Noether. - Adds positivity hypotheses (
hpos/hposA/hposB) togaugeConsistency,fundamentalTheorem_PEPS_of_bondDim, andfundamentalTheorem_PEPS— correcting the vacuous-SameStatecounterexample when bond dimensions are zero (matching the #2394 correction). - Updates
gaugeConsistency'ssorrybody to referenceexists_edgeGaugeFamilyand the remaining dependencies (#1364, #1361). - Adds blueprint entry
thm:peps_exists_edgeGaugeFamily(\leanok) and updatesgaugeConsistency/ fundamental-theorem statements in the blueprint to match the new hypotheses.
🔴 Blocker: Proof correctness gap in exists_edgeGaugeFamily
The simp only at lines 132–133 of EdgeGaugeFamily.lean leaves an unclosed goal. After map_mul distributes the outer reindex and reindexAlgEquiv_finCongr_symm_round simplifies the round-trips on Z and Z⁻¹, the remaining inequality compares Matrix.reindexAlgEquiv ℂ ℂ (finCongr (hEdge e)) M against Matrix.reindexAlgEquiv ℂ ℂ (finCongr (congr_fun hDim e)) M. These differ only in the proof of A.bondDim e = B.bondDim e used for finCongr. simp only with the two listed lemmas cannot equate them.
Fix: Add have hProofEq : hEdge e = congr_fun hDim e := Subsingleton.elim _ _ and rw [hProofEq] before the simp only block (or after it, followed by rfl).
🔴 Proof integrity — PASS
No sorry/axiom/native_decide in the new file. Pre-existing sorrys are in paper-realignment mode and consistent with documentation.
🟡 Mathlib style — PASS
Naming conventions follow project standards. The simp only with explicit lemma list is good style (once the goal is actually closed). open scoped BigOperators is unused in the new file — consider removing, but this is non-blocking.
🔴 Type safety — PASS
No type mismatches, universe issues, or coercion problems. The glReindex definition correctly uses Units.mapEquiv and Matrix.reindexAlgEquiv.
🟡 Performance — PASS
No decide on large types, no unbounded simp. The choose tactic is used with small finite families.
🟡 Documentation — PASS
Docstrings are thorough with source citations. The "Positive-bond hypothesis" paragraph in fundamentalTheorem_PEPS correctly explains the faithfulness fix.
Changes since previous review
- The contradictory "stated with the source's hypothesis set" claim has been fixed ✓
- The new blueprint entry
thm:peps_exists_edgeGaugeFamilyhas been added with\leanok✓ - Blueprint statements for
gaugeConsistency,fundamentalTheorem_PEPS_of_bondDim, andfundamentalTheorem_PEPShave been updated to include positivity hypotheses ✓ - The
\notreadyonthm:gaugeConsistencywas kept (deliberate given thesorryproof body)
There was a problem hiding this comment.
Blueprint ↔ Lean Review — PR 2403 (synchronize, commit ed3018b)
Verdict: REQUEST_CHANGES — 1 new 🟡 B-category issue; no new A-category issues.
Resolved threads (6)
The following threads from prior cycles are now fixed and have been resolved:
| Thread | Issue | Status |
|---|---|---|
PRRT_kwDORK8b986HmDw3 |
A.3 \notready stale on fundamentalTheorem_PEPS_of_bondDim |
✅ Fixed (\leanok) |
PRRT_kwDORK8b986HmDyo |
A.3 \notready stale on fundamentalTheorem_PEPS |
✅ Fixed (\leanok) |
PRRT_kwDORK8b986HmDz3 |
B §1 "across hDim" hypothesis name in docstring |
✅ Fixed (outdated) |
PRRT_kwDORK8b986HmD3N |
B §1 hposA/hposB in docstring |
✅ Fixed (outdated) |
PRRT_kwDORK8b986HmD75 |
A.3 duplicate notready on gaugeConsistency |
✅ Fixed (outdated) |
PRRT_kwDORK8b986HmIp9 |
🔴 simp only goal unclosed |
✅ Fixed by rw [hProofEq] in ed3018b |
Category A — Blueprint ↔ Lean equivalence: no new issues
A.1 — Hypothesis parity (all three updated theorems):
-
gaugeConsistency: blueprint now states "every virtual bond of$A$ has positive dimension" matchinghpos. ✓ -
fundamentalTheorem_PEPS_of_bondDim: blueprint now states "every virtual bond of$A$ has positive dimension" matchinghpos. ✓ -
fundamentalTheorem_PEPS: blueprint now states both$A$ and$B$ positivity, matchinghposA/hposB. ✓
A.2 — \leanok validity:
gaugeConsistency: statement\leanokvalid (signature matches); no\begin{proof}\leanok, correct because Lean proof issorry. ✓fundamentalTheorem_PEPS_of_bondDim: statement\leanokvalid; no proof\leanok, correct (callsgaugeConsistencywhich issorry). ✓fundamentalTheorem_PEPS: statement\leanokvalid; no proof\leanok, correct (contains a directsorry). ✓exists_edgeGaugeFamily: statement\leanok+\begin{proof}\leanokvalid; Lean proof has nosorry. ✓
A.3 — \notready stale: No remaining stale \notready tags on the changed theorems. ✓
A.4 — New decl coverage: exists_edgeGaugeFamily now has a blueprint entry with \lean{TNLean.PEPS.exists_edgeGaugeFamily}, \leanok, and \uses. ✓ Auxiliary helpers (glReindex, glReindex_coe, reindexAlgEquiv_finCongr_symm_round) are bookkeeping lemmas without paper counterparts — no blueprint entries required. ✓
Category B — Prose quality: 1 new 🟡 issue
B §1 — "fundamental-theorem module" in module docstring (line 25 of EdgeGaugeFamily.lean).
The phrase "the fundamental-theorem module" names a Lean organizational unit (the source file FundamentalTheorem.lean) rather than a mathematical object. Per §1 of docs/prose_style.md, implementation language referring to Lean files or the module system should not appear in docstrings. See the inline comment for a suggested fix.
Open advisories (carry-over, not blocking)
PRRT_kwDORK8b986HcZDm:hposBis passed tofundamentalTheorem_PEPSbut not consumed in the sorry-body. Correct once the bond-dimension equality step is filled.PRRT_kwDORK8b986HcZLD:glReindexand round-trip lemma are stated overℂonly; could be generalized.
These are non-blocking and require no action in this PR.
|
|
||
| This is the construction used in the gauge-consistency theorem; the remaining | ||
| cross-edge passage to the per-vertex gauge formula is recorded in | ||
| the fundamental-theorem module and in |
There was a problem hiding this comment.
B §1 — "fundamental-theorem module" is organizational/implementation language.
Line 25 of the module docstring reads:
…is recorded in the fundamental-theorem module and in
docs/paper-gaps/…
"Module" here refers to the Lean source file TNLean/PEPS/FundamentalTheorem.lean — an organizational unit of the Lean build system, not a mathematical object. Per §1 of docs/prose_style.md, implementation language ("module", "file", Lean namespace paths) should not appear in docstrings; the mathematical content should be named instead.
Suggested replacement (one possibility):
This is the construction used in the gauge-consistency theorem; the remaining
cross-edge passage to the per-vertex gauge formula is recorded in the proof of
the fundamental theorem and in
`docs/paper-gaps/peps_injective_ft_section3_route.tex`.
("the proof of the fundamental theorem" names the mathematical content without naming the Lean module.)
There was a problem hiding this comment.
Review Summary — PR #2403 (synchronize)
Verdict: APPROVE ✅
All previously-flagged 🔴/🟡 issues in this review's scope are now addressed, and I verified the central claim by building.
Verification performed
lake build TNLean.PEPS.EdgeGaugeFamily— clean build (2661 jobs, no errors, nosorrywarning in the new file).#print axioms TNLean.PEPS.exists_edgeGaugeFamily→[propext, Classical.choice, Quot.sound]— nosorryAx, confirming the new theorem is sorry-free and axiom-clean.lake build TNLean.PEPS.FundamentalTheorem— builds; the foursorrywarnings (post_absorption_edge_insertion_equality,gaugeConsistency, thehDimstep offundamentalTheorem_PEPS, and the pre-existing one at line 949) are all unchanged/documented and consistent with paper-realignment mode.
Resolved blocking concern (🔴 proof correctness)
The final simp only in exists_edgeGaugeFamily previously failed to close the goal because the outer reindex carried the proof congr_fun hDim e while the round-trip lemma instance carried hEdge e. The added
have hProofEq : congr_fun hDim e = hEdge e := Subsingleton.elim _ _
rw [hProofEq]unifies the two equality proofs before simp only [map_mul, reindexAlgEquiv_finCongr_symm_round ...], and the build confirms the goal now closes. The construction is mathematically sound: hpos → edge-blocked three-site injectivity (edgeBlockedThreeSiteInjective) → the #1367 algebra isomorphism isEdgeBlockedInsertionAlgebraIsomorphism → Skolem–Noether conjugation (edgeGaugeFromInsertionAlgebraIsomorphism) → transport of the B-side conjugator back to the A-bond via glReindex, with reindexAlgEquiv_finCongr_symm_round bridging the round-trip.
Resolved 🟡 (documentation)
The fundamentalTheorem_PEPS docstring no longer claims it is "stated with the source's hypothesis set"; it now carries the Positive-bond hypothesis (faithfulness fix) paragraph explaining the vacuous-SameState counterexample (a zero-dimensional edge makes every state coefficient vanish, so SameState holds without relating the tensors while GaugeEquiv remains a real constraint). The positivity additions to gaugeConsistency, fundamentalTheorem_PEPS_of_bondDim, and fundamentalTheorem_PEPS are reflected in the blueprint statements with a scope-restriction comment and a citation to docs/paper-gaps/peps_injective_ft_section3_route.tex, satisfying the faithfulness rule.
Remaining open threads (ℹ️ advisory — non-blocking)
hposBis unused infundamentalTheorem_PEPS(deliberate placeholder for the still-sorryhDimstep) — left open, accurate.glReindex/glReindex_coe/reindexAlgEquiv_finCongr_symm_roundcould be generalized beyondℂand hoisted if a second consumer appears — acceptable as local helpers.
Blueprint↔Lean tag sync and prose are out of scope here (handled by the dedicated Blueprint Sync & Prose Review workflow); I resolved the stale bot threads on those points that the current push already addressed.
There was a problem hiding this comment.
Review Summary — PR #2403
Verdict: REQUEST_CHANGES 🔴
One 🔴 blocker persists from the previous review cycle. All other issues have been resolved by the new commits.
What changed since last review
The new push addressed the following issues from the previous review:
- ✅ Blueprint
\notready→\leanokforthm:gaugeConsistency,thm:fundamentalTheorem_PEPS_of_bondDim, andthm:fundamentalTheorem_PEPS(blueprint now matches the Lean signatures with positivity hypotheses) - ✅ Added blueprint entry
thm:peps_exists_edgeGaugeFamilywith\lean{TNLean.PEPS.exists_edgeGaugeFamily}and\leanok - ✅ Fixed "assembles"/"assembly" banned words in module docstring
- ✅ Fixed Lean hypothesis names in docstrings (e.g., "
hDim" → "bond-dimension equality", "hposA/hposB" → "positivity conditions") - ✅ Fixed the contradictory faithfulness claim in
fundamentalTheorem_PEPSdocstring - ✅ Fixed CI unicode error (U+0303 combining tilde in comment)
Resolved 5 bot threads that were addressed by this push.
🔴 Blocker: Proof correctness — simp only does not close the goal
Location: TNLean/PEPS/EdgeGaugeFamily.lean, lines 130–135 (theorem exists_edgeGaugeFamily)
First flagged at inline comment — still unresolved.
The issue: After rw [hProofEq] (line 131), the goal has finCongr (hEdge e) as the outer reindex. But the simp only lemma reindexAlgEquiv_finCongr_symm_round (congr_fun hDim e) (hEdge e) is parameterized with finCongr (congr_fun hDim e) as its outer reindex pattern. After the rewrite, congr_fun hDim e no longer appears in the goal, so the lemma's LHS cannot match any subterm. The map_mul expansion fires, but the round-trip simplification is skipped, leaving an unclosed equality.
The residual goal is:
(Z e) * Matrix.reindexAlgEquiv ℂ ℂ (finCongr (hEdge e)) M * (Z e)⁻¹
=
(Z e) * Matrix.reindexAlgEquiv ℂ ℂ (finCongr (congr_fun hDim e)) M * (Z e)⁻¹
(or, after map_mul, a more complex form with un-simplified round-trip terms)
Fix: Change line 135 from:
reindexAlgEquiv_finCongr_symm_round (congr_fun hDim e) (hEdge e)]to:
reindexAlgEquiv_finCongr_symm_round (hEdge e) (hEdge e)]This one-argument change makes the lemma's LHS match the goal (both use finCongr (hEdge e)) after the rw [hProofEq]. The round-trip terms reindexAlgEquiv ... (finCongr (hEdge e)) (reindexAlgEquiv ... (finCongr (hEdge e).symm) ...) then correctly simplify to the inner matrix.
🔴 Proof integrity — PASS
exists_edgeGaugeFamily: Nosorry,axiom,admit,native_decide,unsafeCast—#print axiomsclean- Pre-existing
sorrys ingaugeConsistencyandfundamentalTheorem_PEPSare unchanged from the base branch and consistent with paper-realignment mode - No circular reasoning, no ungrounded proofs
- No kernel/type-system bypasses
🟡 Mathlib style — PASS
- Naming conventions correct:
glReindex(camelCase def),glReindex_coe(snake_case with_coe),exists_edgeGaugeFamily(snake_case),reindexAlgEquiv_finCongr_symm_round(snake_case) - Scoped
openonly (open scoped BigOperators Matrix) - Tactic style: appropriate use of
choose,refine,rw,simp only(once the lemma parameter is fixed)
🔴 Type safety — PASS
- Universe-polymorphic
V : Type*with[Fintype V]— appropriate glReindexusesUnits.mapEquivcorrectly for theGLtransport- No missing typeclass instances
🟡 Performance — PASS
simp onlywith bounded lemma set — not a timeout risk- No
decideon large types Subsingleton.elim _ _onℕequalities is fast
🟡 Modularity & duplication — PASS
- The three helper lemmas (
glReindex,glReindex_coe,reindexAlgEquiv_finCongr_symm_round) are ℂ-specific, but serve as local scaffolding for the gauge-family construction. The existing advisory about eventual generalization (to[CommRing R]) remains non-blocking.
🟡 Documentation — PASS
- New
exists_edgeGaugeFamilyhas thorough docstring with mathematical context and paper citation (arXiv:1804.04964, Section 3, lines 560–586) - All three helper lemmas have docstrings
- Updated
gaugeConsistency,fundamentalTheorem_PEPS_of_bondDim, andfundamentalTheorem_PEPSdocstrings correctly describe the positivity hypotheses and cite the paper-gap document fundamentalTheorem_PEPSdocstring now correctly distinguishes the positive-bond variant from the source's Theorem 2
ℹ️ Advisory (non-blocking)
- Unused
hposBinfundamentalTheorem_PEPS(line 633):hposBis not consumed in the current proof body, but is the correct symmetric hypothesis for the eventualhDimderivation. The Lean unused-variable linter may flag it. Deliberate placeholder; not a defect. - ℂ-specific helper lemmas:
glReindex,glReindex_coe, andreindexAlgEquiv_finCongr_symm_roundcould be generalized beyond ℂ. Acceptable as local helpers for now.
Resolved threads from previous review
Resolved 5 claude-authored bot threads that were addressed by this push:
PRRT_kwDORK8b986HmDw3:\notready→\leanokforthm:fundamentalTheorem_PEPS_of_bondDimPRRT_kwDORK8b986HmDyo:\notready→\leanokforthm:fundamentalTheorem_PEPSPRRT_kwDORK8b986HmD75:\notready→\leanokforthm:gaugeConsistencyPRRT_kwDORK8b986HmDz3: Lean hypothesis namehDimin docstring → now says "bond-dimension equality"PRRT_kwDORK8b986HmD3N: Lean hypothesis nameshposA/hposBin docstring → now says "positivity conditions"
There was a problem hiding this comment.
Review Summary — PR #2403
Verdict: APPROVE ✅
What the PR does
Adds TNLean/PEPS/EdgeGaugeFamily.lean with a sorry-free (#print axioms-clean) proof of exists_edgeGaugeFamily, which assembles a global per-edge gauge family from the per-edge insertion-algebra isomorphisms (#1367) and Skolem–Noether (edgeGaugeFromInsertionAlgebraIsomorphism). Also applies the #2394 positivity correction to gaugeConsistency, fundamentalTheorem_PEPS_of_bondDim, and fundamentalTheorem_PEPS, adding hpos/hposA/hposB hypotheses throughout the gauge-consistency chain.
Category assessment
| Category | Status |
|---|---|
| 🔴 Proof integrity | Clean. exists_edgeGaugeFamily has no sorry, axiom, or sorryAx. Known sorrys in gaugeConsistency (cross-edge assembly), post_absorption_edge_insertion_equality (#1364), and fundamentalTheorem_PEPS (bond-dimension derivation) are all documented in docstrings and tracked in docs/paper-gaps/peps_injective_ft_section3_route.tex. |
| 🔴 Proof correctness | Correct. The exists_edgeGaugeFamily proof follows a clear structure: block the three-site chains, apply #1367 for the isomorphism, Skolem–Noether for conjugation, and transport gauges back across hDim using glReindex. The Subsingleton.elim unification of equality proofs at line 132 and the subsequent simp with map_mul and the round-trip lemma correctly close the conjugation identity. |
| 🟡 Mathlib style | No issues. Naming follows convention (glReindex camelCase def, exists_edgeGaugeFamily snake_case theorem). open scoped is minimal. |
| 🔴 Type safety | No issues. Universe-polymorphic variables, DecidableRel on graph adjacency, LinearOrder V for edge ordering — all correctly scoped. |
| 🟡 Performance | No issues. simp only with two lemmas, no unbounded simp, decide, or omega on large types. |
| 🟡 Modularity | Acceptable. glReindex/glReindex_coe/reindexAlgEquiv_finCongr_symm_round are ℂ-specific local helpers; generalizing them can wait until a second consumer appears (previously noted as ℹ️ advisory). |
| 🟡 Documentation | Adequate. Module docstring, theorem docstrings with source citations (arXiv:1804.04964, Section 3, lines 560--586), and faithfulness-fix notes on the positive-bond hypothesis. |
| 🟡 Paper-gap notes | No new notes changed. Existing route document is correctly referenced. |
Previous review cycle resolution
All 🔴 and 🟡 issues from prior reviews have been addressed:
- A.1 hypothesis mismatches in blueprint entries → fixed (statements updated,
\leanokapplied) - A.3 stale
\notreadytags → replaced with\leanok - A.4 missing blueprint entry for
exists_edgeGaugeFamily→ added asthm:peps_exists_edgeGaugeFamily - 🔴
simp onlynot closing the goal → fixed withSubsingleton.elimandrw [hProofEq] - 🟡 contradictory faithfulness claim in
fundamentalTheorem_PEPSdocstring → corrected
Three ℹ️-level advisory threads remain unresolved (hposB unused placeholder, ℂ-specific modularity, prose-style note); these are non-blocking.
🤖 Generated with Claude Code
There was a problem hiding this comment.
Blueprint ↔ Lean review — synchronize pass
Category A — equivalence and status
All previously flagged A issues are resolved in this iteration:
thm:peps_exists_edgeGaugeFamily(new entry): statement\leanokis valid — the Lean signature matches the blueprint on all axes (hypotheses, conclusion, algebra-isomorphism type, inserted-coefficient identity, conjugation-transport formula). The proof\leanokis valid: the Lean proof body contains nosorryoradmit(confirmed by grep).thm:gaugeConsistency:\notready→\leanokon statement is correct; positivity hypothesis now present in both blueprint and Lean; no spurious proof\leanok.\usescorrectly addsthm:peps_exists_edgeGaugeFamily.thm:fundamentalTheorem_PEPS_of_bondDim:\notready→\leanokon statement is correct; positivity hypothesis now present in both; no spurious proof\leanok.thm:fundamentalTheorem_PEPS:\notready→\leanokon statement is correct; both positivity hypotheses now in blueprint and Lean;% Scope restrictionLaTeX comment records the faithfulness deviation. No spurious proof\leanok.
0 new Category A issues.
Category B — prose quality
1 open thread (unresolved since prior review):
PRRT_kwDORK8b986HmLDV— "the fundamental-theorem module" in theEdgeGaugeFamily.leanmodule docstring (line 25). This is organizational/implementation language (naming the Lean source file) rather than mathematical content. Not yet fixed.
1 new finding:
- Blueprint proof sketch for
thm:peps_exists_edgeGaugeFamily(lines 2056–2058): two verbal phrases suppress the intermediate conjugation formula ($\Phi_e(M) = Z_e M Z_e^{-1}$ ) and the transport identity ($X_e = \phi_{h_e^{-1}}(Z_e)$). Perdocs/prose_style.md§"Source-faithful terminology and formulas", equations should carry the argument. See inline comment.
Verdict: REQUEST_CHANGES — 1 unresolved B thread + 1 new B finding.
There was a problem hiding this comment.
Review Summary — PR #2403 (re-review on synchronize)
Verdict: APPROVE ✅
All 🔴 and 🟡 issues from the previous review cycle have been addressed. The remaining open threads are ℹ️ advisory or prose-style (the latter handled by the dedicated Blueprint Sync & Prose Review workflow).
Resolution of prior blocking issues
-
🔴 Proof correctness —
exists_edgeGaugeFamilysimp onlynot closing the goal (previously atTNLean/PEPS/EdgeGaugeFamily.lean:136): FIXED. The proof now insertshave hProofEq : congr_fun hDim e = hEdge e := Subsingleton.elim _ _ rw [hProofEq]before the
simp only [map_mul, reindexAlgEquiv_finCongr_symm_round (hEdge e) (hEdge e)]. This unifies the two proofs ofA.bondDim e = B.bondDim e—hEdge e(from Skolem–Noether,edgeGaugeFromInsertionAlgebraIsomorphism) andcongr_fun hDim e(from the global bond-dimension hypothesis) — viaSubsingleton.elimonℕequalities, so the outerfinCongrreindex on the RHS lines up with the inner one. I traced the full goal manually: afterrw [hZ e, hXcoe, hXinvcoe, hProofEq]the RHS isreindexAlgEquiv (finCongr (hEdge e)) (reindexAlgEquiv (finCongr (hEdge e).symm) ↑Z · M · reindexAlgEquiv (finCongr (hEdge e).symm) ↑Z⁻¹);map_muldistributes and the round-trip lemma collapses the first and third factors to↑Zand↑Z⁻¹, matching the LHS↑Z · reindexAlgEquiv (finCongr (hEdge e)) M · ↑Z⁻¹. Correct. -
🟡 Documentation —
fundamentalTheorem_PEPSdocstring contradiction: FIXED. The line "The theorem is stated with the source's hypothesis set" is gone, replaced by the "Positive-bond hypothesis (faithfulness fix)" paragraph and a "Proof status:" paragraph that now consistently states positivity is made explicit to exclude the zero-bond vacuous-SameStatecase.
Category assessment (current state)
-
🔴 Proof integrity — PASS.
exists_edgeGaugeFamilyissorry-free. Thesorrys ingaugeConsistency,post_absorption_edge_insertion_equality, and thehDimstep offundamentalTheorem_PEPSare pre-existing, documented paper-realignment gaps tracking #1364/#1361, with the route recorded indocs/paper-gaps/peps_injective_ft_section3_route.tex. No new undocumentedsorry/axiom/native_decide. -
🔴 Proof correctness — PASS. The construction is sound:
hpos⇒IsVertexInjective.edgeBlockedThreeSiteInjective(KernelDescent.lean:689) for both tensors (hposBderived fromhDim);isEdgeBlockedInsertionAlgebraIsomorphism(#1367,InsertionAlgebra.lean:853) givesΦ_ewith the inserted-coefficient identity;edgeGaugeFromInsertionAlgebraIsomorphism(EdgeGaugeExtraction.lean:30, Skolem–Noether) realizesΦ_easZ_e · reindex M · Z_e⁻¹;glReindex (hEdge e).symmtransportsZ_eto theA-side bond.chooseis used correctly, and the per-edge witnesses are packaged faithfully. -
🔴 Type safety — PASS. The proof-irrelevance of
ℕequalities is handled explicitly (Subsingleton.elim);finCongr/reindexAlgEquivcoercions resolve.glReindex_coeis definitional (rfl). -
🟡 Mathlib style — PASS.
glReindex(def, camelCase),glReindex_coe/reindexAlgEquiv_finCongr_symm_round/exists_edgeGaugeFamily(theorems, snake_case) follow conventions; no over-length lines in the new file or changed regions; no strayopens. -
🟡 Performance — PASS. The proof is short with bounded
simp only. -
🟡 Modularity — Acceptable. The advisory that
glReindexand the round-trip lemma are stated only overℂdespite being field-generic stands as a non-blocking ℹ️ note (existing thread); fine as local helpers. -
🟡 Documentation — PASS. Module docstring and per-declaration docstrings are present and state mathematical content with source citations (arXiv:1804.04964, Section 3).
-
Paper-gap notes — N/A. This PR does not modify
docs/paper-gaps/.
Faithfulness note (informational)
The added positivity hypotheses (hpos/hposA/hposB) make fundamentalTheorem_PEPS a scope-restricted (positive-bond) variant of Theorem 2 of Molnár et al. (arXiv:1804.04964). This is handled per CLAUDE.md §Faithfulness: the blueprint statement explicitly states the restriction, drops the "This is Theorem 2" claim, carries a % Scope restriction comment, and points to the route paper-gap note; the docstring gives the zero-bond vacuous-SameState justification and cites the #1366/#1370 precedent. Compliant.
Remaining open threads (non-blocking)
- ℹ️
hposBis currently unused infundamentalTheorem_PEPS(deliberate placeholder for the still-sorryhDimderivation). - ℹ️
glReindexfamily could be generalized beyondℂif a second consumer appears. - Prose: "fundamental-theorem module" in the
EdgeGaugeFamilymodule docstring (line 25) — out of scope here (Blueprint Sync & Prose Review workflow).
Stacked on #2400. Builds
exists_edgeGaugeFamily(sorry-free,#print axioms-clean): from the proved #1367 per-edge isomorphism + Skolem-NoetheredgeGaugeFromInsertionAlgebraIsomorphism, assembles the global edge-gauge familyX : (e:Edge G)→GL(Fin(A.bondDim e))ℂwith the per-edge conjugation + inserted-coefficient identity. Also applies the #2394 positivity correction togaugeConsistency/fundamentalTheorem_PEPSon this branch.gaugeConsistencystayssorry: its cross-edge assembly into the per-vertex formula depends on #1364 (post-absorption) and #1361 (the Z/U/W two-injective comparison), both open. Refs #1364, #1361.Note
Medium Risk
Changes hypotheses and the formal capstone route for injective PEPS gauge equivalence; the new lemma is proved but
gaugeConsistencyand bond-dimension derivation remain sorry, so callers must match the new positivity assumptions.Overview
Adds
TNLean.PEPS.EdgeGaugeFamilywith a complete proof ofexists_edgeGaugeFamily: from per-edge insertion-algebra isomorphisms (#1367) and Skolem–NoetheredgeGaugeFromInsertionAlgebraIsomorphism, it builds a global edge gauge family on (A)’s bonds with matching inserted coefficients and conjugation formulas for each (\Phi_e), usingglReindexto transport (B)-side gauges across bond-dimension equality.gaugeConsistency,fundamentalTheorem_PEPS_of_bondDim, andfundamentalTheorem_PEPSnow require positive bond dimension on (A) (and both tensors in the main theorem) soSameStateis not vacuous when a bond has dimension zero;gaugeConsistencyremainssorry, with comments thatexists_edgeGaugeFamilycovers the per-edge step and cross-edge assembly still needs #1364 and #1361. The blueprint chapter documents the new theorem and updates gauge/FT statements and proof-status tags accordingly.Reviewed by Cursor Bugbot for commit 35b843d. Bugbot is set up for automated code reviews on this repo. Configure here.