The cardinality spectrum of quantum Latin squares of order seven

Abstract

This deposit contains the manuscript, exact algebraic certificates, and complete Lean 4 formalization settling the cardinality spectrum of quantum Latin squares of order seven. We show that the possible cardinalities for order seven are exactly {7, 9, 10, ..., 49}, with 8 excluded. Explicit constructions are provided for all twenty previously open cardinalities (24 through 42, and 45). All twenty corresponding existence statements are formalized and kernel-checked in Lean 4 with mathlib. GitHub repository: https://github.com/Theophilus1030/QLS7