Collision potentials for balanced label schedules

The proof of Lemma 4.5, printed pp. 30–31 of [OAI26c], balances incidence labels and variable groups using two sums of squared deviations. This module supplies the exact finite collision identity and the deterministic implication from a potential bound to an occupancy bound. It does not yet supply the finite-average estimates, select schedules, or certify the paper's bit-operation bound.

All sums of collisions count ordered pairs, including diagonal pairs. Empty source and empty fibers are included. A variable's label is data attached to that variable, not independently chosen for its occurrences.

def Cslib.BalancedSchedules.occupancy {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq B] (label : A → B) (u : B) : ℕ

Number of objects receiving a specified label.

theorem Cslib.BalancedSchedules.sum_occupancy {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) : ∑ u : B, occupancy label u = Fintype.card A

The total occupancy is the number of objects, also when that number is zero.

theorem Cslib.BalancedSchedules.sum_occupancy_sq {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) : ∑ u : B, occupancy label u ^ 2 = ∑ a : A, occupancy label (label a)

Counting collisions by their common label or by their first object gives the same result.

theorem Cslib.BalancedSchedules.sum_occupancy_sq_eq_collisions {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) : ∑ u : B, occupancy label u ^ 2 = ∑ a : A, ∑ a' : A, if label a = label a' then 1 else 0

Exact ordered-pair expansion of the collision count. Diagonal collisions are retained.

def Cslib.BalancedSchedules.potential {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) : ℚ

Rational squared-deviation potential at the exact uniform average.

theorem Cslib.BalancedSchedules.potential_eq_collisions_sub {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) (hB : 0 < Fintype.card B) : potential label = (∑ a : A, ∑ a' : A, if label a = label a' then 1 else 0) - ↑(Fintype.card A) ^ 2 / ↑(Fintype.card B)

Exact centered-square expansion used in the paper's two collision potentials.

theorem Cslib.BalancedSchedules.potential_nonneg {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) : 0 ≤ potential label

A squared-deviation potential is nonnegative, without nonemptiness assumptions.

theorem Cslib.BalancedSchedules.deviation_sq_le_potential {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) (u : B) : (↑(occupancy label u) - ↑(Fintype.card A) / ↑(Fintype.card B)) ^ 2 ≤ potential label

Each individual squared deviation is bounded by the full potential.

theorem Cslib.BalancedSchedules.occupancy_le_twice_mean {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) (hpotential : potential label ≤ (↑(Fintype.card A) / ↑(Fintype.card B)) ^ 2) (u : B) : ↑(occupancy label u) ≤ 2 * ↑(Fintype.card A) / ↑(Fintype.card B)

If the total potential is at most the squared mean, every fiber has occupancy at most twice the mean. This is the square-root-free step used for both bounds in Lemma 4.5.

theorem Cslib.BalancedSchedules.sum_potential_eq_collisions_sub {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] {T : Type u_3} [Fintype T] (label : T → A → B) (hB : 0 < Fintype.card B) : ∑ t : T, potential (label t) = (∑ t : T, ∑ a : A, ∑ a' : A, if label t a = label t a' then 1 else 0) - ↑(Fintype.card T) * ↑(Fintype.card A) ^ 2 / ↑(Fintype.card B)

The second collision expansion in Lemma 4.5, summed over the schedule coordinates.

theorem Cslib.BalancedSchedules.components_le_of_normalized_le_two {Φ Ξ x y : ℚ} (hΦ : 0 ≤ Φ) (hΞ : 0 ≤ Ξ) (hx : 0 < x) (hy : 0 < y) (h : Φ / x + Ξ / y ≤ 2) : Φ ≤ 2 * x ∧ Ξ ≤ 2 * y

The paper's normalized potential bound controls both nonnegative components separately. No relation between the two normalization factors is assumed.

theorem Cslib.BalancedSchedules.occupancy_mul_card_le {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) (hB : 0 < Fintype.card B) (hpotential : potential label ≤ (↑(Fintype.card A) / ↑(Fintype.card B)) ^ 2) (u : B) : occupancy label u * Fintype.card B ≤ 2 * Fintype.card A

Cross-multiplied natural form of the pointwise occupancy bound.

theorem Cslib.BalancedSchedules.occupancy_mul_card_le_of_variance_bound {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (label : A → B) (hB : 0 < Fintype.card B) (C : ℕ) (hpotential : potential label ≤ 2 * ↑(Fintype.card A) * ↑C) (hsize : 2 * C * Fintype.card B ^ 2 ≤ Fintype.card A) (u : B) : occupancy label u * Fintype.card B ≤ 2 * Fintype.card A

The size hypothesis in (4.13) absorbs the collision variance bound, without rounding the source's 2 * M / D bound up to an integer. Here C will be b + w.

theorem Cslib.BalancedSchedules.incidence_and_group_bounds {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] {T : Type u_3} {V : Type u_4} {G : Type u_5} [Fintype T] [Fintype V] [Fintype G] [DecidableEq G] (incidence : A → B) (group : T → V → G) (C : ℕ) (hA : 0 < Fintype.card A) (hB : 0 < Fintype.card B) (hC : 0 < C) (hT : 0 < Fintype.card T) (hV : 0 < Fintype.card V) (hG : 0 < Fintype.card G) (hincidenceSize : 2 * C * Fintype.card B ^ 2 ≤ Fintype.card A) (hgroupSize : 2 * Fintype.card T * Fintype.card G ^ 2 ≤ Fintype.card V) (hpotential : potential incidence / (↑(Fintype.card A) * ↑C) + (∑ t : T, potential (group t)) / (↑(Fintype.card T) * ↑(Fintype.card V)) ≤ 2) : (∀ (u : B), occupancy incidence u * Fintype.card B ≤ 2 * Fintype.card A) ∧ ∀ (t : T) (g : G), occupancy (group t) g * Fintype.card G ≤ 2 * Fintype.card V

The two conclusions of Lemma 4.5 follow from its normalized potential bound and size hypotheses. incidence may be the pair (a v, d f) and group t v is the SAME variable label a v at coordinate t. This implication does not construct labels or assume they exist.