Catalysts from additive completion certificates

Equality in the Grothendieck additive group means equality after adding a common element of the original semiring. This gives catalytic inequalities without assuming additive cancellation.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_catalyst_of_completion_eq {S : Type u_1} [CommSemiring S] [Preorder S] (hadd : ∀ (a b c d : S), a ≤ b → c ≤ d → a + c ≤ b + d) (m k : ℕ) (d X Y s : S) (hXY : X ≤ Y) (heq : -↑m • Algebra.GrothendieckAddGroup.of 1 = Algebra.GrothendieckAddGroup.of Y - Algebra.GrothendieckAddGroup.of X + Algebra.GrothendieckAddGroup.of (d * s) - k • Algebra.GrothendieckAddGroup.of s) : ∃ (D : S), D + ↑m + d * s ≤ D + ↑k * s

A negative-unit certificate in the additive completion gives a catalytic inequality in the original semiring, even when its addition is not cancellative.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_catalyst_of_completion_sum_eq {S : Type u_1} [CommSemiring S] [Preorder S] (hadd : ∀ (a b c d : S), a ≤ b → c ≤ d → a + c ≤ b + d) {I : Type u_2} [Fintype I] (m k : ℕ) (d : S) (n : I → ℕ) (X Y Z : I → S) (hXY : ∀ (i : I), X i ≤ Y i) (heq : -↑m • Algebra.GrothendieckAddGroup.of 1 = ∑ i : I, n i • (Algebra.GrothendieckAddGroup.of (Y i) - Algebra.GrothendieckAddGroup.of (X i) + Algebra.GrothendieckAddGroup.of (d * Z i) - k • Algebra.GrothendieckAddGroup.of (Z i))) : ∃ (D : S), D + ↑m + d * ∑ i : I, n i • Z i ≤ D + ↑k * ∑ i : I, n i • Z i

A finite nonnegative integral combination of completion relations gives one catalytic inequality. The catalyst absorbs the aggregate of the ordered relations, and the resulting test element is the same combination of the original test elements.