Computable collision scores for partial label schedules

In the conditional-expectation construction in the proof of Lemma 4.5, printed p. 31 of [OAI26c], one whole variable or factor label is fixed at a time. A partial assignment stores a whole label or none at each choice index. Unassigned choices are completed by one uniformly enumerated function: repeated reads of one index never resample its value.

The closed-form incidence and group scores equal the actual finite completion averages. Their normalized average is preserved when an unassigned whole label is fixed. Mathlib List.argmin then gives a deterministic nonincreasing step when its explicit candidate list is exhaustive. The scores enumerate incidence/variable pairs, not full completions.

This supplies score evaluation and one greedy step, not traversal of every choice index, an initial potential estimate, or a new complete schedule-existence theorem. Polynomial rational operation/bit-cost bounds and native machine certification remain separate obligations.

def Cslib.BalancedSchedules.completeLabels {I : Type u_1} {L : Type u_2} (assigned : I → Option L) (filler : I → L) (i : I) : L

Complete a partial assignment, using the same filler value on every read of an index.

def Cslib.BalancedSchedules.partialCollision {I : Type u_1} {L : Type u_2} [DecidableEq I] [Fintype L] [DecidableEq L] (assigned : I → Option L) (i j : I) : ℚ

Exact collision score for two choice indices under a partial assignment. A repeated index scores one, not the reciprocal label count.

theorem Cslib.BalancedSchedules.partialCollision_eq_expect {I : Type u_1} {L : Type u_2} [DecidableEq I] [Fintype L] [DecidableEq L] [Fintype I] [Nonempty L] (assigned : I → Option L) (i j : I) : partialCollision assigned i j = Finset.univ.expect fun (filler : I → L) => if completeLabels assigned filler i = completeLabels assigned filler j then 1 else 0

The computable pair score is the true finite average over completions.

theorem Cslib.BalancedSchedules.expect_partialCollision_update {I : Type u_1} {L : Type u_2} [DecidableEq I] [Fintype L] [DecidableEq L] [Nonempty L] (assigned : I → Option L) (k i j : I) (hk : assigned k = none) : (Finset.univ.expect fun (x : L) => partialCollision (Function.update assigned k (some x)) i j) = partialCollision assigned i j

Averaging the candidate values of one unassigned whole label preserves the pair score.

def Cslib.BalancedSchedules.partialCoordinateCollision {I : Type u_1} [DecidableEq I] {T : Type u_3} {G : Type u_4} [Fintype G] [DecidableEq G] (assigned : I → Option (T → G)) (t : T) (i j : I) : ℚ

Observe one coordinate of a partial assignment of whole schedules.

theorem Cslib.BalancedSchedules.partialCoordinateCollision_eq_expect {I : Type u_1} [DecidableEq I] {T : Type u_3} {G : Type u_4} [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] [Fintype I] (assigned : I → Option (T → G)) (t : T) (i j : I) : partialCoordinateCollision assigned t i j = Finset.univ.expect fun (filler : I → T → G) => if completeLabels assigned filler i t = completeLabels assigned filler j t then 1 else 0

The coordinate score averages over whole schedule completions, not independent incidence-level or point-specific replacements.

theorem Cslib.BalancedSchedules.expect_partialCoordinateCollision_update {I : Type u_1} [DecidableEq I] {T : Type u_3} {G : Type u_4} [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (assigned : I → Option (T → G)) (t : T) (k i j : I) (hk : assigned k = none) : (Finset.univ.expect fun (word : T → G) => partialCoordinateCollision (Function.update assigned k (some word)) t i j) = partialCoordinateCollision assigned t i j

Fixing one whole schedule preserves the average of every coordinate-collision score.

def Cslib.BalancedSchedules.partialIncidenceCollision {L : Type u_2} [Fintype L] [DecidableEq L] {V : Type u_3} {F : Type u_4} [DecidableEq V] [DecidableEq F] (varLabels : V → Option L) (factors : F → Option L) (v v' : V) (f f' : F) : ℚ

Incidence collisions factor only across the independent variable-label and factor-label families. Repeated endpoints within either family are retained in partialCollision.

theorem Cslib.BalancedSchedules.partialIncidenceCollision_eq_expect {L : Type u_2} [Fintype L] [DecidableEq L] {V : Type u_3} {F : Type u_4} [Fintype V] [DecidableEq V] [Fintype F] [DecidableEq F] [Nonempty L] (varLabels : V → Option L) (factors : F → Option L) (v v' : V) (f f' : F) : partialIncidenceCollision varLabels factors v v' f f' = Finset.univ.expect fun (a : V → L) => Finset.univ.expect fun (d : F → L) => if (completeLabels varLabels a v, completeLabels factors d f) = (completeLabels varLabels a v', completeLabels factors d f') then 1 else 0

Exact joint completion average for one pair of incidences.

def Cslib.BalancedSchedules.partialIncidencePotential {L : Type u_2} [Fintype L] [DecidableEq L] {E : Type u_3} {V : Type u_4} {F : Type u_5} [Fintype E] [DecidableEq V] [DecidableEq F] (edge : E → F × V) (varLabels : V → Option L) (factorLabels : F → Option L) : ℚ

Closed rational incidence potential of a partial assignment. The summation is over incidences, not over exponentially many full completions.

theorem Cslib.BalancedSchedules.partialIncidencePotential_eq_expect {L : Type u_2} [Fintype L] [DecidableEq L] {E : Type u_3} {V : Type u_4} {F : Type u_5} [Fintype E] [Fintype V] [DecidableEq V] [Fintype F] [DecidableEq F] [Nonempty L] (edge : E → F × V) (varLabels : V → Option L) (factorLabels : F → Option L) : partialIncidencePotential edge varLabels factorLabels = Finset.univ.expect fun (a : V → L) => Finset.univ.expect fun (d : F → L) => potential fun (e : E) => (completeLabels varLabels a (edge e).2, completeLabels factorLabels d (edge e).1)

The closed incidence formula equals the actual potential averaged over completions. In particular, sharing a variable or factor does not create an independent new choice.

def Cslib.BalancedSchedules.partialGroupPotential {T : Type u_3} {V : Type u_4} {G : Type u_5} [Fintype T] [Fintype V] [DecidableEq V] [Fintype G] [DecidableEq G] (assigned : V → Option (T → G)) : ℚ

Closed rational total group potential, computed from the same partial whole schedules.

theorem Cslib.BalancedSchedules.partialGroupPotential_eq_expect {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] (assigned : V → Option (T → G)) : partialGroupPotential assigned = Finset.univ.expect fun (filler : V → T → G) => ∑ t : T, potential fun (v : V) => completeLabels assigned filler v t

The closed group formula equals the actual group potential averaged over completions of whole schedules. No new independently sampled point labels are introduced.

theorem Cslib.BalancedSchedules.expect_partialIncidenceCollision_update_variable {L : Type u_2} [Fintype L] [DecidableEq L] {V : Type u_3} {F : Type u_4} [DecidableEq V] [DecidableEq F] [Nonempty L] (varLabels : V → Option L) (factorLabels : F → Option L) (k v v' : V) (f f' : F) (hk : varLabels k = none) : (Finset.univ.expect fun (x : L) => partialIncidenceCollision (Function.update varLabels k (some x)) factorLabels v v' f f') = partialIncidenceCollision varLabels factorLabels v v' f f'

Averaging a variable-label update preserves every incidence pair score.

theorem Cslib.BalancedSchedules.expect_partialIncidenceCollision_update_factor {L : Type u_2} [Fintype L] [DecidableEq L] {V : Type u_3} {F : Type u_4} [DecidableEq V] [DecidableEq F] [Nonempty L] (varLabels : V → Option L) (factorLabels : F → Option L) (v v' : V) (k f f' : F) (hk : factorLabels k = none) : (Finset.univ.expect fun (x : L) => partialIncidenceCollision varLabels (Function.update factorLabels k (some x)) v v' f f') = partialIncidenceCollision varLabels factorLabels v v' f f'

Averaging a factor-label update preserves every incidence pair score.

theorem Cslib.BalancedSchedules.expect_partialIncidencePotential_update_variable {L : Type u_2} [Fintype L] [DecidableEq L] {E : Type u_3} {V : Type u_4} {F : Type u_5} [Fintype E] [DecidableEq V] [DecidableEq F] [Nonempty L] (edge : E → F × V) (varLabels : V → Option L) (factorLabels : F → Option L) (k : V) (hk : varLabels k = none) : (Finset.univ.expect fun (x : L) => partialIncidencePotential edge (Function.update varLabels k (some x)) factorLabels) = partialIncidencePotential edge varLabels factorLabels

A whole variable-label update preserves the average closed incidence potential.

theorem Cslib.BalancedSchedules.expect_partialIncidencePotential_update_factor {L : Type u_2} [Fintype L] [DecidableEq L] {E : Type u_3} {V : Type u_4} {F : Type u_5} [Fintype E] [DecidableEq V] [DecidableEq F] [Nonempty L] (edge : E → F × V) (varLabels : V → Option L) (factorLabels : F → Option L) (k : F) (hk : factorLabels k = none) : (Finset.univ.expect fun (x : L) => partialIncidencePotential edge varLabels (Function.update factorLabels k (some x))) = partialIncidencePotential edge varLabels factorLabels

A whole factor-label update preserves the average closed incidence potential.

theorem Cslib.BalancedSchedules.expect_partialGroupPotential_update {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] (assigned : V → Option (T → G)) (k : V) (hk : assigned k = none) : (Finset.univ.expect fun (word : T → G) => partialGroupPotential (Function.update assigned k (some word))) = partialGroupPotential assigned

A whole variable-label update preserves the average closed group potential.

def Cslib.BalancedSchedules.normalizedPartialScore {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) : ℚ

The paper's normalized partial score, with C = b + w. Both normalization denominators remain explicit. This rational value carries no algorithmic cost certificate.

theorem Cslib.BalancedSchedules.normalizedPartialScore_eq_expect {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [Fintype F] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) : normalizedPartialScore edge varLabels factorLabels C = Finset.univ.expect fun (a : V → T → G) => Finset.univ.expect fun (d : F → T → G) => (potential fun (e : E) => (completeLabels varLabels a (edge e).2, completeLabels factorLabels d (edge e).1)) / (↑(Fintype.card E) * ↑C) + (∑ t : T, potential fun (v : V) => completeLabels varLabels a v t) / (↑(Fintype.card T) * ↑(Fintype.card V))

The computable normalized score is the conditional finite average of the actual normalized objective on full completions.

theorem Cslib.BalancedSchedules.expect_normalizedPartialScore_update_variable {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) (k : V) (hk : varLabels k = none) : (Finset.univ.expect fun (word : T → G) => normalizedPartialScore edge (Function.update varLabels k (some word)) factorLabels C) = normalizedPartialScore edge varLabels factorLabels C

Fixing a whole variable schedule preserves the average normalized score. The update is one whole word, shared by all its incidences and all schedule coordinates.

theorem Cslib.BalancedSchedules.expect_normalizedPartialScore_update_factor {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) (k : F) (hk : factorLabels k = none) : (Finset.univ.expect fun (word : T → G) => normalizedPartialScore edge varLabels (Function.update factorLabels k (some word)) C) = normalizedPartialScore edge varLabels factorLabels C

Fixing a whole factor schedule preserves the average normalized score; it changes no variable-group assignment.

def Cslib.BalancedSchedules.bestVariableLabel {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) (k : V) (values : List (T → G)) : Option (T → G)

Deterministic candidate selection for one variable: enumerate the supplied whole labels and retain the first minimum. Empty candidate lists return none.

theorem Cslib.BalancedSchedules.bestVariableLabel_spec {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) (k : V) (hk : varLabels k = none) (values : List (T → G)) (hcover : ∀ (word : T → G), word ∈ values) : ∃ (chosen : T → G), bestVariableLabel edge varLabels factorLabels C k values = some chosen ∧ normalizedPartialScore edge (Function.update varLabels k (some chosen)) factorLabels C ≤ normalizedPartialScore edge varLabels factorLabels C

With an exhaustive candidate list, the actual deterministic update does not increase the normalized score. Exhaustiveness is an enumeration condition, not a supplied good-label oracle.

def Cslib.BalancedSchedules.bestFactorLabel {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) (k : F) (values : List (T → G)) : Option (T → G)

Deterministic candidate selection for one factor, without changing variable groups.

theorem Cslib.BalancedSchedules.bestFactorLabel_spec {E : Type u_3} {V : Type u_4} {F : Type u_5} {T : Type u_6} {G : Type u_7} [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq F] [Fintype T] [DecidableEq T] [Fintype G] [DecidableEq G] [Nonempty G] (edge : E → F × V) (varLabels : V → Option (T → G)) (factorLabels : F → Option (T → G)) (C : ℕ) (k : F) (hk : factorLabels k = none) (values : List (T → G)) (hcover : ∀ (word : T → G), word ∈ values) : ∃ (chosen : T → G), bestFactorLabel edge varLabels factorLabels C k values = some chosen ∧ normalizedPartialScore edge varLabels (Function.update factorLabels k (some chosen)) C ≤ normalizedPartialScore edge varLabels factorLabels C

The actual factor update selected from an exhaustive list does not increase the score.