The collision tail

Choose a direction for each of k requests independently and uniformly among the nonzero vectors of K ^ ℓ. A fixed point other than the target blocks Fintype.card K - 1 of the Fintype.card K ^ ℓ - 1 directions, so the line of one request meets a fixed set B for at most #B * (Fintype.card K - 1) directions. If fewer than half of the requests are clean, then a collision cut (exists_collisionCut) selects ⌈k / 4⌉ requests whose lines meet the occupied points or the lines of requests outside the selection. Once the directions outside the selection are fixed, these events concern distinct coordinates, so conditional counting (card_filter_forall_mem_le) bounds them by a product. A union bound over the selections shows that, under the budget 256 * ((#occupied + k * (q - 1)) * (q - 1)) ≤ q ^ ℓ - 1, at most a 2 ^ (-k) fraction of the direction tuples leave fewer than half of the requests clean.

Targets may repeat and may be occupied: the bound counts every tuple of targets and every occupied set.

Main results

• Cslib.LineCode.card_filter_two_mul_card_isClean_lt_mul_two_pow_le: the collision tail.

References

• Adapted, with nonzero vectors in place of projective directions, from MassProduction/Nonuniform/CollisionTail.lean and MassProduction/Nonuniform/PhaseMenu.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.LineCode.card_filter_two_mul_card_isClean_lt_mul_two_pow_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ k : ℕ} (occupied : Finset (Fin ℓ → K)) (targets : Fin k → Fin ℓ → K) (hbudget : 256 * ((occupied.card + k * (Fintype.card K - 1)) * (Fintype.card K - 1)) ≤ Fintype.card K ^ ℓ - 1) : {d : Fin k → { v : Fin ℓ → K // v ≠ 0 } | 2 * {i : Fin k | IsClean occupied targets (fun (j : Fin k) => ↑(d j)) i}.card < k}.card * 2 ^ k ≤ (Fintype.card K ^ ℓ - 1) ^ k

Collision tail. Under the budget 256 * ((#occupied + k * (q - 1)) * (q - 1)) ≤ q ^ ℓ - 1, where q = Fintype.card K, at most a 2 ^ (-k) fraction of the tuples of nonzero directions leave fewer than half of the k requests clean, for every occupied set and every tuple of targets.