noncomputable def OrthogonalityLines.lineHighFreq {p : ℕ} (L : Finset (ZMod p × ZMod p)) (x : ZMod p × ZMod p) : ℝ

The high-frequency part of the characteristic function $\mathbf{1}_L$ of a (would-be) line $L \subseteq \mathbb{F}_p^2$: $L_h(x) = \mathbf{1}_L(x) - 1/p$. For an actual affine line of cardinality $p$, this subtracts the average value $|L|/p^2 = 1/p$.

noncomputable def OrthogonalityLines.affineLine {p : ℕ} [Fact (Nat.Prime p)] (a b c : ZMod p) : Finset (ZMod p × ZMod p)

The affine line $\{(x, y) \in \mathbb{F}_p^2 \mid a x + b y = c\}$.

def OrthogonalityLines.IsAffineLine {p : ℕ} [Fact (Nat.Prime p)] (L : Finset (ZMod p × ZMod p)) : Prop

A finite subset $L \subseteq \mathbb{F}_p^2$ is an affine line if there exist coefficients $(a, b) \ne (0, 0)$ and $c \in \mathbb{F}_p$ with $L = \{a x + b y = c\}$.

theorem OrthogonalityLines.affineLine_card {p : ℕ} [Fact (Nat.Prime p)] (a b c : ZMod p) (hab : (a, b) ≠ (0, 0)) : (affineLine a b c).card = p

An affine line $\{a x + b y = c\}$ in $\mathbb{F}_p^2$ (with $(a, b) \ne 0$) has exactly $p$ points.

theorem OrthogonalityLines.IsAffineLine.card_eq {p : ℕ} [Fact (Nat.Prime p)] {L : Finset (ZMod p × ZMod p)} (hL : IsAffineLine L) : L.card = p

Every affine line in $\mathbb{F}_p^2$ has $|L| = p$.

theorem OrthogonalityLines.linear_system_unique {p : ℕ} [Fact (Nat.Prime p)] (a₁ b₁ a₂ b₂ dx dy : ZMod p) (hdet : a₁ * b₂ - a₂ * b₁ ≠ 0) (heq1 : a₁ * dx + b₁ * dy = 0) (heq2 : a₂ * dx + b₂ * dy = 0) : dx = 0 ∧ dy = 0

A homogeneous $2 \times 2$ linear system over $\mathbb{F}_p$ with nonzero determinant $a_1 b_2 - a_2 b_1 \ne 0$ has only the trivial solution $dx = dy = 0$.

theorem OrthogonalityLines.affineLine_mem_iff_of_proportional {p : ℕ} [Fact (Nat.Prime p)] (a₁ b₁ c₁ a₂ b₂ c₂ : ZMod p) (hab₁ : (a₁, b₁) ≠ (0, 0)) (hab₂ : (a₂, b₂) ≠ (0, 0)) (hsub : a₁ * b₂ = a₂ * b₁) (hcross_b : c₁ * b₂ = c₂ * b₁) (hcross_a : c₁ * a₂ = c₂ * a₁) (x' y' : ZMod p) : a₁ * x' + b₁ * y' = c₁ ↔ a₂ * x' + b₂ * y' = c₂

If two line equations $(a_1, b_1; c_1)$ and $(a_2, b_2; c_2)$ over $\mathbb{F}_p^2$ have proportional coefficients (cross ratios all vanish), then they define the same line: every point satisfies one iff it satisfies the other.

theorem OrthogonalityLines.affineLine_inter_card {p : ℕ} [Fact (Nat.Prime p)] (a₁ b₁ c₁ a₂ b₂ c₂ : ZMod p) (hab₁ : (a₁, b₁) ≠ (0, 0)) (hab₂ : (a₂, b₂) ≠ (0, 0)) (hdist : affineLine a₁ b₁ c₁ ≠ affineLine a₂ b₂ c₂) : (affineLine a₁ b₁ c₁ ∩ affineLine a₂ b₂ c₂).card ≤ 1

Two distinct affine lines in $\mathbb{F}_p^2$ intersect in at most one point.

theorem OrthogonalityLines.IsAffineLine.inter_card_le_one {p : ℕ} [Fact (Nat.Prime p)] {L₁ L₂ : Finset (ZMod p × ZMod p)} (hL₁ : IsAffineLine L₁) (hL₂ : IsAffineLine L₂) (hdist : L₁ ≠ L₂) : (L₁ ∩ L₂).card ≤ 1

Two distinct affine lines in $\mathbb{F}_p^2$ meet in at most one point.

theorem OrthogonalityLines.innerProduct_highFreq_eq {p : ℕ} [Fact (Nat.Prime p)] (L₁ L₂ : Finset (ZMod p × ZMod p)) (hL₁ : L₁.card = p) (hL₂ : L₂.card = p) : ∑ x : ZMod p × ZMod p, lineHighFreq L₁ x * lineHighFreq L₂ x = ↑(L₁ ∩ L₂).card - 1

Inner product of the high-frequency parts of two finite sets of size $p$ in $\mathbb{F}_p^2$: $\sum_{x \in \mathbb{F}_p^2} L_{1, h}(x) L_{2, h}(x) = |L_1 \cap L_2| - 1$.

theorem OrthogonalityLines.orthogonality_lines {p : ℕ} [Fact (Nat.Prime p)] (L₁ L₂ : Finset (ZMod p × ZMod p)) (hL₁ : IsAffineLine L₁) (hL₂ : IsAffineLine L₂) (hdist : L₁ ≠ L₂) : ∑ x : ZMod p × ZMod p, lineHighFreq L₁ x * lineHighFreq L₂ x ≤ 0

Lemma 2.4 (Orthogonality of lines). If $L_1, L_2$ are two distinct affine lines in $\mathbb{F}_q^2$, then $\sum_{x \in \mathbb{F}_q^2} L_{1, h}(x) L_{2, h}(x) \le 0$. This follows from $|L_1 \cap L_2| \le 1$ for distinct lines.