Partial Proof of a Conjecture with Implications for Spectral Majorization

In this paper we report new developments based on the proven cases of a surprising conjecture relating to special properties of n n positive definite (PD) matrices for n 6. It is argued in [8] that traditional mathematics has focused primarily on results that hold generally for all n, whereas most theoretical physics models, and most applied mathematics and engineering problems, are intrinsically defined in a fixed (and small) number of dimensions, e.g., time and the three spatial dimensions of ordinary experience. What is not commonly recognized is that as soon the dimensionality of a problem becomes fixed, e.g., to 3 dimensions, opportunities exist to establish potentially useful properties of the system of interest that do not hold generally in higher dimensions. Unfortunately, proving such properties typically requires computer-assisted methods that are not familiar to most scientists, mathematicians, and engineers. In Section 2, we illustrate these statements by showing how the IRGA conjecture for n 3 is relatively straightforward to establish by hand, while proof of the n = 4 case was accomplished using powerful computer-assisted proof methods. We discuss why such methods are likely required, and why proofs for the remaining n = 5 and n = 6 cases are likely beyond the capabilities of current state-of-the-art methods on even the most powerful supercomputers. In Section 3, we describe how proven cases of the IRGA conjecture define a fixed-dimensional family of matrices for which the diagonal majorizes the spectrum [9]. In Section 4, we present new results showing that Kronecker products of these matrices retain this unique majorization property. Then, in Section 5, we conclude with considerations on the imminent arrival of AI-based theorem provers, which can be viewed as proof oracles rather than computer-assisted tools.