Exponential collision tails for independently chosen recovery sets

The proof applies to any finite family of recovery sets in which a fixed point blocks at most one choice. A collision cut selects requests whose failures become independent after the complementary directions are fixed. Counting all such cuts proves an exponential bound without assuming that the individual collision edges are independent.

def Algebraic.MassProduction.Nonuniform.Clean {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} (sets : Index → Choice → Finset Point) (occupied : Finset Point) (assignment : Index → Choice) (index : Index) : Prop

A request is clean if its recovery set avoids the occupied set and all other requests' recovery sets.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.Nonuniform.badRequests {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (assignment : Index → Choice) : Finset Index

Nonclean request indices, including requests colliding with occupancy.

Equations

• Algebraic.MassProduction.Nonuniform.badRequests sets occupied assignment = {index : Index | ¬Algebraic.MassProduction.Nonuniform.Clean sets occupied assignment index}

theorem Algebraic.MassProduction.Nonuniform.existsRequestCollisionCut {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] [DecidableEq Point] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (assignment : Index → Choice) (size : ℕ) (enoughBad : 2 * size ≤ (badRequests sets occupied assignment).card + 1) : ∃ (selected : Finset Index), selected.card = size ∧ ∀ index ∈ selected, ¬Disjoint (sets index (assignment index)) occupied ∨ ∃ other ∉ selected, ¬Disjoint (sets index (assignment index)) (sets other (assignment other))

A large set of nonclean requests has a cut witness of any requested size at most the ceiling of half the number of nonclean requests.

noncomputable def Algebraic.MassProduction.Nonuniform.outsidePoints {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] [DecidableEq Index] [DecidableEq Point] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (selected : Finset Index) (outside : { index : Index // index ∉ selected } → Choice) : Finset Point

The union of occupancy and the complementary requests, after their directions have been fixed.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.cardOutsidePoints_le {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] [DecidableEq Index] [DecidableEq Point] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (selected : Finset Index) (outside : { index : Index // index ∉ selected } → Choice) (setSize : ℕ) (setsSmall : ∀ (index : Index) (choice : Choice), (sets index choice).card ≤ setSize) : (outsidePoints sets occupied selected outside).card ≤ occupied.card + Fintype.card Index * setSize

Occupancy and the complementary recovery sets use at most the sum of their individual point budgets.

theorem Algebraic.MassProduction.Nonuniform.cardCutFailures_le {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] [Fintype Choice] [DecidableEq Index] [DecidableEq Point] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (setSize : ℕ) (setsSmall : ∀ (index : Index) (choice : Choice), (sets index choice).card ≤ setSize) (blocking : ∀ (index : Index) (used : Finset Point), Nat.card { choice : Choice // ¬Disjoint (sets index choice) used } ≤ used.card) (selected : Finset Index) : Nat.card { assignment : Index → Choice // ∀ index ∈ selected, ¬Disjoint (sets index (assignment index)) (outsidePoints sets occupied selected fun (outside : { index : Index // index ∉ selected }) => assignment ↑outside) } ≤ Fintype.card Choice ^ (Fintype.card Index - selected.card) * (occupied.card + Fintype.card Index * setSize) ^ selected.card

For each fixed cut, the choices on its selected side are independent once the complementary choices have been fixed.

theorem Algebraic.MassProduction.Nonuniform.cardManyCollisions_le {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] [Fintype Choice] [DecidableEq Index] [DecidableEq Point] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (setSize : ℕ) (setsSmall : ∀ (index : Index) (choice : Choice), (sets index choice).card ≤ setSize) (blocking : ∀ (index : Index) (used : Finset Point), Nat.card { choice : Choice // ¬Disjoint (sets index choice) used } ≤ used.card) : Nat.card { assignment : Index → Choice // Fintype.card Index ≤ 2 * (badRequests sets occupied assignment).card } ≤ 2 ^ Fintype.card Index * (Fintype.card Choice ^ (Fintype.card Index - (Fintype.card Index + 3) / 4) * (occupied.card + Fintype.card Index * setSize) ^ ((Fintype.card Index + 3) / 4))

A union bound over cuts of size ceil(k/4) counts all assignments in which at least half of the requests are nonclean.

theorem Algebraic.MassProduction.Nonuniform.cardManyCollisionsMulTwoPow_le {Index : Type u_1} {Choice : Type u_2} {Point : Type u_3} [Fintype Index] [Fintype Choice] [DecidableEq Index] [DecidableEq Point] (sets : Index → Choice → Finset Point) (occupied : Finset Point) (setSize : ℕ) (setsSmall : ∀ (index : Index) (choice : Choice), (sets index choice).card ≤ setSize) (blocking : ∀ (index : Index) (used : Finset Point), Nat.card { choice : Choice // ¬Disjoint (sets index choice) used } ≤ used.card) (budget : 256 * (occupied.card + Fintype.card Index * setSize) ≤ Fintype.card Choice) : Nat.card { assignment : Index → Choice // Fintype.card Index ≤ 2 * (badRequests sets occupied assignment).card } * 2 ^ Fintype.card Index ≤ Fintype.card Choice ^ Fintype.card Index

If the blocking budget is at most 1/256 of the choice space, the fraction of candidates with at least half their requests nonclean is at most 2^(-k). The statement uses exact natural-number cardinalities.