Proposition 12.6 -- nonsingularity of a mixed matrix

Open

DiscreteConvex.MixedMatrices.mixed_matrix_nonsingular_iff

by Shuze Chen · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracombinatoricsdiscrete-convex-analysis

Proposition 12.6 (p.357). A square mixed matrix $A = Q + T$ is nonsingular if and only if there exist $I \subseteq R$ and $J \subseteq C$ such that both $Q[I,J]$ and $T[R\setminus I, C\setminus J]$ are nonsingular.

This is the combinatorial certificate underlying every later result of the chapter: it reduces the (numerically delicate) nonsingularity of a matrix mixing exact and generic entries to a combinatorial search over row/column splits, each half checked in its own, easier arithmetic (numeric determinant for $Q$ , a bipartite matching argument for $T$ , since $T$ 's entries are free parameters).

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.357, Proposition 12.6.)

Preamble

import Mathlib
import Definitions.Def_DiscreteConvex_MixedMatrices_IsMixedMatrix
import Definitions.Def_DiscreteConvex_MixedMatrices_IsNonsingularSub

Formal statement

namespace DiscreteConvex.MixedMatrices

/-- Proposition 12.6 (Murota, *Discrete Convex Analysis*, SIAM 2003, p.357). A square mixed
matrix `A = Q + T` is nonsingular if and only if there exist `I ⊆ R` and `J ⊆ C` such that both
`Q[I,J]` and `T[R\I,C\J]` are nonsingular. -/
theorem mixed_matrix_nonsingular_iff {R C K F : Type*} [Fintype R] [Fintype C] [Field K] [Field F]
    [Algebra K F] [DecidableEq R] [DecidableEq C]
    (A : Matrix R C F) (Q : Matrix R C K) (T : Matrix R C F) (hA : IsMixedMatrix A Q T)
    (hsq : Fintype.card R = Fintype.card C) :
    IsNonsingularSub A (Finset.univ : Finset R) (Finset.univ : Finset C) ↔
      ∃ I : Finset R, ∃ J : Finset C, IsNonsingularSub Q I J ∧ IsNonsingularSub T Iᶜ Jᶜ := by sorry

end DiscreteConvex.MixedMatrices

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.357, Proposition 12.6

Human review

Endorsed by Community (Bot) · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph