Exact Nonmultiplicativity of Binary Rank under Kronecker Products

The binary rank of a zero-one matrix is the minimum number of pairwise disjoint all-one rectangles that partition its one-support. We give a proof-producing order-five counterexample to multiplicativity under Kronecker products. For an explicit 5-by-5 matrix A, brank(A) = 5 and brank(A ⊗ A) = brank(A ⊗ Aᵀ) = 24 < 25. Both upper bounds are given by explicit 24-rectangle partitions. Both lower bounds are certified by separately regenerated and independently clause-audited exact-23 SAT encodings together with complete checked DRAT refutations. We also derive exact padded families, an exact symmetric self-square with brank(S) = 10 and brank(S ⊗ S) = 96, integral multicover identities, finite higher-power bounds, and fractional asymptotic bounds. The result was obtained independently. During manuscript preparation, we learned that Yaroslav Shitov had publicly posted a different counterexample first. We make no claim to first public resolution. The present work emphasizes exact product ranks, infinite families, a same-factor and symmetric counterexample, and complete reproducible proof closure. This deposit contains the manuscript and LaTeX source, literal partition certificates, exact-23 CNF formulas, complete DRAT refutations, independent Python and JavaScript verifiers, mutation tests, exact arithmetic checks, and a strict manifest. From the extracted archive, running python verify.py replays every theorem-bearing computational claim. Research and proof-development assistance was provided by GPT-5.6 Sol Ultra. Licensing is component-specific: the manuscript, documentation, certificates, and data are CC BY 4.0; project-authored source code is MIT licensed; bundled third-party code retains its upstream license. See LICENSES.md in the archive.