Finite uniform averages and existence of balanced label schedules

This module develops the finite-average step and schedule-existence proof of Lemma 4.5, printed pp. 30–31 of [OpenAI2026ETH]:

1. Schedule marginals and expected potentials:

   • A sampled schedule is a single function: repeated access to one variable reads the same coordinate (expect_schedule_apply, expect_schedule_apply_apply, expect_schedule_collision).
   • Exact finite-uniform occupancy variance expect_potential and expected total group potential expect_group_potential ($\mathbb{E}\Xi = Q n (1 - 1 / r) \le Q n$, expect_group_potential_le).
   • Product formula expect_incidence_collision for incidence-label collisions and the upper bound expect_incidence_potential_le ($\mathbb{E}\Phi \le M (b + w)$) when each variable belongs to at most b incidences and each factor contains at most w incidences.

2. Finite-average selection and conditional expectation step:

   • exists_le_expect and exists_coord_expect_le (fixing one schedule coordinate at a time without increasing the conditional expectation over the remaining coordinates).
   • normalizeEmptyFactors: setting $d_f(t) = g_0$ on factors with no incidences in A leaves all incidence labels (a (varOf e), d (factorOf e)) unchanged (incidenceLabel_normalizeEmptyFactors).
   • exists_balanced_schedules and exists_balanced_schedules_of_scopes: full existence statement of Lemma 4.5 from the size hypotheses (4.13).

Finite averages are mathematical sums, not runtime certificates.

References

• [OAI26c]

theorem Cslib.BalancedSchedules.expect_schedule_apply {A : Type u_1} {L : Type u_2} [Fintype A] [DecidableEq A] [Fintype L] [Nonempty L] (i : A) (f : L → ℚ) : (Finset.univ.expect fun (a : A → L) => f (a i)) = Finset.univ.expect fun (x : L) => f x

Accessing one coordinate of a uniformly enumerated function gives a uniform label.

theorem Cslib.BalancedSchedules.expect_schedule_apply_apply {A : Type u_1} {L : Type u_2} [Fintype A] [DecidableEq A] [Fintype L] [Nonempty L] (i j : A) (hji : j ≠ i) (f : L → L → ℚ) : (Finset.univ.expect fun (a : A → L) => f (a i) (a j)) = Finset.univ.expect fun (x : L) => Finset.univ.expect fun (y : L) => f x y

Distinct coordinates of a uniformly enumerated function give two independent uniform labels. The distinctness hypothesis is essential: a repeated coordinate is not resampled.

theorem Cslib.BalancedSchedules.expect_schedule_collision {A : Type u_1} {L : Type u_2} [Fintype A] [DecidableEq A] [Fintype L] [Nonempty L] [DecidableEq L] (i j : A) : (Finset.univ.expect fun (a : A → L) => if a i = a j then 1 else 0) = if i = j then 1 else 1 / ↑(Fintype.card L)

Exact collision average, retaining the diagonal case separately.

theorem Cslib.BalancedSchedules.expect_potential {A : Type u_1} {L : Type u_2} [Fintype A] [DecidableEq A] [Fintype L] [Nonempty L] [DecidableEq L] : (Finset.univ.expect fun (a : A → L) => potential a) = ↑(Fintype.card A) * (1 - 1 / ↑(Fintype.card L))

Exact finite-uniform occupancy variance. No independence is asserted for a repeated source coordinate; its diagonal collision contributes one.

theorem Cslib.BalancedSchedules.expect_group_potential {T : Type u_3} {V : Type u_4} {G : Type u_5} [Fintype T] [DecidableEq T] [Fintype V] [DecidableEq V] [Fintype G] [DecidableEq G] [Nonempty G] : (Finset.univ.expect fun (a : V → T → G) => ∑ t : T, potential fun (v : V) => a v t) = ↑(Fintype.card T) * ↑(Fintype.card V) * (1 - 1 / ↑(Fintype.card G))

The expected total group potential for a schedule family. Every variable has one whole schedule, reused at all points; swapping the two function indices just enumerates that same data.

theorem Cslib.BalancedSchedules.expect_incidence_collision {L : Type u_2} [Fintype L] [Nonempty L] {V : Type u_3} {F : Type u_4} [Fintype V] [DecidableEq V] [Fintype F] [DecidableEq F] [DecidableEq L] (v v' : V) (f f' : F) : (Finset.univ.expect fun (a : V → L) => Finset.univ.expect fun (d : F → L) => if (a v, d f) = (a v', d f') then 1 else 0) = (if v = v' then 1 else 1 / ↑(Fintype.card L)) * if f = f' then 1 else 1 / ↑(Fintype.card L)

Exact average collision probability for two incidence labels. Only variable labels and factor labels are independently enumerated; incidences sharing either endpoint stay correlated.

theorem Cslib.BalancedSchedules.expect_group_potential_le {T : Type u_3} {V : Type u_4} {G : Type u_5} [Fintype T] [DecidableEq T] [Fintype V] [DecidableEq V] [Fintype G] [DecidableEq G] [Nonempty G] : (Finset.univ.expect fun (a : V → T → G) => ∑ t : T, potential fun (v : V) => a v t) ≤ ↑(Fintype.card T) * ↑(Fintype.card V)

Upper bound 𝔼 Ξ ≤ |T| * |V| on the expected total group potential (Lemma 4.5, p. 31).

def Cslib.BalancedSchedules.incidenceLabel {A : Type u_3} {V : Type u_4} {F : Type u_5} {L : Type u_6} (varOf : A → V) (factorOf : A → F) (a : V → L) (d : F → L) (e : A) : L × L

The incidence label map u_e = (a (varOf e), d (factorOf e)) assigning each incidence e : A the pair of schedules of its variable varOf e and its factor factorOf e (Section 4.4, p. 30).

theorem Cslib.BalancedSchedules.expect_incidenceLabel_collision {A : Type u_3} {V : Type u_4} {F : Type u_5} {L : Type u_6} [Fintype V] [DecidableEq V] [Fintype F] [DecidableEq F] [Fintype L] [DecidableEq L] [Nonempty L] (varOf : A → V) (factorOf : A → F) (e e' : A) : (Finset.univ.expect fun (a : V → L) => Finset.univ.expect fun (d : F → L) => if incidenceLabel varOf factorOf a d e = incidenceLabel varOf factorOf a d e' then 1 else 0) = (if varOf e = varOf e' then 1 else 1 / ↑(Fintype.card L)) * if factorOf e = factorOf e' then 1 else 1 / ↑(Fintype.card L)

Expected collision probability of incidenceLabel varOf factorOf a d at two incidences e, e' : A.

theorem Cslib.BalancedSchedules.expect_incidence_potential_le {A : Type u_1} {L : Type u_2} [Fintype A] [Fintype L] [Nonempty L] {V : Type u_3} {F : Type u_4} [Fintype V] [DecidableEq V] [Fintype F] [DecidableEq F] [DecidableEq L] (varOf : A → V) (factorOf : A → F) {b w : ℕ} (hb : ∀ (e : A), {e' : A | varOf e' = varOf e}.card ≤ b) (hw : ∀ (e : A), {e' : A | factorOf e' = factorOf e}.card ≤ w) : (Finset.univ.expect fun (a : V → L) => Finset.univ.expect fun (d : F → L) => potential (incidenceLabel varOf factorOf a d)) ≤ ↑(Fintype.card A) * (↑b + ↑w)

Lemma 4.5 expected incidence potential bound (p. 31): when each variable occurs in at most b incidences and each factor contains at most w incidences, 𝔼 a, 𝔼 d, potential (incidenceLabel varOf factorOf a d) ≤ |A| * (b + w).

theorem Cslib.BalancedSchedules.exists_le_expect {Ω : Type u_3} [Fintype Ω] [Nonempty Ω] (f : Ω → ℚ) : ∃ (ω : Ω), f ω ≤ Finset.univ.expect fun (ω' : Ω) => f ω'

Any rational function on a nonempty finite type attains a value at most its uniform average.

theorem Cslib.BalancedSchedules.exists_coord_expect_le {A : Type u_1} {L : Type u_2} [Fintype A] [DecidableEq A] [Fintype L] [Nonempty L] (i : A) (f : (A → L) → ℚ) : ∃ (x : L), (Finset.univ.expect fun (a' : { j : A // j ≠ i } → L) => f ((Equiv.funSplitAt i L).symm (x, a'))) ≤ Finset.univ.expect fun (a : A → L) => f a

Fixing one coordinate i : A of a schedule a : A → L can be done without increasing the conditional expectation over the remaining coordinates {j : A // j ≠ i} → L (Lemma 4.5, p. 31).

def Cslib.BalancedSchedules.normalizeEmptyFactors {A : Type u_1} [Fintype A] {F : Type u_3} {T : Type u_4} {G : Type u_5} [DecidableEq F] (factorOf : A → F) (g₀ : G) (d : F → T → G) (f : F) : T → G

Replace d f by the constant schedule fun _ => g₀ on every factor f : F that has no incidences in A (Lemma 4.5, p. 30: "with d_f(t) = 1 for factors of empty scope").

theorem Cslib.BalancedSchedules.normalizeEmptyFactors_of_not_exists {A : Type u_1} [Fintype A] {F : Type u_3} {T : Type u_4} {G : Type u_5} [DecidableEq F] (factorOf : A → F) (g₀ : G) (d : F → T → G) {f : F} (hf : ¬∃ (e : A), factorOf e = f) : normalizeEmptyFactors factorOf g₀ d f = fun (x : T) => g₀

@[simp]

theorem Cslib.BalancedSchedules.normalizeEmptyFactors_factorOf {A : Type u_1} [Fintype A] {F : Type u_3} {T : Type u_4} {G : Type u_5} [DecidableEq F] (factorOf : A → F) (g₀ : G) (d : F → T → G) (e : A) : normalizeEmptyFactors factorOf g₀ d (factorOf e) = d (factorOf e)

@[simp]

theorem Cslib.BalancedSchedules.incidenceLabel_normalizeEmptyFactors {A : Type u_1} [Fintype A] {V : Type u_3} {F : Type u_4} {T : Type u_5} {G : Type u_6} [DecidableEq F] (varOf : A → V) (factorOf : A → F) (g₀ : G) (a : V → T → G) (d : F → T → G) : incidenceLabel varOf factorOf a (normalizeEmptyFactors factorOf g₀ d) = incidenceLabel varOf factorOf a d

theorem Cslib.BalancedSchedules.exists_balanced_schedules {A : Type u_1} [Fintype A] {T : Type u_3} {V : Type u_4} {F : Type u_5} {G : Type u_6} [Fintype T] [DecidableEq T] [Nonempty T] [Fintype V] [DecidableEq V] [Nonempty V] [Finite F] [DecidableEq F] [Fintype G] [DecidableEq G] [Nonempty G] (varOf : A → V) (factorOf : A → F) {b w : ℕ} (hb : ∀ (e : A), {e' : A | varOf e' = varOf e}.card ≤ b) (hw : ∀ (e : A), {e' : A | factorOf e' = factorOf e}.card ≤ w) (hbw : 0 < b + w) (hincidenceSize : 2 * (b + w) * Fintype.card ((T → G) × (T → G)) ^ 2 ≤ Fintype.card A) (hgroupSize : 2 * Fintype.card T * Fintype.card G ^ 2 ≤ Fintype.card V) (g₀ : G) : ∃ (a : V → T → G) (d : F → T → G), (∀ (f : F), (¬∃ (e : A), factorOf e = f) → d f = fun (x : T) => g₀) ∧ (∀ (u : (T → G) × (T → G)), occupancy (incidenceLabel varOf factorOf a d) u * Fintype.card ((T → G) × (T → G)) ≤ 2 * Fintype.card A) ∧ ∀ (t : T) (g : G), occupancy (fun (v : V) => a v t) g * Fintype.card G ≤ 2 * Fintype.card V

Lemma 4.5 (balanced variable and factor schedules, pp. 30–31): Suppose each variable in V occurs in at most b incidences of A, each factor in F contains at most w incidences of A, 0 < b + w, and the size hypotheses (4.13) hold: 2 * (b + w) * Fintype.card ((T → G) × (T → G)) ^ 2 ≤ Fintype.card A and 2 * Fintype.card T * Fintype.card G ^ 2 ≤ Fintype.card V. Then for any default group g₀ : G, there exist schedules a : V → T → G and d : F → T → G such that:

1. d f = fun _ => g₀ for every factor f : F with no incidences in A;
2. Every label pair u : (T → G) × (T → G) has incidence occupancy satisfying occupancy (incidenceLabel varOf factorOf a d) u * Fintype.card ((T → G) × (T → G)) ≤ 2 * Fintype.card A;
3. Every step t : T and group g : G has variable group size satisfying occupancy (fun v => a v t) g * Fintype.card G ≤ 2 * Fintype.card V.

Explicit factor-scope incidence type A = {(f, v) : f ∈ F, v ∈ I_f} (eq. 4.1, p. 26)

@[reducible, inline]

abbrev Cslib.BalancedSchedules.ScopeIncidence {F : Type u_3} {V : Type u_4} (scope : F → Finset V) : Type (max u_4 u_3)

The incidence type A = {(f, v) : f ∈ F, v ∈ scope f} of a family of factor scopes scope : F → Finset V (eq. 4.1, p. 26).

def Cslib.BalancedSchedules.scopeVarOf {F : Type u_3} {V : Type u_4} (scope : F → Finset V) (e : ScopeIncidence scope) : V

Variable projection (f, v) ↦ v on ScopeIncidence scope.

def Cslib.BalancedSchedules.scopeFactorOf {F : Type u_3} {V : Type u_4} (scope : F → Finset V) (e : ScopeIncidence scope) : F

Factor projection (f, v) ↦ f on ScopeIncidence scope.

theorem Cslib.BalancedSchedules.card_scopeIncidence {F : Type u_3} {V : Type u_4} [Fintype F] (scope : F → Finset V) : Fintype.card (ScopeIncidence scope) = ∑ f : F, (scope f).card

Total incidence count M = |A| = ∑ f, #(scope f) (eq. 4.1, p. 26).

theorem Cslib.BalancedSchedules.card_filter_scopeFactorOf_eq {F : Type u_3} {V : Type u_4} [Fintype F] [DecidableEq F] (scope : F → Finset V) (e : ScopeIncidence scope) : {e' : ScopeIncidence scope | scopeFactorOf scope e' = scopeFactorOf scope e}.card = (scope (scopeFactorOf scope e)).card

For each e : ScopeIncidence scope, the number of incidences sharing factor scopeFactorOf scope e equals #(scope (scopeFactorOf scope e)).

theorem Cslib.BalancedSchedules.card_filter_scopeVarOf_eq {F : Type u_3} {V : Type u_4} [Fintype F] [DecidableEq V] (scope : F → Finset V) (e : ScopeIncidence scope) : {e' : ScopeIncidence scope | scopeVarOf scope e' = scopeVarOf scope e}.card = {f : F | scopeVarOf scope e ∈ scope f}.card

For each e : ScopeIncidence scope, the number of incidences sharing variable scopeVarOf scope e equals #{f : F | scopeVarOf scope e ∈ scope f}.

theorem Cslib.BalancedSchedules.exists_scopeFactorOf_eq_iff {F : Type u_3} {V : Type u_4} (scope : F → Finset V) (f : F) : (∃ (e : ScopeIncidence scope), scopeFactorOf scope e = f) ↔ (scope f).Nonempty

A factor f : F has an incidence in ScopeIncidence scope iff scope f is nonempty.

theorem Cslib.BalancedSchedules.exists_balanced_schedules_of_scopes {T : Type u_3} {V : Type u_4} {F : Type u_5} {G : Type u_6} [Fintype T] [DecidableEq T] [Nonempty T] [Fintype V] [DecidableEq V] [Nonempty V] [Fintype F] [Fintype G] [DecidableEq G] [Nonempty G] (scope : F → Finset V) {b w : ℕ} (hb : ∀ (v : V), {f : F | v ∈ scope f}.card ≤ b) (hw : ∀ (f : F), (scope f).card ≤ w) (hbw : 0 < b + w) (hincidenceSize : 2 * (b + w) * Fintype.card ((T → G) × (T → G)) ^ 2 ≤ Fintype.card (ScopeIncidence scope)) (hgroupSize : 2 * Fintype.card T * Fintype.card G ^ 2 ≤ Fintype.card V) (g₀ : G) : ∃ (a : V → T → G) (d : F → T → G), (∀ (f : F), scope f = ∅ → d f = fun (x : T) => g₀) ∧ (∀ (u : (T → G) × (T → G)), occupancy (incidenceLabel (scopeVarOf scope) (scopeFactorOf scope) a d) u * Fintype.card ((T → G) × (T → G)) ≤ 2 * Fintype.card (ScopeIncidence scope)) ∧ ∀ (t : T) (g : G), occupancy (fun (v : V) => a v t) g * Fintype.card G ≤ 2 * Fintype.card V

Lemma 4.5 for explicit factor scopes scope : F → Finset V (pp. 30–31): When ∀ f, #(scope f) ≤ w, ∀ v, #{f | v ∈ scope f} ≤ b, 0 < b + w, and the size bounds (4.13) hold for M = Fintype.card (ScopeIncidence scope) = ∑ f, #(scope f), there exist schedules a : V → T → G and d : F → T → G such that d f = fun _ => g₀ whenever scope f = ∅, every label pair u has incidence occupancy at most 2 * M / D, and every variable group has size at most 2 * |V| / |G|.