RMM 2023 Shortlist N1

Let $n$ be a positive integer. Let $S$ be a set of ordered pairs $(x, y)$ such that $1 \le x \le n$ and $0 \le y \le n$ in each pair, and there are no pairs $(a, b)$ and $(c, d)$ of different elements in $S$ such that $a^2 + b ^ 2$ divides both $ac + bd$ and $ad - bc$. In terms of $n$, determine the size of the largest possible set $S$.

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Finset.Card
import Mathlib.Order.Bounds.Defs

def answer (n : ℕ) : ℕ := sorry

def S (n : ℕ) : Set ℕ := { a : ℕ | ∃ S : Finset (ℕ × ℕ), S.card = a ∧
    (∀ p ∈ S, 1 ≤ p.1 ∧ p.1 ≤ n ∧ 0 ≤ p.2 ∧ p.2 ≤ n) ∧
    (∀ u ∈ S, ∀ v ∈ S, u ≠ v → ¬(
      (u.1 ^ 2 + u.2 ^ 2) ∣ (u.1 * v.1 + u.2 * v.2) ∧
      (u.1 ^ 2 + u.2 ^ 2) ∣ (u.1 * v.2 - u.2 * v.1))) }

theorem solution (n : ℕ) (hn : n > 0) : IsGreatest (S n) (answer n) := sorry

Login to submit a solution.