The Bruck–Ryser–Chowla theorem for projective planes

If a finite projective plane of order n exists (Mathlib's Configuration.ProjectivePlane) and n ≡ 1 or 2 (mod 4), then n is a sum of two squares; in particular there are no planes of order 6 or 14. With points and lines matched by a bijection, the incidence matrix scales the dot product of zero-sum vectors by n (two points lie on n + 1 common lines if equal and on one otherwise). Padding to dimension n² + n + 2 ≡ 0 (mod 4), Lagrange's four squares (Nat.sum_four_squares) and Euler's 4×4 blocks give a rational M with M Mᵀ = n I. An isometry-extension lemma for the standard form on ℚⁿ (a case of Witt's theorem, by reflections) then yields a vector of squared length n constant on lines, i.e. n = d² + (n² + n + 1) c² with rational c, d; a descent modulo primes q ≡ 3 (mod 4) and Nat.eq_sq_add_sq_iff turn this into two integer squares.

Main results

• BruckRyserChowla.exists_sq_add_sq: projective plane of order n = 1, 2 mod 4: n is a sum of two squares
• BruckRyserChowla.exists_isometry: extension of isometries for the standard form on Q^n (a case of Witt)
• BruckRyserChowla.exists_orthogonal_vector: a rational vector of squared length n constant on the lines
• BruckRyserChowla.exists_sq_add_sq_of_rat: n z^2 = x^2 + y^2 over Q with z != 0 gives n a sum of two integer squares

References

• R. H. Bruck and H. J. Ryser, The nonexistence of certain finite projective planes, Canad. J. Math. 1 (1949), 88–93.
• S. Chowla and H. J. Ryser, Combinatorial problems, Canad. J. Math. 2 (1950), 93–99.
• Witt's extension theorem in general (not used here) is in facebookresearch/atlas-lean, v1/Atlas/Buildings/code/GeometricAlgebra/ExtendingIsometries.lean.

Part B: extension of finite families of isometries on ι → ℚ (Witt-style)

theorem BruckRyserChowla.exists_isometry {ι : Type u_1} {κ : Type u_2} [Fintype ι] (s : List κ) (u v : κ → ι → ℚ) (h : ∀ a ∈ s, ∀ b ∈ s, u a ⬝ᵥ u b = v a ⬝ᵥ v b) : ∃ (O : (ι → ℚ) → ι → ℚ), (∀ (x y : ι → ℚ), O x ⬝ᵥ O y = x ⬝ᵥ y) ∧ ∀ a ∈ s, O (u a) = v a

Finite families with equal Gram matrices are related by an isometry of ι → ℚ.

Part C: Euler's four-square similarity on ι → ℚ when 4 ∣ card ι

theorem BruckRyserChowla.exists_orthogonal_vector {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] (n : ℕ) (h4 : 4 ∣ Fintype.card ι) (u g : κ → ι → ℚ) (ε : ι → ℚ) (hG : ∀ (a b : κ), u a ⬝ᵥ u b = ↑n * g a ⬝ᵥ g b) (hε : ∀ (a : κ), ε ⬝ᵥ u a = 0) (hε1 : ε ⬝ᵥ ε = 1) : ∃ (r : ι → ℚ), (∀ (a : κ), r ⬝ᵥ g a = 0) ∧ r ⬝ᵥ r = ↑n

Algebraic core. Let u a and g a be families in ι → ℚ, with 4 ∣ card ι, such that the Gram matrix of u is n times that of g, and let ε be a unit vector orthogonal to all u a. Then some vector of squared norm n is orthogonal to all g a.

Part A: n = d² + v c² over ℚ with v ≡ 1 (mod q) forces even valuations

theorem BruckRyserChowla.exists_sq_add_sq_of_rat (n : ℕ) (c d : ℚ) (h : ↑n = d ^ 2 + (↑n ^ 2 + ↑n + 1) * c ^ 2) : ∃ (a : ℕ) (b : ℕ), n = a ^ 2 + b ^ 2

If n = d² + (n² + n + 1) c² with c d rational, then n is a sum of two squares.

Part D: the incidence structure of a finite projective plane

theorem BruckRyserChowla.exists_sq_add_sq (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Finite L] (h : Configuration.ProjectivePlane.order P L % 4 = 1 ∨ Configuration.ProjectivePlane.order P L % 4 = 2) : ∃ (a : ℕ) (b : ℕ), Configuration.ProjectivePlane.order P L = a ^ 2 + b ^ 2

Bruck–Ryser–Chowla (1949, 1950). If a finite projective plane of order n exists and n ≡ 1 or 2 (mod 4), then n is a sum of two squares (so there is no plane of order 6 or 14).