The Turán number ex(41;C4) equals 132

For a positive integer n, ex(n;C4) is the maximum number of edges of a graph on n vertices with no cycle of length four. Exact values are known for all n <= 40, and 132 <= ex(41;C4) <= 133. We prove ex(41;C4) = 132, which settles the smallest open case. The proof combines counting arguments with exhaustive SAT computations certified by LRAT proofs. A 133-edge graph would have all degrees in {6,7,8}. Without a vertex of degree 8, codegree counting reduces the problem to two finite searches. A vertex of degree 8 leads to an exact rooted model with 239 symmetry-reduced cubes; a global codegree count excludes 32 of them, and the other 207 are refuted by the solver with proofs checked by lrat-check. This record contains the manuscript (PDF) and the supplementary archive (a zip file in five parts; see JOIN.txt): the lower-bound graphs and their check, the count checks, the case ledgers, encoders and counter-completeness check of the searches without a vertex of degree 8, the 239 cubes of the rooted model with their encoders, the per-cube table and the audit evidence, a re-check of 28 sample proofs with two checkers, positive controls of the cube encoder, and the solver and checker binaries with their digests, with a SHA-256 manifest and instructions for reproducing every computation. MSC2020: 05C35 (primary); 05C38, 68V15 (secondary)