Summand separation from transpose injectivity

Proved

RybinAI2026.P20.summand_separation

by ryanshin · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

injectivitylinear-algebrasemirings

Let $R$ be a commutative semiring with identity, let $n\ge 2$ , and let $A=(a_{ij})$ be an $n\times n$ matrix. Assume that $x\mapsto A^T x$ is injective. If vectors $x,y\in R^n$ satisfy $Ax=Ay$ , then every matrix summand agrees separately:

a_{pq}x_q=a_{pq}y_q\qquad\text{for all rows }p\text{ and columns }q.

This is the unital specialization of the source's summand separation lemma. Together with one-column separation, it yields transpose symmetry of injectivity over arbitrary commutative semirings with identity.

Preamble

import Mathlib.Data.Matrix.Mul

Formal statement

theorem RybinAI2026.P20.summand_separation
    {R : Type*} [CommSemiring R] {n : Nat} (hn : 2 <= n)
    (A : Matrix (Fin n) (Fin n) R)
    (hA : Function.Injective A.transpose.mulVec)
    (x y : Fin n -> R) (hxy : A.mulVec x = A.mulVec y) :
    forall p q, A p q * x q = A p q * y q := by sorry

Source

Sixuan Gu, Wei Qi, Yaoyu Cheng, Transpose Symmetry of Injectivity over Commutative Semirings, arXiv:2608.16205v1 (2026), Section 3, Lemma 3 (Summand separation), equations (3.1)-(3.8). https://arxiv.org/html/2608.16205v1

View graph