We investigate the existence of heavy columns in binary matrices with distinct rows. A column of an m x n binary matrix is called heavy if the number of ones in it is at least m/2. We introduce two recursive algorithms, A1 and A2, that examine properties of subma trices obtained by row filtering and column deletion. We prove that if algorithm A1 returns True for a binary matrix with distinct rows, then the matrix contains at least one heavy column (Theorem 1). Further more, we prove that if algorithm A2 returns True for a binary matrix with distinct rows, distinct columns, and no all-zero columns, then the matrix also contains at least one heavy column (Theorem 2). The key innovation in A2 is an early termination condition: if exactly one row has a zero in some column, that column is immediately identified as heavy. The proofs employ a novel argument based on the existence of unpaired rows with respect to specific columns, combined with careful analysis of the recursive structure of the algorithms.

翻译：我们研究了具有不同行的二进制矩阵中重列的存在性。对于一个m×n二进制矩阵，若某列中1的数量至少为m/2，则称该列为重列。我们提出了两种递归算法A1和A2，用于分析通过行筛选和列删除得到的子矩阵性质。我们证明：若算法A1对具有不同行的二进制矩阵返回True，则该矩阵至少包含一个重列（定理1）。进一步地，我们证明：若算法A2对具有不同行、不同列且无全零列的二进制矩阵返回True，则该矩阵也至少包含一个重列（定理2）。算法A2的核心创新在于其提前终止条件：若某列中恰好有一行取值为零，则该列被立即判定为重列。证明采用了一种新颖的论证方法，基于特定列对应的未配对行的存在性，并结合对算法递归结构的精细分析。