feat(peps): close two_injective_tensor_insertion_comparison (#1361) (#2406)

* feat(PEPS): dispatch empty-bond vacuous case of two-injective comparison

Split two_injective_tensor_insertion_comparison into the empty-config
vacuous branch (twoBlockReciprocalScalarProportional_of_isEmpty_config)
and a nonempty-bond core (two_injective_tensor_insertion_comparison_core,
still sorry). The empty case picks c=1; all configs are absent.

Refs #1361.

* feat(PEPS): open-leg matrix-unit insertion extraction

Add twoBlockInsertedCoeff_matrixUnit: inserting the matrix unit E_{p,q}
on bond b yields the open-b contraction sum (other bonds traced by the
identity, bond b carrying row p / column q). Generalizes
twoBlockInsertedCoeff_singletonBond_single to a multi-bond family; the
open-leg equality is the entry point for the Z,U,W inversion route.

Refs #1361.

* feat(PEPS): one-leg-open equality from per-bond insertions

Add sameOpenBondContraction: SameTwoBlockInsertions yields equality of
all one-leg-open contractions (open bond b, trace the rest) for the
A-pair and B-pair. This is the first reduction of the source proof of
lem:inj_equal_tensors_2 (the displayed open-leg equalities), feeding the
A2-inversion that reads off the Z,U,W gauges.

Refs #1361.

* doc(PEPS): record committed reductions and remaining inversion gap

Update two_injective_tensor_insertion_comparison_core docstring to cite
the committed building blocks (twoBlockInsertedCoeff_matrixUnit,
sameOpenBondContraction) and state the precise remaining obstruction: the
two-leg-open equalities do not follow linearly from the one-leg-open ones
and require a left inverse of A2 (then B1) to extract Z,U,W.

Refs #1361.

* feat(PEPS): add inversion helpers for two-injective comparison

Add reusable sorry-free building blocks toward
two_injective_tensor_insertion_comparison_core (arXiv:1804.04964
lem:inj_equal_tensors_2):
- twoBlockInsertedCoeff_one / fullContraction_eq: identity-insertion gives
  the all-bonds diagonal contraction equality
- twoBlockComb / twoBlockComb_injective / twoBlockLeftInverse: the left
  inverse of an injective two-block tensor (the paper's inverse of A2)

The _core sorry is unchanged.

* feat(PEPS): close operator-Schmidt bond-gauge lemma (#1361)

Prove exists_bondGauge_of_fullContraction: from the full-contraction
identity and injectivity of A1,A2,B1,B2, produce an invertible gauge
matrix g on the shared-bond configurations with A1 = g·B1 and B2 = gᵀ·A2.
This is the operator-Schmidt uniqueness linchpin for
two_injective_tensor_insertion_comparison_core (arXiv:1804.04964 Lemma
inj_equal_tensors_2, lines 1157-1204).

Supporting lemmas (all sorry-free, axioms = propext/Classical.choice/Quot.sound):
- IsTwoBlockInjective.config_linearIndependent: config-indexed independence
  bridge from joint injectivity
- exists_dual_isolating: dual functional isolating one member of an
  independent finite family
- gauge_eq1 / gauge_eq2: the two gauge equations from bipartite uniqueness
- gauge_inv: mutual-inverse of the forward and backward gauges (g*g'=1)

_core remains sorry (matrix-gauge to scalar via threeLeg_residual_forms_scalar
is a separate step).

* feat(PEPS): close two_injective_tensor_insertion_comparison (#1361)

Discharge the residual-operator step of the generalized two-injective
tensor comparison (arXiv:1804.04964, Section 3, Lemma inj_equal_tensors_2).

From the bond gauge produced by exists_bondGauge_of_fullContraction, the
one-leg-open contraction identities (sameOpenBondContraction) plus the two
gauge equations are separated over the linearly independent families B1 and A2
to give a master per-bond constraint on the gauge g. Iterating that constraint
over all shared bonds forces g to be a nonzero scalar multiple of the identity,
yielding A1 = lam B1 and A2 = lam^{-1} B2.

New lemmas: bilinear_coeff_zero, reindex_update, bondGauge_master_constraint,
bondGauge_scalar_of_master.

Closes two_injective_tensor_insertion_comparison_core and the public
two_injective_tensor_insertion_comparison; no sorryAx in either
(#print axioms = propext, Classical.choice, Quot.sound).

Blueprint thm:peps_twoInjectiveTensorInsertionComparison proof marked leanok.

* feat(PEPS): close bond-dimension equality (#874) via edge-blocked algebra equivalence

Discharge the hDim sorry in fundamentalTheorem_PEPS edgewise: edgeTransferAlgEquiv
packages matched matrix insertions on each bond as an algebra equivalence between
the two full bond matrix algebras, and bondDim_eq_of_matrixAlgEquiv forces equal
index sizes by the dimension count m*m = n*n. Axiom-clean.

* feat(PEPS): global open form of inserted-edge coefficient

Add the cast-free global open form of edgeInsertedCoeff: a sum over the
two open bond indices, the inserted-matrix weight, and a free complement
configuration on all other edges (insertedOpenConfigEquiv,
edgeInsertedCoeff_eq_sum_complement). This is the open-edge analog of
virtualConfigEquivEdgeBoundary used in the post-absorption edge-insertion
identity (arXiv:1804.04964, Section 3).

* feat(PEPS): local-configuration form of inserted-edge coefficient

Add the OpenLocalConfig delta form of edgeInsertedCoeff
(edgeInsertedCoeff_eq_sum_local) together with the off-edge consistency
machinery (IsConsistentOff, consistentOffEquivDoubled, localOfDoubled) and
the endpoint/middle bridges. The delta on every edge other than e filters
to configurations consistent off e, the open-edge analog of
sum_local_with_edge_deltas.

* feat(PEPS): open-edge gauge sum cancellation

Add the core open-edge gauge cancellation (open_gauge_sum_over_outer) and
its supporting pieces (prod_gaugeVertex_eq_sum_local_open,
prod_edgeGaugeAt_eq_prod_edge, localOfDoubled edge-value lemmas). Summing
the gauge factors over the outer configuration, weighted by the inserted
matrix and constrained by consistency off e, cancels the gauges on every
other edge and conjugates the inserted matrix by the open-edge gauge
(X_e)ᵀ. This is the open-edge analog of gauge_sum_over_virtual.

* feat(PEPS): edgeInsertedCoeff_applyGauge (open-edge gauge cancellation)

Prove edgeInsertedCoeff_applyGauge: applying an oriented edge-gauge family
Z to a PEPS tensor and inserting N on edge e equals inserting the
conjugated matrix (Z_e)ᵀ N ((Z_e)⁻¹)ᵀ on the ungauged tensor. Internal-edge
gauges cancel pairwise; the two endpoint gauges on the open edge conjugate
the inserted matrix by the transpose of the open-edge gauge. This is the
open-edge analog of applyGauge_stateCoeff, a linchpin for the
post-absorption edge-insertion identity (#1364) toward the injective PEPS
Fundamental Theorem (arXiv:1804.04964, Section 3, eq:inj_equal_edge).

Axioms: only [propext, Classical.choice, Quot.sound].

* doc(PEPS): record edgeInsertedCoeff_applyGauge linchpin in #1364

Document in post_absorption_edge_insertion_equality that the open-edge
gauge action is now available sorry-free from edgeInsertedCoeff_applyGauge,
and that the remaining obstruction is the positive-bond-dimension hypothesis
required by exists_edgeGaugeFamily but absent from this statement (not
implied by IsVertexInjective).

* feat(PEPS): add GL-transpose and reindex-transpose helpers

Add `glTranspose` (transpose of an invertible bond matrix as a `GL`
element), its matrix and inverse-matrix coercion lemmas, and
`reindexAlgEquiv_transpose` (reindexing commutes with transposition).
These package the conjugation bookkeeping needed to absorb the transpose
of the per-edge gauge family into the second PEPS tensor.

* feat(PEPS): close post_absorption_edge_insertion_equality (#1364)

Prove the post-absorption edge insertion equality. The per-edge gauge
family X on the A-side bonds comes from `exists_edgeGaugeFamily`;
absorbing the transpose of X_e (transported across hDim) into B makes the
open-edge gauge action conjugate each inserted matrix by (X_e)ᵀ, matching
the insertion-algebra transport's conjugation by X_e.

Add the positive-bond hypothesis `hpos : ∀ e, 0 < A.bondDim e` to the
signature, the same faithfulness fix already applied to the sibling
chain (`fundamentalTheorem_PEPS`, `gaugeConsistency`); without it the
edge-blocking step into a three-site injective chain is unavailable.
Documented in docs/paper-gaps/peps_injective_ft_section3_route.tex.

`exists_edgeGaugeFamily` is now imported, which enlarges the environment
and tips two pre-existing combinatorial `simpa` proofs over the default
heartbeat budget; raise it locally for that section.

Update the blueprint statement to record the positive-bond restriction
and mark the proof \leanok. Axioms: only propext, Classical.choice,
Quot.sound (no sorryAx).

* feat(PEPS): one-vertex two-block tensor wrapping + injectivity

Wrap the tensor at a fixed vertex `v` as an abstract `TwoBlockTensor` over
the shared bonds `IncidentEdge G v` (one-point external boundary, physical
leg `Fin d`), and derive its `IsTwoBlockInjective` directly from vertex
injectivity by reindexing along `PUnit × X ≃ X`. First glue lemma of the
concrete to abstract bridge feeding `one_vertex_complement_comparison`
(arXiv:1804.04964, Section 3, lines 1205-1210).

* doc(PEPS): record precise gaugeConsistency translation gap

Correct the stale in-proof note (two_injective_tensor_insertion_comparison
is now proved, #1361) and itemize the three remaining load-bearing steps:
(1) the concrete vertex/complement two-block matching to edgeInsertedCoeff,
(2) vertex-complement region injectivity (V minus v; only the edge-middle
block is formalized), and (3) gauge inversion plus per-vertex scalar
absorption into a balanced edge-scalar reweighting.

* feat(PEPS): vertex-complement region tensor definitions

Add the V\{v} complement block opened along the v-star (IncidentEdge G v)
as the shared boundary: VertexComplementConfig, vertexComplementValue,
vertexComplementWeight, vertexComplementTensorFamily, and the injectivity
predicate VertexComplementTensorInjective.

Parallels EdgeMiddlePhysical.Basic with the vertex star as the open
boundary. Step toward closing the vertex-complement injectivity input of
one_vertex_complement_comparison (arXiv:1804.04964 Section 3, lines
1205-1210). Refs #1361.

* feat(PEPS): vertex-complement kernel-descent scaffolding

Reformulate the V\{v} complement weight as a fiber sum over global virtual
configurations restricting to the v-star label. Add the per-complement-vertex
split equivalence vertexConfigSplitAt, the exposed-agreement indicator, the
guarded local factor, and the stagewise kernel condition.

Mirrors EdgeMiddlePhysical.KernelDescent with the v-star as the open
boundary. Refs #1361.

* feat(PEPS): vertex-complement kernel-condition erase-vertex step

Add the descent implication K_c(S) => K_c(S\{j}) for a complement vertex
j != v, via the per-complement-vertex split and the one-sided inverse at j
(localCoeff_eq_zero_of_contract_zero). Includes the exposed/extra indicator
factorization and the marginal coefficient vanishing.

Mirrors edgeMiddleKernelCondition_erase. Refs #1361.

* feat(PEPS): vertex-complement terminal kernel relation

Add the empty-region step K_c(emptyset) => c = 0: the v-star witness
configuration (positive bonds fill non-star edges) collapses the empty-region
kernel sum to a single coefficient. Mirrors
edgeMiddleKernelCondition_empty_eq_zero. Refs #1361.

* feat(PEPS): vertex-complement tensor family is linearly independent

Assemble the kernel-descent datum (initial / erase / terminal steps) and
prove vertexComplementTensorInjective_of_isVertexInjective: the contraction
of injective tensors over V\{v} is injective, under positive bond dimensions.

Mirrors edgeMiddleKernelDescentData. Refs #1361.

* feat(PEPS): vertex-complement two-block injectivity

Add complementTwoBlock (the V\{v} contraction viewed as a TwoBlockTensor over
the v-star IncidentEdge G v with one-point external boundary and physical leg
on V\{v}) and isTwoBlockInjective_complementTwoBlock, the second injectivity
input of one_vertex_complement_comparison. Bridges the kernel-descent
linear independence through the PUnit-product reindexing, paralleling
isTwoBlockInjective_vertexTwoBlock. Wire the new module into the root import
graph. Refs #1361.

* doc(PEPS): record vertex-complement injectivity closure

Update the gaugeConsistency remaining-obligations comment and the paper-gap
note: the V\{v} complement-block injectivity (step 2 of
one_vertex_complement_comparison's inputs) is now formalized via
isTwoBlockInjective_complementTwoBlock and the star-boundary kernel descent.
Refs #1361.

* feat(PEPS): vertex injectivity of the absorbed tensor family

* doc(peps): add vertex two-block blueprint entries

* feat(PEPS): two-block coefficient as a global virtual-configuration sum

* refactor(peps): split oversized comparison files

* feat(PEPS): collapse the constrained v-star sum and split global configs

* fix(peps): address two-injective comparison review

* feat(PEPS): two-block coefficient identity for both edge orientations

* doc(peps): address blueprint prose review

* refactor(peps): split one-vertex comparison module

* feat(PEPS): unified two-block coefficient identity over incident edges

* style(peps): finish two-injective comparison review fixes

* feat(PEPS): SameTwoBlockInsertions from the edge-insertion equality

* fix(peps): move comparison imports to one-vertex module

* doc(PEPS): note algebra relocation for Schmidt lemmas

* doc(peps): record connectivity gap refuting gauge consistency

gaugeConsistency (and the headline fundamentalTheorem_PEPS) asserts one
global edge-gauge family relates two same-state injective PEPS tensors.
This is false without a connectivity hypothesis: on the empty graph over
Bool, two vertex-injective tensors with equal state and vacuously positive
bond dimensions need not be equal, yet the empty edge-gauge family forces
equality. The per-vertex scalar reduction is sorry-free; the remaining
edge-scalar absorption is solvable only on a connected graph.

The refutation was machine-checked and axiom-clean (no sorryAx). Documents
the existence-clause gap, distinct from the uniqueness-clause balanced
edge-scalar gap.

* feat(PEPS): machine-check gaugeConsistency connectivity counterexample

* fix(PEPS): add connectivity hypothesis to gaugeConsistency and PEPS FT

gaugeConsistency and fundamentalTheorem_PEPS are false on a disconnected
graph: the per-vertex scalars from the source reduction are absorbable into
edge gauges only when their reciprocal product is 1 on each connected
component, which the state equality forces only for a connected graph. Add
G.Connected to gaugeConsistency, fundamentalTheorem_PEPS, and
fundamentalTheorem_PEPS_of_bondDim, threading it through. Positivity is kept.
gaugeConsistency stays sorry (spanning-tree edge-scalar solve is the
follow-up). Refutation machine-checked in
GaugeConsistencyConnectivityCounterexample. Documented in
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex.

* fix(PEPS): import GaugeAction not the orphan capstone in connectivity counterexample

* doc(peps): avoid proof-token words in connectivity note

* doc(peps): address complement-block blueprint review

* doc(peps): address gauge-action prose review

* feat(PEPS): oriented edge-scalar incidence and product-one necessity

Introduce the oriented incidence product of an edge-scalar family on a simple
graph (edgeScalarUnit / orientedIncidence) and prove the necessity direction of
the absorption solvability condition: the product of the oriented incidences
over all vertices is 1 (prod_orientedIncidence_eq_one), since each edge cancels
its own scalar against its inverse across its two endpoints.

This is the consistency obstruction recorded in
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex and the foundation
for the spanning-tree edge-scalar existence step of gaugeConsistency.

* feat(PEPS): edge transfer for vertex deletion in edge-scalar solve

Add the combinatorial infrastructure for the induction step of the spanning-tree
edge-scalar existence proof: lift/restrict edges between G and G.induce {v0}ᶜ
(liftEdge / restrictEdge), the incidence bijection incEquiv between v0-avoiding
incident edges of a vertex w in G and the incident edges of w in the deleted
subgraph, and prod_free_eq showing the v0-free part of w's oriented incidence
product equals the deleted-subgraph oriented incidence of the lifted scalars.

These are the load-bearing helpers for the vertex-deletion recursion of
gaugeConsistency's absorption step.

* feat(PEPS): spanning-tree edge-scalar existence on a connected graph

Prove exists_edgeScalars_of_connected: on a connected simple graph, any
vertex-scalar family t : V → ℂˣ with ∏ t = 1 is the oriented incidence product
of an edge-scalar family. This is the spanning-tree coboundary step of the
absorption argument in the injective PEPS Fundamental Theorem
(arXiv:1804.04964 §3), documented in
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex.

The proof is by induction on the number of vertices, removing a non-cut vertex
v₀ (SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial),
folding v₀'s target into a neighbor, recursing on the deleted subgraph, and
absorbing v₀'s scalar into the single edge {v₀,w₀}. Axiom-clean
(propext, Classical.choice, Quot.sound).

* feat(PEPS): per-vertex scalar and reindex injectivity for gaugeConsistency

Add two sorry-free lemmas toward closing gaugeConsistency:
- isVertexInjective_reindexTensor: bond-dimension reindexing preserves vertex
  injectivity (the local family precomposed with an injective index recast).
- perVertexScalar: at every vertex with a nonempty incident-edge set, the
  post-absorption edge-insertion equality plus the four two-block injectivity
  facts and one_vertex_complement_comparison yield a nonzero c with
  A_v = c · gaugeVertex B Z v.

This realizes the per-vertex scalar step of arXiv:1804.04964 §3 documented in
docs/paper-gaps/peps_gaugeConsistency_connectivity_gap.tex. gaugeConsistency
itself remains sorry pending the gauge-inversion / edge-scalar assembly.

* doc(PEPS): record precise remaining gaugeConsistency obligations

Update the gaugeConsistency proof-status comment to reference the now-available
perVertexScalar and exists_edgeScalars_of_connected, and to name the two
remaining obligations precisely: (1) ∏ c_v = 1 via gauge-state invariance, and
(2) the gauge-inversion product-kernel collapse packaging X_e = s_e·(Z_e)⁻¹.

* doc(peps): document vertex-complement indicator split

* doc(peps): document gauge-action helper lemmas

---------

Co-authored-by: Sirui Lu <lion.sr@icloud.com>

Author: LionSR

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

@@ -53,6 +53,41 @@ theorem reindexAlgEquiv_finCongr_symm_round {m n : ℕ} (h h' : m = n)
   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.**