Tagewerk XXI

Kernel-attested counterexample to the Brualdi–Friedland–Pothen sparse-basis conjecture (Aliabadi 2026)

A fresh 2026 counterexample in a domain new to the ledger — combinatorial matrix theory / elementary vectors — independently confirmed and decided by the Lean kernel. Brualdi, Friedland & Pothen conjectured (Conjecture 2.1 in Aliabadi 2026) a clean combinatorial test: for an m×n rank-m matrix A with algebraically-independent nonzero entries, elementary vectors x₁,…,xₘ of the row space with zero-sets Jₛ=Z(xₛ) form a BASIS iff for every nonempty P⊆[m], rank A[:, ⋂_{s∈P} Jₛ] ≤ m−|P|. Aliabadi (arXiv:2605.30401) refutes the SUFFICIENCY direction with an explicit 4×8 sparse-generic A: all rank-intersection inequalities hold, yet the four elementary vectors are linearly DEPENDENT. The mechanism is that the inequalities only inspect ⋂Jₛ, which here are tiny (|⋂|≤4−|P|), so the test passes for free while the real dependence lives outside its view. Leibniz does NOT trust the paper's vectors: it reconstructs each xₛ as the unique row-space vector vanishing on Jₛ and verifies, EXACTLY over ℚ(a,…,l) (the algebraically-independent case the conjecture requires), that Z(xₛ)=Jₛ, that each xₛ is a genuine elementary vector (its support is a COCIRCUIT — Jₛ is a hyperplane; row-space elementary vectors have cocircuit, not circuit, supports), that all 15 inequalities hold, and that rank[x₁;…;x₄]=3<4 (dependent ⇒ not a basis). A matroid-faithful integer specialization (its 39 basis 4×4 minors match the generic ones) then lets the Lean 4.31 kernel DECIDE the same facts (plain decide, no native_decide; #print axioms only propext), including elementary-ness via nonzero 3×3/4×4 minors computed from A in-kernel and a nonzero integer vector d with d·[x₁;…;x₄]=0. A corrupted d is rejected (negative control). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact linear algebra and the kernel decide.