Palomar solution

This module exposes the canonical proof for the Palomar challenge. The theorem and its proof live in LeanSuperorthogonality.MainTheorem, as Superorthogonal.sqfct_estimate_of_type_iv_superorthogonal. Keeping this module import-only ensures that Comparator checks the actual formalization rather than a duplicate wrapper theorem.

It provides the proof of Theorem 1 of Philip T. Gressman, Lillian B. Pierce, Joris Roos, and Po-Lam Yung, A new type of superorthogonality, Proceedings of the American Mathematical Society 152 (2024), no. 2, 665--675. doi:10.1090/proc/16631.