doc(peps): mark gauge statements formalized

Author: Sirui Lu

TNLean/PEPS/EdgeGaugeFamily.lean

@@ -20,9 +20,9 @@ the first tensor's bonds across the bond-dimension equality gives 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 passage to the
-per-vertex gauge formula is recorded there and in
+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
 `docs/paper-gaps/peps_injective_ft_section3_route.tex`.
 -/
 
@@ -63,13 +63,13 @@ 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` gives a single global gauge
-family `X`, and records, edgewise, both the inserted-coefficient identity and
+matrices back to the \(A\)-side bonds across the bond-dimension equality gives
+a single global gauge family, and records, edgewise, both the inserted-coefficient identity and
 that `Φ_e` is conjugation by `X_e`.
 
 This records 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 passage to the per-vertex formula `B_v = gaugeVertex A X v`, which
+edge gauges are produced. The remaining work in gauge consistency is the
+cross-edge passage to the per-vertex formula \(B_v = X\cdot A_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
@@ -127,6 +127,8 @@ theorem exists_edgeGaugeFamily (A B : Tensor G d)
           (↑(Z e)⁻¹ : Matrix (Fin (B.bondDim e)) (Fin (B.bondDim e)) ℂ) := by
     rw [← map_inv, glReindex_coe]
   rw [hXcoe, hXinvcoe]
+  have hProofEq : congr_fun hDim e = hEdge e := Subsingleton.elim _ _
+  rw [hProofEq]
   -- `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,

TNLean/PEPS/FundamentalTheorem.lean

@@ -548,9 +548,10 @@ theorem localGauge_exists (A B : Tensor G d)
 
 /-- Post-absorption edge insertion equality from arXiv:1804.04964, Section 3,
 lines 1037--1065. Assuming the separately tracked bond-dimension equality
-`hDim` (#874), the edge gauges obtained from the three-site comparison can be
-absorbed into `B` so that every edge insertion in `A` agrees with the transported
-edge insertion in the absorbed tensor family. The remaining proof is #1364. -/
+(\#874), the edge gauges obtained from the three-site comparison can be absorbed
+into the second tensor family so that every edge insertion in \(A\) agrees with
+the transported edge insertion in the absorbed tensor family. The remaining
+proof is #1364. -/
 theorem post_absorption_edge_insertion_equality (A B : Tensor G d)
     (hA : IsVertexInjective A) (hB : IsVertexInjective B) (hAB : SameState A B)
     (hDim : A.bondDim = B.bondDim) :
@@ -610,7 +611,7 @@ and have the same state coefficients, then there are invertible edge matrices
 `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
+**Positive-bond hypothesis (faithfulness fix).** Without the positivity conditions 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
@@ -639,7 +640,7 @@ theorem fundamentalTheorem_PEPS (A B : Tensor G d)
   -- `docs/paper-gaps/peps_injective_ft_section3_route.tex`.
   have hDim : A.bondDim = B.bondDim := by
     sorry
-  -- With matching bond dimensions, `gaugeConsistency` supplies the global gauges.
+  -- With matching bond dimensions, gauge consistency supplies the global gauges.
   exact fundamentalTheorem_PEPS_of_bondDim A B hA hB hAB hDim hposA
 
 /-! ### Balanced edge scalars -/

blueprint/src/chapter/ch13a_peps_ft.tex

@@ -2251,7 +2251,7 @@ \chapter{Fundamental Theorems for Injective and Normal PEPS}%
 \begin{theorem}[Gauge consistency]%
     \label{thm:gaugeConsistency}
     \lean{TNLean.PEPS.gaugeConsistency}
-    \notready
+    \leanok
     \uses{thm:peps_exists_edgeGaugeFamily,
         thm:peps_postAbsorptionEdgeInsertionEquality,
         thm:localGauge_exists, def:gaugeVertex}
@@ -2690,7 +2690,7 @@ \chapter{Fundamental Theorems for Injective and Normal PEPS}%
         bond-dimension equality]%
     \label{thm:fundamentalTheorem_PEPS_of_bondDim}
     \lean{TNLean.PEPS.fundamentalTheorem_PEPS_of_bondDim}
-    \notready
+    \leanok
     \uses{thm:gaugeConsistency, thm:peps_oneVertexComplementComparison,
         def:GaugeEquivPEPS, def:IsVertexInjective}
     Suppose that the corresponding virtual edge spaces of $A$ and $B$ are
@@ -2704,7 +2704,7 @@ \chapter{Fundamental Theorems for Injective and Normal PEPS}%
 \begin{theorem}[Fundamental Theorem for injective PEPS]%
     \label{thm:fundamentalTheorem_PEPS}
     \lean{TNLean.PEPS.fundamentalTheorem_PEPS}
-    \notready
+    \leanok
     % Scope restriction: this is the positive-bond variant of Theorem 2 in
     % \cite{Molnar2018NormalPEPS}. The elimination plan for the positivity
     % hypotheses is recorded in