feat(peps): close the injective PEPS Fundamental Theorem (positivity + connectivity faithful)

TNLean.lean

@@ -372,6 +372,8 @@ import TNLean.PEPS.VirtualInsertion
 import TNLean.PEPS.SingletonRegion
 import TNLean.PEPS.Blocking
 import TNLean.PEPS.EdgeMiddlePhysical
+import TNLean.PEPS.VertexComplement.Basic
+import TNLean.PEPS.VertexComplement.KernelDescent
 import TNLean.PEPS.NormalEdgeBlockingData
 import TNLean.PEPS.NormalBlocking
 import TNLean.PEPS.SquareLatticeGraph
@@ -389,5 +391,7 @@ import TNLean.PEPS.TensorFactorScalar
 import TNLean.PEPS.EdgeGaugeExtraction
 import TNLean.PEPS.EdgeGaugeFamily
 import TNLean.PEPS.TwoInjectiveComparison
+import TNLean.PEPS.EdgeScalarSolve
+import TNLean.PEPS.GaugeConsistencyConnectivityCounterexample
 -- 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

@@ -46,13 +46,48 @@
   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
 
+/-- The transpose of an invertible matrix, packaged as an invertible matrix. The
+inverse is the transpose of the inverse, since transposition is an
+anti-homomorphism. -/
+def glTranspose {m : ℕ} (X : GL (Fin m) ℂ) : GL (Fin m) ℂ where
+  val := (↑X : Matrix (Fin m) (Fin m) ℂ)ᵀ
+  inv := (↑X⁻¹ : Matrix (Fin m) (Fin m) ℂ)ᵀ
+  val_inv := by
+    rw [← Matrix.transpose_mul, ← Units.val_mul, inv_mul_cancel, Units.val_one,
+      Matrix.transpose_one]
+  inv_val := by
+    rw [← Matrix.transpose_mul, ← Units.val_mul, mul_inv_cancel, Units.val_one,
+      Matrix.transpose_one]
+
+/-- The matrix of `glTranspose X` is the transpose of the matrix of `X`. -/
+theorem glTranspose_coe {m : ℕ} (X : GL (Fin m) ℂ) :
+    (↑(glTranspose X) : Matrix (Fin m) (Fin m) ℂ) =
+      (↑X : Matrix (Fin m) (Fin m) ℂ)ᵀ :=
+  rfl
+
+/-- The matrix of `(glTranspose X)⁻¹` is the transpose of the inverse of `X`. -/
+theorem glTranspose_inv_coe {m : ℕ} (X : GL (Fin m) ℂ) :
+    (↑(glTranspose X)⁻¹ : Matrix (Fin m) (Fin m) ℂ) =
+      (↑X⁻¹ : Matrix (Fin m) (Fin m) ℂ)ᵀ := by
+  rw [Matrix.GeneralLinearGroup.coe_inv, glTranspose_coe,
+    ← Matrix.transpose_nonsing_inv, Matrix.GeneralLinearGroup.coe_inv]
+
+/-- Reindexing commutes with transposition: `reindexAlgEquiv` along a single index
+equivalence sends a transpose to the transpose of the reindexed matrix. -/
+theorem reindexAlgEquiv_transpose {m n : ℕ} (h : m = n)
+    (N : Matrix (Fin m) (Fin m) ℂ) :
+    Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) Nᵀ =
+      (Matrix.reindexAlgEquiv ℂ ℂ (finCongr h) N)ᵀ := by
+  simp only [Matrix.reindexAlgEquiv_apply, Matrix.reindex_apply,
+    Matrix.transpose_submatrix]
+
 /-- **Per-edge gauge family from the edge-blocked insertion algebra
 isomorphisms.**