Nonsingular minors: dominant weights and block-diagonal minors

Two certificates that a square matrix is nonsingular, or that a matrix has large rank.

• Dominance. A nonempty sum ∑ ±2^{E x} with pairwise distinct exponents is nonzero (Algebraic.sum_mul_two_pow_ne_zero): the term with the least exponent is not divisible by the next power of 2, while all the others are.
• Doubly exponential weights. Let M be a square matrix over a commutative ring of characteristic zero whose nonzero entries are ±2^{2^{L i j}}, where the labels L i j of the nonzero entries are pairwise distinct, and suppose some permutation σ has M (σ j) j ≠ 0 for every j (the support of M contains a perfect matching). Then det M ≠ 0 (Matrix.det_ne_zero_of_two_pow_two_pow). Each permutation supported on the nonzero entries contributes ±2^{E σ} to the Leibniz expansion with E σ = ∑_j 2^{L (σ j) j}, the binary number whose set bits are the labels used by σ; distinct labels make these exponents pairwise distinct, and dominance applies.
• Block-diagonal minors. If rows f i b and columns g i b of A, indexed by i : ι within each block b : β, give nonsingular square blocks and all entries between different blocks vanish, then card ι * card β ≤ rank A (Matrix.card_mul_card_le_rank_of_det_blocks_ne_zero).

theorem Algebraic.sum_mul_two_pow_ne_zero {κ : Type u_1} {s : Finset κ} (hs : s.Nonempty) {ε : κ → ℤ} (hε : ∀ x ∈ s, IsUnit (ε x)) {E : κ → ℕ} (hE : Set.InjOn E ↑s) : ∑ x ∈ s, ε x * 2 ^ E x ≠ 0

Dominance. A nonempty sum ∑ ε x * 2 ^ E x with unit coefficients ε x = ±1 and pairwise distinct exponents E x is nonzero.

theorem Matrix.det_ne_zero_of_two_pow_two_pow {R : Type u_1} [CommRing R] [CharZero R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) (L : ι → ι → ℕ) (hM : ∀ (i j : ι), M i j ≠ 0 → M i j = 2 ^ 2 ^ L i j ∨ M i j = -2 ^ 2 ^ L i j) (hL : ∀ (i j i' j' : ι), M i j ≠ 0 → M i' j' ≠ 0 → L i j = L i' j' → i = i' ∧ j = j') (σ : Equiv.Perm ι) (hσ : ∀ (j : ι), M (σ j) j ≠ 0) : M.det ≠ 0

Nonsingularity from doubly exponential weights. Let M be a square matrix over a commutative ring of characteristic zero whose nonzero entries are ±2^{2^{L i j}}, with labels L i j that are pairwise distinct on the nonzero entries. If some permutation σ has M (σ j) j ≠ 0 for every j, then det M ≠ 0.

theorem Matrix.card_mul_card_le_rank_of_det_blocks_ne_zero {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] {ι : Type u_4} {β : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] (A : Matrix m n K) (f : ι → β → m) (g : ι → β → n) (hoff : ∀ (i i' : ι) (b b' : β), b ≠ b' → A (f i b) (g i' b') = 0) (hdet : ∀ (b : β), (A.submatrix (fun (x : ι) => f x b) fun (x : ι) => g x b).det ≠ 0) : Fintype.card ι * Fintype.card β ≤ A.rank

Block-diagonal minors. Choose, for each block b : β, rows f i b and columns g i b of A indexed by i : ι. If every entry between different blocks vanishes and every block A.submatrix (f · b) (g · b) is nonsingular, then card ι * card β ≤ rank A.