noncomputable def ProjectionTheory.projMap (p : ℕ) (θ : ZMod p) (x : ZMod p × ZMod p) : ZMod p

Projection map over ZMod p: projMap p θ (x₁, x₂) = x₁ + θ · x₂, the direction-θ projection in the affine plane 𝔽_p².

noncomputable def ProjectionTheory.projImage (p : ℕ) (θ : ZMod p) (X : Finset (ZMod p × ZMod p)) : Finset (ZMod p)

The image π_θ(X) ⊆ 𝔽_p of a finite set X ⊆ 𝔽_p² under the projection projMap p θ.

theorem ProjectionTheory.double_counting_ineq (p : ℕ) [hp : Fact (Nat.Prime p)] (X : Finset (ZMod p × ZMod p)) (D : Finset (ZMod p)) (hX : X.Nonempty) (S : ℕ) (hS : ∀ t ∈ D, (projImage p t X).card ≤ S) : X.card * D.card ≤ S * (D.card + X.card)

Double-counting inequality on 𝔽_p²: if for every direction t ∈ D the projection π_t(X) has size at most S, then |X| · |D| ≤ S · (|D| + |X|). This is the key estimate underlying the contagious-structure double-counting lemma.

theorem ProjectionTheory.double_counting_lower_bound : ∃ C > 0, ∀ (p : ℕ), Nat.Prime p → ∀ (X : Finset (ZMod p × ZMod p)) (D : Finset (ZMod p)), D.Nonempty → ∃ t ∈ D, C * min ↑X.card ↑D.card ≤ ↑(projImage p t X).card

Lemma (Double Counting, lower bound). For any subset X ⊆ 𝔽_p² and any nonempty set of directions D ⊆ 𝔽_p, there exists t ∈ D such that |π_t(X)| ≥ (1/2) · min(|X|, |D|). That is, max_{t ∈ D} |π_t(X)| ≳ min(|X|, |D|).