theorem BKT.expansion_from_structured_subset (p : ℕ) [Fact (Nat.Prime p)] (X : Finset (ZMod p × ZMod p)) (D A : Finset (ZMod p)) (hA_lower : 1 < A.card) (hA_upper : ↑A.card ≤ ↑p) (hD_card : 1 < D.card) (hX_sub : ∀ x ∈ X, x.1 ∈ A ∧ x.2 ∈ A) (hX_lower : 1 < X.card) (hX_upper : ↑X.card < ↑p ^ 2) (hA_ge_sqrt : ↑A.card ^ 2 ≥ ↑X.card) : ∃ ε > 0, ∃ t ∈ D, ↑(Finset.image (fun (x : ZMod p × ZMod p) => x.1 + t * x.2) X).card ≥ ↑p ^ ε * ↑X.card ^ (1 / 2)

Structured-subset version of BKT: assuming X ⊆ A × A for some A ⊆ 𝔽_p with |A|² ≥ |X|, there exist ε > 0 and a direction t ∈ D so that the projection π_t(X) = {x₁ + t · x₂ : x ∈ X} satisfies |π_t(X)| ≥ p^ε · |X|^{1/2}. This is the key step in deducing BKT from the abelian sum–product input.

theorem BKT.bkt_projection_bound (p : ℕ) [Fact (Nat.Prime p)] (X : Finset (ZMod p × ZMod p)) (D : Finset (ZMod p)) (hX : 1 < X.card) (hD : 1 < D.card) (hX_upper : ↑X.card < ↑p ^ 2) (hD_upper : ↑D.card ≤ ↑p) : ∃ ε > 0, ∃ t ∈ D, ↑(Finset.image (fun (x : ZMod p × ZMod p) => x.1 + t * x.2) X).card ≥ ↑p ^ ε * ↑X.card ^ (1 / 2)

The Bourgain–Katz–Tao projection theorem (BKT) in 𝔽_p²: for X ⊆ 𝔽_p² of size |X| = p^{s_X} with 0 < s_X < 2 and a nontrivial set of directions D ⊆ 𝔽_p, there exist ε > 0 and t ∈ D such that the linear projection π_t(X) = {x₁ + t · x₂ : x ∈ X} obeys |π_t(X)| ≥ p^ε · |X|^{1/2}. The argument reduces to expansion_from_structured_subset applied to A = π_1(X) ∪ π_2(X).