Deterministic construction of balanced label schedules

The conditional-expectation construction in Lemma 4.5, printed p. 31 of [OAI26c], fixes one whole variable or factor label at a time. This module completes the traversal using bestVariableLabel and bestFactorLabel. A slot that is already assigned is retained, so repeated slots do not invalidate the fresh-choice premise. Every incidence still reads the same label of its original variable and factor.

The canonical construction uses the executable enumerations FinEnum.toList and List.Pi.enum. Its total schedules have joint normalized potential no greater than the initial finite average. Factors with empty scopes receive the specified constant label. This is an executable finite algorithm and its mathematical correctness proof; rational bit-cost and native-machine bounds are separate obligations.

Main definitions

• Cslib.BalancedSchedules.greedyLabelStep: fix one fresh variable or factor label.
• Cslib.BalancedSchedules.greedyLabelPass: traverse an explicit list of slots.
• Cslib.BalancedSchedules.greedySchedules: construct both complete schedule families.

Main results

• Cslib.BalancedSchedules.greedyLabelPass_spec: completion, preservation and score monotonicity.
• Cslib.BalancedSchedules.greedySchedules_candidates_length: the exact r ^ Q candidate count.
• Cslib.BalancedSchedules.greedySchedules_slots_length: the exact number of slots.
• Cslib.BalancedSchedules.greedySchedules_score_le: the output beats the initial average.
• Cslib.BalancedSchedules.greedySchedules_empty_factor: empty-factor normalization.
• Cslib.BalancedSchedules.greedySchedules_balanced: both pointwise occupancy bounds.

References

• [OAI26c], §4.4, Lemma 4.5, printed pp. 30–31.

def Cslib.BalancedSchedules.greedyLabelStep {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] (edge : E → F × V) (C : ℕ) (values : List (T → G)) (assigned : (V → Option (T → G)) × (F → Option (T → G))) (slot : V ⊕ F) : (V → Option (T → G)) × (F → Option (T → G))

Fix one fresh whole label using the first minimizing candidate. Already fixed labels are retained. Empty candidate lists leave a fresh slot unassigned.

def Cslib.BalancedSchedules.greedyLabelPass {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] (edge : E → F × V) (C : ℕ) (values : List (T → G)) (slots : List (V ⊕ F)) (assigned : (V → Option (T → G)) × (F → Option (T → G))) : (V → Option (T → G)) × (F → Option (T → G))

Traverse slots in the supplied order, retaining each selected whole label for all later score evaluations. This accepts repeated slots without overwriting an earlier selection.

theorem Cslib.BalancedSchedules.greedyLabelPass_spec {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (edge : E → F × V) (C : ℕ) (values : List (T → G)) (hcover : ∀ (word : T → G), word ∈ values) (slots : List (V ⊕ F)) (assigned : (V → Option (T → G)) × (F → Option (T → G))) : normalizedPartialScore edge (greedyLabelPass edge C values slots assigned).1 (greedyLabelPass edge C values slots assigned).2 C ≤ normalizedPartialScore edge assigned.1 assigned.2 C ∧ (∀ slot ∈ slots, ∃ (word : T → G), Sum.elim (greedyLabelPass edge C values slots assigned).1 (greedyLabelPass edge C values slots assigned).2 slot = some word) ∧ ∀ (slot : V ⊕ F) (word : T → G), Sum.elim assigned.1 assigned.2 slot = some word → Sum.elim (greedyLabelPass edge C values slots assigned).1 (greedyLabelPass edge C values slots assigned).2 slot = some word

The full pass never increases the joint score, fills every visited slot and preserves all initially assigned labels. Candidate coverage concerns whole words; duplicates are allowed.

theorem Cslib.BalancedSchedules.greedySchedules_candidates_length {T : Type u_4} {G : Type u_5} [Fintype T] [Fintype G] [FinEnum T] [FinEnum G] : (List.Pi.enum fun (x : T) => G).length = Fintype.card G ^ Fintype.card T

The whole-label candidate list has exactly r ^ Q entries, including the single empty word when Q = 0.

theorem Cslib.BalancedSchedules.greedySchedules_slots_length {V : Type u_2} {F : Type u_3} [Fintype V] [FinEnum V] [FinEnum F] : (List.map Sum.inl (FinEnum.toList V) ++ List.map Sum.inr (FinEnum.toList F)).length = Fintype.card V + Fintype.card F

The traversal visits exactly one slot for each variable and factor.

def Cslib.BalancedSchedules.greedySchedules {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [Fintype T] [Fintype G] [FinEnum V] [FinEnum F] [FinEnum T] [FinEnum G] (edge : E → F × V) (C : ℕ) (g₀ : G) : (V → T → G) × (F → T → G)

Construct schedules by fixing all variables, then all factors, in their explicit finite orders. Candidate whole labels use List.Pi.enum; no good-label witness is supplied. Normalize empty factors to the constant g₀ schedule after the pass.

theorem Cslib.BalancedSchedules.greedySchedules_empty_factor {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [Fintype T] [Fintype G] [FinEnum V] [FinEnum F] [FinEnum T] [FinEnum G] (edge : E → F × V) (C : ℕ) (g₀ : G) {f : F} (hf : ¬∃ (e : E), (edge e).1 = f) : (greedySchedules edge C g₀).2 f = fun (x : T) => g₀

Every empty factor gets the specified constant schedule, independently of tie breaking.

theorem Cslib.BalancedSchedules.greedySchedules_score_le {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [Fintype T] [Fintype G] [FinEnum V] [FinEnum F] [FinEnum T] [FinEnum G] (edge : E → F × V) (C : ℕ) (g₀ : G) : (potential fun (e : E) => ((greedySchedules edge C g₀).1 (edge e).2, (greedySchedules edge C g₀).2 (edge e).1)) / (↑(Fintype.card E) * ↑C) + (∑ t : T, potential fun (v : V) => (greedySchedules edge C g₀).1 v t) / (↑(Fintype.card T) * ↑(Fintype.card V)) ≤ Finset.univ.expect fun (a : V → T → G) => Finset.univ.expect fun (d : F → T → G) => (potential fun (e : E) => (a (edge e).2, d (edge e).1)) / (↑(Fintype.card E) * ↑C) + (∑ t : T, potential fun (v : V) => a v t) / (↑(Fintype.card T) * ↑(Fintype.card V))

The complete deterministic construction has joint normalized potential at most the initial finite-uniform average. All choices are whole schedules; repeated incidence endpoints remain correlated. Empty index types and zero normalization denominators retain their rational meaning.

theorem Cslib.BalancedSchedules.greedySchedules_score_le_two {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [Fintype T] [Fintype G] [FinEnum V] [FinEnum F] [FinEnum T] [FinEnum G] [Nonempty T] [Nonempty V] (edge : E → F × V) {b w : ℕ} (hb : ∀ (e : E), {e' : E | (edge e').2 = (edge e).2}.card ≤ b) (hw : ∀ (e : E), {e' : E | (edge e').1 = (edge e).1}.card ≤ w) (hbw : 0 < b + w) (hE : 0 < Fintype.card E) (g₀ : G) : (potential fun (e : E) => ((greedySchedules edge (b + w) g₀).1 (edge e).2, (greedySchedules edge (b + w) g₀).2 (edge e).1)) / (↑(Fintype.card E) * ↑(b + w)) + (∑ t : T, potential fun (v : V) => (greedySchedules edge (b + w) g₀).1 v t) / (↑(Fintype.card T) * ↑(Fintype.card V)) ≤ 2

Under the incidence degree bounds, the constructed schedules have normalized potential at most two, by the established finite-average incidence and group estimates.

theorem Cslib.BalancedSchedules.greedySchedules_balanced {E : Type u_1} {V : Type u_2} {F : Type u_3} {T : Type u_4} {G : Type u_5} [Fintype E] [Fintype V] [Fintype T] [Fintype G] [FinEnum V] [FinEnum F] [FinEnum T] [FinEnum G] [Nonempty T] [Nonempty V] (edge : E → F × V) {b w : ℕ} (hb : ∀ (e : E), {e' : E | (edge e').2 = (edge e).2}.card ≤ b) (hw : ∀ (e : E), {e' : E | (edge e').1 = (edge e).1}.card ≤ w) (hbw : 0 < b + w) (hincidenceSize : 2 * (b + w) * Fintype.card ((T → G) × (T → G)) ^ 2 ≤ Fintype.card E) (hgroupSize : 2 * Fintype.card T * Fintype.card G ^ 2 ≤ Fintype.card V) (g₀ : G) : (∀ (u : (T → G) × (T → G)), occupancy (fun (e : E) => ((greedySchedules edge (b + w) g₀).1 (edge e).2, (greedySchedules edge (b + w) g₀).2 (edge e).1)) u * Fintype.card ((T → G) × (T → G)) ≤ 2 * Fintype.card E) ∧ ∀ (t : T) (g : G), occupancy (fun (v : V) => (greedySchedules edge (b + w) g₀).1 v t) g * Fintype.card G ≤ 2 * Fintype.card V

The actual constructed schedules satisfy both occupancy bounds of Lemma 4.5 under its size hypotheses. Empty factors have the prescribed constant labels by greedySchedules_empty_factor. This certifies the result of the program, not its bit cost.