feat(peps): per-edge gauge family from the insertion isomorphism (toward gaugeConsistency)

TNLean.lean

@@ -386,6 +386,7 @@ import TNLean.PEPS.InsertionAlgebra
 import TNLean.PEPS.LocalGauge
 import TNLean.PEPS.TensorFactorScalar
 import TNLean.PEPS.EdgeGaugeExtraction
+import TNLean.PEPS.EdgeGaugeFamily
 import TNLean.PEPS.TwoInjectiveComparison
 -- The PEPS fundamental theorem is an exploratory capstone with recorded
 -- paper-alignment gaps; it is deliberately not part of the default root.

TNLean/PEPS/EdgeGaugeFamily.lean

@@ -0,0 +1,136 @@
+import TNLean.PEPS.Blocking
+import TNLean.PEPS.InsertionAlgebra
+import TNLean.PEPS.EdgeGaugeExtraction
+import TNLean.PEPS.EdgeMiddlePhysical
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
+
+/-!
+# Per-edge gauge family for injective PEPS
+
+This file assembles the per-edge content of the injective PEPS Fundamental
+Theorem (arXiv:1804.04964, Section 3) into one global gauge family.
+
+For each edge `e`, blocking a vertex-injective PEPS around `e` gives a three-site
+injective chain. Comparing two PEPS that generate the same state then yields, via
+`isEdgeBlockedInsertionAlgebraIsomorphism` (#1367), an algebra isomorphism `Φ_e`
+between the two bond matrix algebras whose inserted edge coefficients agree.
+Skolem--Noether (`edgeGaugeFromInsertionAlgebraIsomorphism`) realizes each `Φ_e`
+as conjugation by an invertible bond matrix. Transporting these matrices back to
+the first tensor's bonds across the bond-dimension equality assembles a single
+gauge family `X` and records, edgewise, both the inserted-coefficient identity
+and the conjugation form of `Φ_e`.
+
+This is the construction consumed by `gaugeConsistency` in
+`TNLean/PEPS/FundamentalTheorem.lean`; the remaining cross-edge assembly into the
+per-vertex gauge formula is recorded there and in
+`docs/paper-gaps/peps_injective_ft_section3_route.tex`.
+-/
+
+open scoped BigOperators Matrix
+
+namespace TNLean
+namespace PEPS
+
+variable {V : Type*} [Fintype V] [LinearOrder V]
+variable {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ}
+
+/-- Transport an invertible matrix across an equality of finite index sizes. -/
+noncomputable def glReindex {m n : ℕ} (h : m = n) :
+    GL (Fin m) ℂ ≃* GL (Fin n) ℂ :=
+  Units.mapEquiv (Matrix.reindexAlgEquiv ℂ ℂ (finCongr h)).toRingEquiv.toMulEquiv
+
+/-- The matrix of a transported invertible matrix is the reindexed matrix. -/
+theorem glReindex_coe {m n : ℕ} (h : m = n) (Z : GL (Fin m) ℂ) :
+    (↑(glReindex h Z) : Matrix (Fin n) (Fin n) ℂ) =
+      Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) (↑Z : Matrix (Fin m) (Fin m) ℂ) :=
+  rfl
+
+/-- Reindexing back and forth across an index-size equality is the identity. -/
+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
+  subst h
+  simp
+
+/-- **Per-edge gauge family from the edge-blocked insertion algebra
+isomorphisms.**
+
+For each edge `e`, blocking `A` and `B` around `e` gives three-site injective
+chains (`IsVertexInjective.edgeBlockedThreeSiteInjective`, using the positive
+bond dimensions), and `isEdgeBlockedInsertionAlgebraIsomorphism` (#1367) supplies
+an algebra isomorphism `Φ_e` between the bond matrix algebras whose inserted
+coefficients match. The finite-dimensional algebra step
+`edgeGaugeFromInsertionAlgebraIsomorphism` (Skolem--Noether) realizes each `Φ_e`
+as conjugation by an invertible bond matrix on the `B`-side. Transporting those
+matrices back to the `A`-side bonds across `hDim` assembles a single global gauge
+family `X`, and records, edgewise, both the inserted-coefficient identity and
+that `Φ_e` is conjugation by `X_e`.
+
+This packages the per-edge content of the source proof up to the point where the
+edge gauges are produced. The remaining work in `gaugeConsistency` is the
+cross-edge assembly into the per-vertex formula `B_v = gaugeVertex A X v`, which
+the source obtains from the post-absorption insertion identity
+(`eq:inj_equal_edge`) and the one-vertex-versus-complement comparison; both of
+those steps are tracked separately (see
+`docs/paper-gaps/peps_injective_ft_section3_route.tex`).
+
+Source: arXiv:1804.04964, Section 3, lines 560--586. -/
+theorem exists_edgeGaugeFamily (A B : Tensor G d)
+    (hA : IsVertexInjective A) (hB : IsVertexInjective B)
+    (hAB : SameState A B)
+    (hDim : A.bondDim = B.bondDim)
+    (hpos : ∀ e : Edge G, 0 < A.bondDim e) :
+    ∃ X : (e : Edge G) → GL (Fin (A.bondDim e)) ℂ,
+      ∀ e : Edge G,
+        ∃ Φ :
+          Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ ≃ₐ[ℂ]
+            Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ,
+          (∀ (σ : V → Fin d)
+              (M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ),
+            edgeInsertedCoeff (G := G) A e σ M =
+              edgeInsertedCoeff (G := G) B e σ (Φ M)) ∧
+          ∀ M : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ,
+            Φ M =
+              Matrix.reindexAlgEquiv ℂ ℂ (finCongr (congr_fun hDim e))
+                ((↑(X e) : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) * M *
+                  (↑(X e)⁻¹ : Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ)) := by
+  classical
+  have hposB : ∀ e : Edge G, 0 < B.bondDim e := by
+    intro e; rw [← congr_fun hDim e]; exact hpos e
+  have hAblk : ∀ e : Edge G, EdgeBlockedThreeSiteInjective (G := G) A e :=
+    fun e => hA.edgeBlockedThreeSiteInjective hpos e
+  have hBblk : ∀ e : Edge G, EdgeBlockedThreeSiteInjective (G := G) B e :=
+    fun e => hB.edgeBlockedThreeSiteInjective hposB e
+  have hiso : ∀ e : Edge G, IsEdgeBlockedInsertionAlgebraIsomorphism (G := G) A B e :=
+    fun e =>
+      isEdgeBlockedInsertionAlgebraIsomorphism A B e (hAblk e) (hBblk e) hAB hpos hposB
+  choose Φ hΦcoeff using fun e => (hiso e)
+  -- Skolem--Noether: each `Φ e` is conjugation by an invertible `B`-side matrix.
+  choose hEdge Z hZ using
+    fun e => edgeGaugeFromInsertionAlgebraIsomorphism A B e (Φ e)
+  -- Transport each `Z e` back to the `A`-side bond.
+  refine ⟨fun e => glReindex (hEdge e).symm (Z e), fun e => ⟨Φ e, hΦcoeff e, ?_⟩⟩
+  intro M
+  rw [hZ e]
+  -- Both sides reindex `M` from the `A`-bond to the `B`-bond, conjugated by `Z e`.
+  have hXcoe :
+      (↑(glReindex (hEdge e).symm (Z e)) :
+          Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) =
+        Matrix.reindexAlgEquiv ℂ ℂ (finCongr (hEdge e).symm)
+          (↑(Z e) : Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ) :=
+    glReindex_coe (hEdge e).symm (Z e)
+  have hXinvcoe :
+      (↑(glReindex (hEdge e).symm (Z e))⁻¹ :
+          Matrix (Fin (A.bondDim e)) (Fin (A.bondDim e)) ℂ) =
+        Matrix.reindexAlgEquiv ℂ ℂ (finCongr (hEdge e).symm)
+          (↑(Z e)⁻¹ : Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ) := by
+    rw [← map_inv, glReindex_coe]
+  rw [hXcoe, hXinvcoe]
+  -- `reindexAlgEquiv (finCongr h)` is a ring hom; push it through products, and
+  -- the inner `finCongr (hEdge e).symm` round-trips against the outer reindex.
+  simp only [map_mul,
+    reindexAlgEquiv_finCongr_symm_round (congr_fun hDim e) (hEdge e)]
+
+end PEPS
+end TNLean

TNLean/PEPS/FundamentalTheorem.lean

@@ -577,21 +577,34 @@
 theorem gaugeConsistency (A B : Tensor G d)
     (hA : IsVertexInjective A) (hB : IsVertexInjective B)
     (hAB : SameState A B)
-    (hDim : A.bondDim = B.bondDim) :
+    (hDim : A.bondDim = B.bondDim)
+    (hpos : ∀ e : Edge G, 0 < A.bondDim e) :
     ∃ (X : (e : Edge G) → GL (Fin (A.bondDim e)) ℂ),
       ∀ (v : V) (η : (ie : IncidentEdge G v) → Fin (A.bondDim ie.1)) (σ : Fin d),
         B.component v (fun ie => Fin.cast (congr_fun hDim ie.1) (η ie)) σ =
           gaugeVertex A X v η σ := by
-  -- Derive `BlockedMiddleGaugeFormula A B hA hDim v` from `SameState` at each
-  -- vertex by comparing the edge-blocked coefficient from `PEPS/Blocking` with
-  -- the three-site MPS reduction, then use
-  -- `hasFactorizedLocalGauge_of_blockedMiddleGaugeFormula` to obtain the local
-  -- gauges.
-  -- The key remaining consistency step is: for each edge e = (u,v), the gauges
-  -- extracted from u and v must agree as inverse-transposes, with the
-  -- orientation convention in `edgeGaugeAt`.
-  -- The current status is recorded in
-  -- `docs/paper-gaps/peps_injective_ft_section3_route.tex`.
+  -- The global gauge family `X` is already available, sorry-free, from
+  -- `exists_edgeGaugeFamily A B hA hB hAB hDim hpos`: each edge `e` yields the
+  -- algebra isomorphism `Φ_e` (#1367) realized as conjugation by `X_e`
+  -- (Skolem--Noether, `edgeGaugeFromInsertionAlgebraIsomorphism`).
+  --
+  -- The remaining content is the cross-edge assembly into the per-vertex formula
+  -- `B_v = gaugeVertex A X v`. In the source this is obtained by:
+  --   1. absorbing the edge gauges `X_e` into `B` and proving the post-absorption
+  --      insertion identity `eq:inj_equal_edge`
+  --      (`post_absorption_edge_insertion_equality`, still `sorry`, #1364), and
+  --   2. blocking one vertex against its complement and applying the generalized
+  --      two-injective comparison `inj_equal_tensors_2`
+  --      (`one_vertex_complement_comparison`, which depends on
+  --      `two_injective_tensor_insertion_comparison`, still `sorry`, #1361) to
+  --      get `A_v = λ_v · B̃_v`, absorbing `λ_v` into the edge gauges.
+  -- The per-vertex output is `BlockedMiddleGaugeFormula A B hA hDim v`, which
+  -- `localGauge_exists_of_blockedMiddleGaugeFormula` converts to the local gauge
+  -- relation; the orientation flip to `edgeGaugeAt`/`gaugeVertex` is the last
+  -- bookkeeping step.
+  -- Both load-bearing dependencies (#1364, #1361) are open `sorry`s; the status
+  -- is recorded in `docs/paper-gaps/peps_injective_ft_section3_route.tex`,
+  -- Section "Remaining mathematical obligations".
   sorry
 
 /-! ### Main theorem -/
@@ -609,9 +622,10 @@
 mathematical obligations". -/
 theorem fundamentalTheorem_PEPS_of_bondDim (A B : Tensor G d)
     (hA : IsVertexInjective A) (hB : IsVertexInjective B)
-    (hAB : SameState A B) (hDim : A.bondDim = B.bondDim) :
+    (hAB : SameState A B) (hDim : A.bondDim = B.bondDim)
+    (hpos : ∀ e : Edge G, 0 < A.bondDim e) :
     GaugeEquiv A B := by
-  rcases gaugeConsistency A B hA hB hAB hDim with ⟨X, hX⟩
+  rcases gaugeConsistency A B hA hB hAB hDim hpos with ⟨X, hX⟩
   exact ⟨hDim, X, hX⟩
 
 /-- **Fundamental Theorem for injective PEPS** (arXiv:1804.04964, Theorem 2).
@@ -621,13 +635,25 @@
 `X_e` such that, at every vertex, `B_v` is obtained from `A_v` by the oriented
 endpoint action of the matrices `X_e` on the incident virtual legs.
 
+**Positive-bond hypothesis (faithfulness fix).** Without `hposA`/`hposB` the
+theorem is false: a zero-dimensional edge makes the virtual configuration empty,
+so both state coefficients vanish and `SameState` holds vacuously without
+relating the two tensors, while the gauge-equivalence conclusion stays a genuine
+constraint that fails. The hypotheses (every bond dimension positive) are the
+source's standing assumption that injective PEPS have nonzero virtual bond
+spaces; the same defect was corrected for the edge-blocked three-site
+injectivity (#1366) and the physical-to-virtual recovery (#1370), and is
+recorded in `docs/paper-gaps/peps_injective_ft_section3_route.tex`.
+
 **Proof status:** The theorem is stated with the source's hypothesis set. The
 remaining bond-dimension and edge-centred gauge obligations are recorded in
 `docs/paper-gaps/peps_injective_ft_section3_route.tex`, Section "Remaining
 mathematical obligations". -/
 theorem fundamentalTheorem_PEPS (A B : Tensor G d)
     (hA : IsVertexInjective A) (hB : IsVertexInjective B)
-    (hAB : SameState A B) :
+    (hAB : SameState A B)
+    (hposA : ∀ e : Edge G, 0 < A.bondDim e)
+    (hposB : ∀ e : Edge G, 0 < B.bondDim e) :
     GaugeEquiv A B := by
   -- Bond-dimension equality should follow from the full family of boundary
   -- insertions. Linear independence at each vertex (`IsVertexInjective`) gives
@@ -638,7 +664,7 @@
   have hDim : A.bondDim = B.bondDim := by
     sorry
   -- With matching bond dimensions, `gaugeConsistency` supplies the global gauges.
-  exact fundamentalTheorem_PEPS_of_bondDim A B hA hB hAB hDim
+  exact fundamentalTheorem_PEPS_of_bondDim A B hA hB hAB hDim hposA
 
 /-! ### Balanced edge scalars -/
 
@@ -972,7 +998,7 @@
       edgeGaugeProduct_eq_of_gaugeVertex_eq (G := G) A hA v X Y (hGauge v) η η'
   -- From `hProd v` at each vertex `v`, extract a nonzero scalar `c_v(ie)` on
   -- each incident edge such that `edgeGaugeAt A X v ie = c_v(ie) • edgeGaugeAt A Y v ie`
   -- with the oriented product of `c_v(ie)` over incident `ie` at `v` equal to
   -- `1`, then reconcile `c_u` and `c_w` on every shared edge `e = (u,w)` into a
   -- single global family `c : (e : Edge G) → Units ℂ` satisfying
   -- `IsVertexBalanced c`. This is the local scalar-ratio argument of