Lean 4 kernel check of the S(6) ≥ 537 partition of Chen, Zhu and Long

A Lean 4 kernel check (decide +kernel, no native_decide, Lean core only) of the partition of {1, ..., 537} into six sum-free sets published by Z. Chen, L. Zhu and F. Long in "A new lower bound for the sixth Schur number: S(6) ≥ 537" (arXiv:2610.31362v1, ancillary file certificate.col, sha256 5f950ad88a5437108a0c6ab4b9d40cc2832a43dd474b5c4b269e02ac81258315). The partition and the bound are the authors'; this upload checks the partition and states no bound of its own. The theorem schur6_partition_537 states, over six bit masks, that the masks are pairwise disjoint, that their union is exactly {1, ..., 537}, and that no mask contains y and y + x for any x in it, so each class is sum-free. Here S(k) is the largest n such that {1, ..., n} splits into k sum-free sets; OEIS A030126 lists S(k) + 1. There is no Lean definition of S(k). Axioms: [propext]. A negative control (1, 2, 3 in one colour) fails in the kernel. certificate.col is licensed CC BY 4.0 by its authors and is included unchanged. Nothing here concerns the exact value of S(6) or the further bounds the paper derives.