PEPS FT: formalize the generalized two-injective-tensor comparison

[LionSR]

Goal

Formalize the generalized two-injective-tensor comparison used in arXiv:1804.04964, Section 3, Lemma inj_equal_tensors_2.

The paper proves that if two pairs of injective tensors agree after inserting an arbitrary matrix on every shared virtual bond, then the corresponding tensors are proportional with inverse scalar factors:

A_1 = lambda * B_1,
A_2 = lambda^{-1} * B_2.

The scalar-reduction substep in this proof is tracked separately by #1362. This issue is the enclosing two-tensor comparison used after eq:inj_equal_edge from #1364, before the final one-vertex-versus-complement specialization tracked by #1360.

Blueprint target

The current worktree adds a not-yet-formalized blueprint node:

thm:peps_twoInjectiveTensorInsertionComparison

and a semantic diagram macro:

\TNPEPSTwoInjectiveTensorInsertionComparison

The diagram depicts two injective tensors joined by several shared virtual bonds, with an arbitrary matrix X inserted on one such bond, matching the displayed hypothesis of lem:inj_equal_tensors_2.

The proof substep #1362 is represented by:

thm:peps_twoInjectiveGaugeScalarReduction
\TNPEPSTwoInjectiveGaugeScalarReduction

Dependencies

• PEPS FT: formalize scalar reduction in the two-injective-tensor comparison #1362 for the scalar-reduction substep in the proof;
• PEPS FT: formalize the post-absorption edge insertion equality #1364 for the post-absorption insertion equality eq:inj_equal_edge that supplies the insertion equality on PEPS edges;
• PEPS: build virtual-insertion and blocking infrastructure for the remaining Fundamental Theorem theorems #763 for graph blocking and virtual-insertion infrastructure;
• PEPS FT: formalize the final one-vertex versus complement comparison #1360 for the downstream application to one vertex versus its complement;
• PEPS: local gauge existence, consistency, and main theorem assembly #780 for final theorem assembly.

Acceptance criteria

• State the Lean theorem corresponding to thm:peps_twoInjectiveTensorInsertionComparison with arbitrary matrix insertions on shared virtual bonds.
• The theorem assumes injectivity of both tensor blocks, not merely equality of fully contracted scalar states.
• The conclusion gives reciprocal scalar proportionality of the two tensors.
• The proof follows the argument of lem:inj_equal_tensors_2, using the scalar-reduction substep PEPS FT: formalize scalar reduction in the two-injective-tensor comparison #1362 to reduce the possible remaining virtual gauges to scalar multiples of the identity.
• No new untracked sorry is introduced outside this theorem endpoint.
• Chapter 13a keeps the diagram attached to this theorem node.

[LionSR]

Initial blueprint and diagram representation is now present in the worktree:

• blueprint/src/chapter/ch13a_peps_ft.tex contains thm:peps_twoInjectiveTensorInsertionComparison as a separate not-ready theorem node.
• blueprint/src/macros/tn_print.tex contains \TNPEPSTwoInjectiveTensorInsertionComparison.
• blueprint/src/Packages/tn_diagrams.py registers the macro.
• docs/paper-gaps/peps_injective_ft_section3_route.tex lists this theorem as the generalized comparison needed before the one-vertex-versus-complement step PEPS FT: formalize the final one-vertex versus complement comparison #1360.

The issue is attached as a native subissue of #1252. This is not yet a Lean theorem; it is the paper-faithful blueprint target and diagram split for the next formalization step.

[LionSR]

Dependency refinement:

The scalar-reduction substep in the proof of lem:inj_equal_tensors_2 has been split out as #1362. The blueprint node thm:peps_twoInjectiveTensorInsertionComparison now depends on thm:peps_twoInjectiveGaugeScalarReduction.

This mirrors the source proof more closely: after the insertion comparison and inversion of one injective block, residual operators Z, U, W appear on pairs of exposed virtual legs; #1362 is the theorem that these residual operators are scalar, allowing the reciprocal proportionality conclusion in this issue.