Problem 20 Goal — Transpose injectivity semiring
ProvedRybinAI2026.P20.transpose_injectivity_semiringFor every natural number (including ), every type equipped with a chosen unital commutative-semiring structure, and every matrix with entries in and row and column indices , the following two conditions are equivalent. The first condition is that left multiplication by is injective on column vectors: for all functions , if for every , then for every . The second condition is that left multiplication by the transpose of is injective: for all functions , if for every , then for every . All sums, products, zeros, and ones are those of the chosen commutative-semiring structure, and transposition means exactly that the entry in position becomes . No nontriviality, finiteness of , additive inverses, cancellation, integral-domain, or field assumption is imposed on , and no condition is imposed on . In particular, semirings with are included; when is a subsingleton, every such vector type is a subsingleton and both maps are automatically injective. When , the index set is empty, every displayed sum is the empty sum , there is exactly one vector , and both maps are injective. The assertion is a biconditional, so each injectivity condition implies the other; it does not assert that the two matrix-vector maps are equal or that either one is injective without the other being injective.
import Mathlib
namespace RybinAI2026.P20
/-- Injectivity of a square matrix over a unital commutative semiring is invariant under
transpose. The theorem is stated for every finite size, including the source problem's first
open case `n = 3`. -/
theorem transpose_injectivity_semiring
{R : Type*} [CommSemiring R] {n : ℕ}
(A : Matrix (Fin n) (Fin n) R) :
Function.Injective A.mulVec ↔ Function.Injective A.transpose.mulVec := by
sorry
end RybinAI2026.P20Read-back
What the Lean code literally says, in plain math · gpt-5.6-sol
For every natural number (including ), every type equipped with a chosen unital commutative-semiring structure, and every matrix with entries in and row and column indices , the following two conditions are equivalent. The first condition is that left multiplication by is injective on column vectors: for all functions , if for every , then for every . The second condition is that left multiplication by the transpose of is injective: for all functions , if for every , then for every . All sums, products, zeros, and ones are those of the chosen commutative-semiring structure, and transposition means exactly that the entry in position becomes . No nontriviality, finiteness of , additive inverses, cancellation, integral-domain, or field assumption is imposed on , and no condition is imposed on . In particular, semirings with are included; when is a subsingleton, every such vector type is a subsingleton and both maps are automatically injective. When , the index set is empty, every displayed sum is the empty sum , there is exactly one vector , and both maps are injective. The assertion is a biconditional, so each injectivity condition implies the other; it does not assert that the two matrix-vector maps are equal or that either one is injective without the other being injective.
Confirmed by the mission captain (proposal self-audit).