PEPS: bond-dimension equality from SameState and vertex injectivity

[LionSR]

Context

This is a focused sorry-elimination issue for the PEPS main theorem assembly.

Target direct sorry on current origin/main:

TNLean/PEPS/FundamentalTheorem.lean:569
the `hDim : A.bondDim = B.bondDim` step inside `TNLean.PEPS.fundamentalTheorem_PEPS`

The other live PEPS sorries are already tracked by #820 / #780 (gaugeConsistency) and #842 (gauge_unique_mod_edge_scalars). This issue isolates the bond-dimension equality needed before gaugeConsistency can be applied in the final theorem.

Concrete target

Prove that if two vertex-injective PEPS tensors have the same state family, then their bond-dimension functions agree:

A.bondDim = B.bondDim

The proof should use the boundary-insertion / graph-blocking infrastructure from #763 and the virtual-insertion helpers landed in #809, not just the fully contracted scalar SameState alone.

Notes

The in-code comment explicitly says the missing ingredient is a boundary-insertion / blocking lemma: SameState as currently stated captures the fully-contracted scalar, while the PEPS FT derivation of bond-dimension equality uses a family of boundary insertions plus vertex injectivity.

Validation

• lake env lean TNLean/PEPS/FundamentalTheorem.lean
• no new sorry in TNLean/PEPS/FundamentalTheorem.lean

Refs #128 #763 #780 #820

[LionSR]

@claude auto fix

Please pick this up from the issue body and open a focused PR from main for #874.

Keep the PR scoped to this issue, reference #874 in the PR body, and avoid introducing any new sorry, admit, axiom, native_decide, or proof-integrity workaround. If the statement is false or blocked by a dependency that is not yet on main, make the smallest useful preparatory PR or report the precise Lean-level blocker instead of adding placeholder proofs.

Use the repository conventions in docs/pr_review_management.md, docs/style.md, docs/doc.md, and the relevant blueprint style guide. Run targeted lake build checks for touched Lean modules, and run cd blueprint && leanblueprint checkdecls whenever blueprint declarations or tags are changed.

[claude]

Claude finished @LionSR's task in 5m 38s —— View job

---

Lean-level blocker report: hDim inside fundamentalTheorem_PEPS

• Read TNLean/PEPS/FundamentalTheorem.lean around line 569
• Survey PEPS virtual-insertion / blocking infrastructure on main (TNLean/PEPS/{VirtualInsertion,Blocking,LocalGauge}.lean)
• Inspect SameState, IsVertexInjective, and bondDim in TNLean/PEPS/Defs.lean
• Confirm the blocked-middle / three-site-MPS reduction from arXiv:1804.04964 §3 is not on main
• Decide path: report precise blocker (not open a code PR)

Summary

After reviewing the target sorry and the surrounding infrastructure, I am not opening a code PR for #874, because closing the hDim step honestly requires exactly the same blocked-middle / three-site-MPS reduction that is still tracked as open work in #763, and which issue #874 itself flags as "the missing ingredient". Any non-trivial proof I could add today would either be a placeholder for that reduction or would re-introduce the same sorry under a different name, both of which the trigger instructions explicitly forbid.

Per the instruction to "report the precise Lean-level blocker instead of adding placeholder proofs", here is the precise gap.

Target

-- TNLean/PEPS/FundamentalTheorem.lean:568-569
have hDim : A.bondDim = B.bondDim := by
  sorry

Context (from the same theorem):

theorem fundamentalTheorem_PEPS (A B : Tensor G d)
    (hA : IsVertexInjective A) (hB : IsVertexInjective B)
    (hAB : SameState A B) :
    GaugeEquiv A B := by
  ...
  have hDim : A.bondDim = B.bondDim := by sorry
  ...

Goal: A.bondDim = B.bondDim as functions Edge G → ℕ, i.e. ∀ e : Edge G, A.bondDim e = B.bondDim e.

What is actually available on main

The inputs we are allowed to use are:

• SameState A B : ∀ σ : V → Fin d, stateCoeff A σ = stateCoeff B σ, where stateCoeff is the fully contracted scalar TNLean/PEPS/Defs.lean:60-63.
• IsVertexInjective A : ∀ v, LinearIndependent ℂ (A.component v) (TNLean/PEPS/Defs.lean:85-86).
• Local helpers from feat(PEPS): virtual-insertion and graph-blocking infrastructure (#763) #809 in TNLean/PEPS/VirtualInsertion.lean: localTensorMap, IsVertexInjective.localTensorMap_injective, localLeftInverse, physRealizeLocalOp, localProjector.
• Edge-centered decompositions from feat(PEPS): virtual-insertion and graph-blocking infrastructure (#763) #809 in TNLean/PEPS/Blocking.lean: localVirtualConfigSplitAt, edgeLeftVertices, edgeMiddleVertices, edgeRightVertices, edgeVertices_union.
• Gauge-consuming contraction algebra from the same file: applyGauge_stateCoeff, GaugeEquiv.sameState, prod_gaugeVertex_eq_sum_local, sum_local_with_edge_deltas, …

What the proof mathematically requires (arXiv:1804.04964, §3)

For a fixed edge e = (u, v), the bond dimension A.bondDim e is recovered as the rank of the blocked-middle 3-site tensor obtained by contracting every vertex not in {u, v} and leaving the edge e itself uncontracted. Concretely:

1. Blocked-middle tensor: using edgeVertices_union to partition V = {u} ⊔ (V \ {u,v}) ⊔ {v}, form the 3-site object
   blocked A e : M_u × M_mid × M_v → ℂ
   where the left and right "physical-plus-virtual" legs carry (σ_u, η|_{incident(u)\{e}}) and (σ_v, η|_{incident(v)\{e}}), and the middle leg is the fully contracted middle block. The virtual leg corresponding to e is left open.
2. Injectivity transfer: vertex injectivity IsVertexInjective A plus the edge-centered star decomposition in TNLean/PEPS/Blocking.lean is expected to imply that the blocked 3-site tensor is an injective MPS in the sense of TNLean.MPS.FundamentalTheorem.
3. SameState transfer: SameState A B (the fully contracted scalar equality) needs to be refined, via the boundary-insertion / blocking argument, to SameState of the blocked 3-site objects.
4. Apply the 1D MPS FT: the injective-MPS bond-isomorphism conclusion (1D hDim for the middle leg) then forces A.bondDim e = B.bondDim e at each e.

Why none of these four steps is expressible on current main

• No definition of the blocked-middle tensor exists yet. edgeMiddleVertices gives the index set; there is no Lean object blocked A e on main yet.
• No injectivity-transfer lemma from IsVertexInjective to 1D-MPS injectivity on the blocked object.
• No boundary-inserted form of SameState: SameState as defined in TNLean/PEPS/Defs.lean captures only the fully contracted scalar; there is no lemma on main that upgrades it to an open-bond comparison. This is explicitly the missing ingredient called out in the in-code comment on lines 562-567.
• No bridge to TNLean.MPS.FundamentalTheorem for the resulting 3-site object.

All four of these are the deliverables of issue #763 ("PEPS: build virtual-insertion and blocking infrastructure for the remaining Fundamental Theorem theorems"), which is still OPEN. PR #809 landed the per-vertex linear-algebra piece and the elementary edge-centered partitions, but the blocked-middle tensor, its injectivity transfer, and the blocked-SameState bridge are still open.

Why the shallow bound is not enough

From IsVertexInjective A alone one can prove the vertex-local dimension bound

∀ v, ∏ ie : IncidentEdge G v, A.bondDim ie.1 ≤ d

via LinearIndependent.fintype_card_le_finrank (Mathlib/LinearAlgebra/Dimension/Finite.lean:161-164) combined with Fintype.card_pi and Module.finrank_fin_fun. I considered landing exactly this as a "smallest useful preparatory PR". I chose not to, for two reasons:

• It yields only an upper bound on each vertex's local virtual dimension, not the pointwise equality A.bondDim e = B.bondDim e. It does not replace any of the four missing steps above.
• It can be added later as a one-liner once the blocked-middle tensor is in place, so landing it now does not reduce the eventual diff and does not change the critical-path dependency on PEPS: build virtual-insertion and blocking infrastructure for the remaining Fundamental Theorem theorems #763.

Landing it preemptively would amount to shipping a lemma whose only consumer is the missing blocking infrastructure, which violates the "smallest useful" criterion and would be churn rather than progress.

No statement change

Before flagging the blocker I also checked whether the existing target statement is possibly too strong — e.g. whether A.bondDim = B.bondDim as functions is forced by the current definition of SameState. It is, in the MPS (path-graph) case and more generally under the paper's hypotheses; the bondedge-by-bondedge argument in arXiv:1804.04964 §3 does give pointwise equality. So no restatement of fundamentalTheorem_PEPS is appropriate — the statement is correct, but its proof requires #763.

Recommendation

Keep this issue open, parented to #763. Once the blocked-middle tensor and its SameState-transfer lemma land from #763, hDim becomes a short rank/bond-isomorphism consequence of the 1D MPS Fundamental Theorem applied edge-by-edge.

No commits on claude/issue-874-formalizationpeps-prove-bond-dimension-equality-from. Working tree is clean against main.
· branch: claude/issue-874-formalizationpeps-prove-bond-dimension-equality-from