The Colomo–Pronko conjecture for frozen-corner alternating sign matrices

We prove the Colomo–Pronko conjecture for alternating sign matrices with a prescribed square of zeros at a corner, for all matrix sizes and freezing parameters. A known multiple-integral formula for the frozen-corner count is reduced to determinant representations built from fixed polynomial kernels, which are then related to the conjectured determinant through an inverse identity for the commutator of a signed Pascal matrix with reversal. The odd-dimensional case is handled through its one-dimensional nullspace and a central projection. Combined with the asymptotic analysis of Colomo and Pronko, the result removes the conjectural assumption from their GUE Tracy–Widom fluctuation theorem for the intersection of the frozen boundary with the main diagonal in uniformly random alternating sign matrices. The finite-dimensional algebraic core of the proof has been formalized in Lean 4. The supplementary material and the Lean source package are included with this record.