def ProjectionTheory.piTheta {F : Type u_1} [Add F] [Mul F] (θ : F) : F × F → F

The projection in direction θ of a point (x₁, x₂) ∈ F × F, defined as π_θ(x) = x₁ + θ · x₂.

noncomputable def ProjectionTheory.projectionImage {F : Type u_1} [Add F] [Mul F] [DecidableEq F] (θ : F) (X : Finset (F × F)) : Finset F

The image π_θ(X) ⊆ F of a finite set X ⊆ F × F under the direction-θ projection piTheta θ.

theorem ProjectionTheory.piTheta_eq_subsingleton {F : Type u_1} [Field F] (x₁ x₂ : F × F) (hne : x₁ ≠ x₂) : {θ : F | piTheta θ x₁ = piTheta θ x₂}.Subsingleton

For two distinct points x₁ ≠ x₂ in F × F over a field F, the set of directions θ for which π_θ(x₁) = π_θ(x₂) is a subsingleton: at most one direction can identify the two points.

theorem ProjectionTheory.card_filter_piTheta_le_one {F : Type u_1} [Field F] [DecidableEq F] (x₁ x₂ : F × F) (hne : x₁ ≠ x₂) (D : Finset F) : {θ ∈ D | piTheta θ x₁ = piTheta θ x₂}.card ≤ 1

Finset version of piTheta_eq_subsingleton: for distinct x₁, x₂ and any direction set D, at most one θ ∈ D satisfies π_θ(x₁) = π_θ(x₂).

theorem ProjectionTheory.sum_sq_fibers_eq {F : Type u_1} [Field F] [DecidableEq F] (θ : F) (X : Finset (F × F)) : ∑ z ∈ Finset.image (piTheta θ) X, {y ∈ X | piTheta θ y = z}.card ^ 2 = ∑ x ∈ X, {y ∈ X | piTheta θ y = piTheta θ x}.card

The sum of squared fiber sizes of π_θ over its image equals the sum, over x ∈ X, of the fiber size of π_θ at π_θ(x). This identity rewrites a squared count as a diagonal-weighted count.

theorem ProjectionTheory.double_counting_key_ineq {F : Type u_1} [Field F] [DecidableEq F] [Fintype F] (X : Finset (F × F)) (D : Finset F) (S : ℕ) (hS : S > 0) (hS_bound : ∀ θ ∈ D, (projectionImage θ X).card ≤ S) (hXS : S ≤ X.card) : D.card * (X.card - S) ≤ S * X.card

Core double-counting inequality used in the proof of Theorem 2.2: if S bounds the projection size |π_θ(X)| for every θ ∈ D and S ≤ |X|, then |D| · (|X| − S) ≤ S · |X|. Combining a Cauchy–Schwarz lower bound on incidences with an upper bound on coincidences across directions yields this estimate.

theorem ProjectionTheory.double_counting_ff {F : Type u_1} [Field F] [DecidableEq F] [Fintype F] (X : Finset (F × F)) (D : Finset F) (hX : X.Nonempty) (S : ℕ) (hS : S > 0) (hS_bound : ∀ θ ∈ D, (projectionImage θ X).card ≤ S) (hSX : 2 * S ≤ X.card) : D.card ≤ 2 * S

Theorem 2.2 (Double counting in 𝔽_q²). Suppose X ⊆ F × F over a finite field F and D ⊆ F, with S := max_{θ ∈ D} |π_θ(X)|. If S ≤ |X|/2 (equivalently 2S ≤ |X|), then |D| ≤ 2S, i.e. |D| ≲ S.