Counting lower bounds for anchored witness assignments

theorem GenLimit.FiniteWitness.Anchored.anchor_cover {k q : ℕ} {T : Set Point → Finset Point} (hT : Valid (family k) T) (hb : ∀ L ∈ family k, (T L).card ≤ q) : ∃ (D : Set ℕ) (R : Fin k → Finset (Fin k)), (∀ (j : Fin k), (R j).card ≤ q) ∧ ∀ (i j : Fin k), Sum.inl ↑j ∈ T (leftTarget i D) ∨ i ∈ R j

theorem GenLimit.FiniteWitness.Anchored.lower_incidence {k q : ℕ} {T : Set Point → Finset Point} (hT : Valid (family k) T) (hb : ∀ L ∈ family k, (T L).card ≤ q) : k * k ≤ 2 * k * q

theorem GenLimit.FiniteWitness.Anchored.lower_bound {k q : ℕ} (h : HasBoundedWitnesses (family k) q) : (k + 1) / 2 ≤ q