Runtime construction of balanced label schedules

Completes the (n + m)-slot greedy pass and empty-scope factor normalization of Lemma 4.5 of [OAI26c] (printed pp. 30–32) on top of Complexity.Computability.PolyTime.GreedySlotScore.

1. Streaming (n + m)-slot pass: greedySchedulePass iterates greedySlotStepBody via Cslib.GenericRAM.IndexFold.run across all n variable and m factor slots using streamBestSlotLabel, and constructBalancedSchedules normalizes empty-scope factors (∀ e ∈ edges, e.1 ≠ f) to List.replicate Q 0.
2. Lemma 4.5 occupancy bounds: constructBalancedSchedules_balanced bridges the runtime pass to greedyLabelPass, proving empty-factor normalization and both occupancy bounds under (4.13).
3. Bit-length bounds and native certificates: length_encOuterState_run_le, length_encOuterState_run_valid_le, greedySchedulePassCertificate, and constructBalancedSchedulesCertificate certify O((r ^ Q + 1) * poly(|input|)) native time and polynomial workspace (ComputableInPolySpace).

Public encoded ComputableInPolyTime, NativeCertificate, ComputableInO, and ComputableInPolySpace theorems govern slotOfIndex, greedySchedulePass, constructBalancedSchedules, and their certificates (built on the concrete list/integer step and postprocessing subroutines pendingSlotOfState, greedySlotStepBody, and normalizeEmptyFactorSchedules) under encScheduleParams and encOuterAcc, whereas constructedVarSchedule and constructedFactorSchedule are unencoded typed specification bridges (Fin n → Fin Q → Fin r and Fin m → Fin Q → Fin r) to greedyLabelPass, completeLabels, normalizeEmptyFactors, potential, and occupancy. Total fallback conventions: slotOfIndex caps s at n + m via min (n + m) s before unary subtraction and returns none for s ≥ n + m; pendingSlotOfState and greedySlotStepBody leave assigned or out-of-range indices unchanged; when r = 0 (Q > 0, so r ^ Q = 0) or a slot is none, fallback words are List.replicate Q 0 (when Q = 0, every word is []); normalizeEmptyFactorSchedules sets every empty-scope factor (∀ e ∈ edges, e.1 ≠ f) to List.replicate Q 0 (group ⟨0, hr⟩ for d_f(t) = 1); and constructedVarSchedule / constructedFactorSchedule clamp out-of-range digits or missing positions to 0 via wordToSchedule.

Main definitions

• slotOfIndex, ScheduleParams, pendingSlotOfState, greedySlotStepBody: outer (n + m)-slot decoding and single-slot step callback over IndexFold.run.
• greedySchedulePass, normalizeEmptyFactorSchedules, constructBalancedSchedules: full greedy pass, empty-scope factor normalization, and complete schedule constructor.
• constructedVarSchedule, constructedFactorSchedule: typed schedule bridges.
• encScheduleParams, encOuterAcc, greedySchedulePassCertificate, constructBalancedSchedulesCertificate: encodings and uniform NativeCertificates.

Main results

• run_greedySlotStepBody_wf, wf_constructBalancedSchedules, getD_constructBalancedSchedules_empty_factor: word well-formedness and empty-scope factor reset.
• greedySchedulePass_eq_greedyLabelPass, constructedSchedules_eq_pass, constructedFactorSchedule_empty_factor: exact agreement with greedyLabelPass and completion.
• constructBalancedSchedules_score_le, constructBalancedSchedules_score_le_two, constructBalancedSchedules_balanced: potential and Lemma 4.5 occupancy bounds under (4.13).
• length_encEdges_le_of_lt, length_encPartialSchedules_le, length_encSlotSelectState_run_valid_le, length_encOuterState_run_valid_le, length_encOuterState_run_le: encoded bit-length bounds across inner and outer loop prefixes.
• computableInPolyTime_slotOfIndex, greedySchedulePassCertificate_bounds, computableInO_greedySchedulePass, computableInPolySpace_greedySchedulePass, constructBalancedSchedulesCertificate_bounds, computableInO_constructBalancedSchedules, computableInPolySpace_constructBalancedSchedules: native time and workspace bounds.

References

• OpenAI, The Exponential Time Hypothesis is False, §4.4, Lemma 4.5, pp. 30–32.

Section 1: (n + m)-slot pass and empty-scope factor normalization

def Cslib.BalancedSchedules.slotOfIndex (n m s : ℕ) : Option (Bool × ℕ)

Decode outer index s < n + m into (false, s) (s < n) or (true, s - n) (n ≤ s < n + m), capping s at n + m so unary conversion stays bounded.

@[reducible, inline]

abbrev Cslib.BalancedSchedules.ScheduleParams : Type

Runtime input tuple ((n, m, Q), (r, C), edges) for full schedule construction.

def Cslib.BalancedSchedules.pendingSlotOfState (state : ℕ × ScheduleParams × List (Option (List ℕ)) × List (Option (List ℕ))) : Option (Bool × ℕ)

Return some slot when s < n + m points to a still-unassigned slot, or none otherwise.

def Cslib.BalancedSchedules.greedySlotStepBody (state : ℕ × ScheduleParams × List (Option (List ℕ)) × List (Option (List ℕ))) : ScheduleParams × List (Option (List ℕ)) × List (Option (List ℕ))

Outer IndexFold.run callback fixing unassigned slot s < n + m via streamBestSlotLabel.

def Cslib.BalancedSchedules.greedySchedulePass (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : List (Option (List ℕ)) × List (Option (List ℕ))

Full (n + m)-slot greedy partial-schedule pass implemented with IndexFold.run.

def Cslib.BalancedSchedules.normalizeEmptyFactorSchedules (Q : ℕ) (edges : List (ℕ × ℕ)) (facWords : List (List ℕ)) : List (List ℕ)

Replace schedules of empty-scope factors (∀ e ∈ edges, e.1 ≠ f) with List.replicate Q 0.

def Cslib.BalancedSchedules.constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : List (List ℕ) × List (List ℕ)

Construct complete balanced variable and factor schedules (varWords, facWords) over [r]^Q by streaming all r ^ Q candidates at each slot and normalizing empty-scope factors (Lemma 4.5).

Section 2: Prefix invariants and Lemma 4.5 occupancy bounds

theorem Cslib.BalancedSchedules.run_greedySlotStepBody_wf (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) (s : ℕ) : have scheds := (GenericRAM.IndexFold.run greedySlotStepBody s (((n, m, Q), (r, C), edges), List.replicate n none, List.replicate m none)).2.2; scheds.1.length = n ∧ scheds.2.length = m ∧ (∀ o ∈ scheds.1, ∀ (w : List ℕ), o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) ∧ ∀ o ∈ scheds.2, ∀ (w : List ℕ), o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1

Outer-loop prefix invariant: at every slot prefix s, varSched has length n, facSched has length m, and every assigned word has length Q with digits < max r 1.

@[simp]

theorem Cslib.BalancedSchedules.length_fst_constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : (constructBalancedSchedules n m Q r C edges).1.length = n

@[simp]

theorem Cslib.BalancedSchedules.length_snd_constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : (constructBalancedSchedules n m Q r C edges).2.length = m

theorem Cslib.BalancedSchedules.wf_constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : (∀ w ∈ (constructBalancedSchedules n m Q r C edges).1, w.length = Q ∧ ∀ x ∈ w, x < max r 1) ∧ ∀ w ∈ (constructBalancedSchedules n m Q r C edges).2, w.length = Q ∧ ∀ x ∈ w, x < max r 1

Every variable and factor word produced by constructBalancedSchedules has exact length Q and digits < max r 1 (hence < r whenever 1 ≤ r).

theorem Cslib.BalancedSchedules.getD_constructBalancedSchedules_empty_factor {n m Q r C f : ℕ} (hf : f < m) (edges : List (ℕ × ℕ)) (hempty : ∀ e ∈ edges, e.1 ≠ f) : (constructBalancedSchedules n m Q r C edges).2.getD f [] = List.replicate Q 0

Concrete empty-factor normalization: any factor f < m absent from edges gets List.replicate Q 0.

theorem Cslib.BalancedSchedules.greedySchedulePass_eq_greedyLabelPass {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (C : ℕ) : greedySchedulePass n m Q r C (edgesOfFin edge) = have slots := (List.ofFn fun (v : Fin n) => Sum.inl v) ++ List.ofFn fun (f : Fin m) => Sum.inr f; have res := greedyLabelPass edge C (candidateScheduleList hr Q) slots (fun (x : Fin n) => none, fun (x : Fin m) => none); (partialScheduleListOfFin res.1, partialScheduleListOfFin res.2)

Exact bridge between the runtime IndexFold.run schedule pass greedySchedulePass and the combinatorial specification greedyLabelPass.

def Cslib.BalancedSchedules.constructedVarSchedule {r : ℕ} (hr : 1 ≤ r) (n m Q C : ℕ) (edges : List (ℕ × ℕ)) (v : Fin n) : Fin Q → Fin r

Typed variable schedule Fin n → Fin Q → Fin r extracted from constructBalancedSchedules.

def Cslib.BalancedSchedules.constructedFactorSchedule {r : ℕ} (hr : 1 ≤ r) (n m Q C : ℕ) (edges : List (ℕ × ℕ)) (f : Fin m) : Fin Q → Fin r

Typed factor schedule Fin m → Fin Q → Fin r extracted from constructBalancedSchedules.

theorem Cslib.BalancedSchedules.constructedSchedules_eq_pass {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (C : ℕ) : have g₀ := ⟨0, hr⟩; have slots := (List.ofFn fun (v : Fin n) => Sum.inl v) ++ List.ofFn fun (f : Fin m) => Sum.inr f; have raw := greedyLabelPass edge C (candidateScheduleList hr Q) slots (fun (x : Fin n) => none, fun (x : Fin m) => none); (constructedVarSchedule hr n m Q C (edgesOfFin edge) = completeLabels raw.1 fun (x : Fin n) (x_1 : Fin Q) => g₀) ∧ constructedFactorSchedule hr n m Q C (edgesOfFin edge) = normalizeEmptyFactors (fun (e : Fin E) => (edge e).1) g₀ (completeLabels raw.2 fun (x : Fin m) (x_1 : Fin Q) => g₀)

Typed schedules extracted from constructBalancedSchedules coincide with completing and normalizing greedyLabelPass.

theorem Cslib.BalancedSchedules.constructedFactorSchedule_empty_factor {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (C : ℕ) {f : Fin m} (hf : ¬∃ (e : Fin E), (edge e).1 = f) : constructedFactorSchedule hr n m Q C (edgesOfFin edge) f = fun (x : Fin Q) => ⟨0, hr⟩

Empty-scope factor schedules are normalized to the constant zero group ⟨0, hr⟩.

theorem Cslib.BalancedSchedules.constructBalancedSchedules_score_le {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (C : ℕ) : have a := constructedVarSchedule hr n m Q C (edgesOfFin edge); have d := constructedFactorSchedule hr n m Q C (edgesOfFin edge); (potential fun (e : Fin E) => (a (edge e).2, d (edge e).1)) / (↑E * ↑C) + (∑ t : Fin Q, potential fun (v : Fin n) => a v t) / (↑Q * ↑n) ≤ Finset.univ.expect fun (a' : Fin n → Fin Q → Fin r) => Finset.univ.expect fun (d' : Fin m → Fin Q → Fin r) => (potential fun (e : Fin E) => (a' (edge e).2, d' (edge e).1)) / (↑E * ↑C) + (∑ t : Fin Q, potential fun (v : Fin n) => a' v t) / (↑Q * ↑n)

constructBalancedSchedules achieves joint normalized potential at most the initial finite-uniform average over (Fin n → Fin Q → Fin r) × (Fin m → Fin Q → Fin r).

theorem Cslib.BalancedSchedules.constructBalancedSchedules_score_le_two {E m n Q r : ℕ} (hr : 1 ≤ r) (hQ : 1 ≤ Q) (hn : 1 ≤ n) (hE : 0 < E) (edge : Fin E → Fin m × Fin n) {b w : ℕ} (hb : ∀ (e : Fin E), {e' : Fin E | (edge e').2 = (edge e).2}.card ≤ b) (hw : ∀ (e : Fin E), {e' : Fin E | (edge e').1 = (edge e).1}.card ≤ w) (hbw : 0 < b + w) : have a := constructedVarSchedule hr n m Q (b + w) (edgesOfFin edge); have d := constructedFactorSchedule hr n m Q (b + w) (edgesOfFin edge); (potential fun (e : Fin E) => (a (edge e).2, d (edge e).1)) / (↑E * ↑(b + w)) + (∑ t : Fin Q, potential fun (v : Fin n) => a v t) / (↑Q * ↑n) ≤ 2

Under Lemma 4.5's degree hypotheses (hb, hw), constructBalancedSchedules achieves joint normalized potential at most 2.

theorem Cslib.BalancedSchedules.constructBalancedSchedules_balanced {E m n Q r : ℕ} (hr : 1 ≤ r) (hQ : 1 ≤ Q) (hn : 1 ≤ n) (edge : Fin E → Fin m × Fin n) {b w : ℕ} (hb : ∀ (e : Fin E), {e' : Fin E | (edge e').2 = (edge e).2}.card ≤ b) (hw : ∀ (e : Fin E), {e' : Fin E | (edge e').1 = (edge e).1}.card ≤ w) (hbw : 0 < b + w) (hincidenceSize : 2 * (b + w) * ((r ^ Q) ^ 2) ^ 2 ≤ E) (hgroupSize : 2 * Q * r ^ 2 ≤ n) : have a := constructedVarSchedule hr n m Q (b + w) (edgesOfFin edge); have d := constructedFactorSchedule hr n m Q (b + w) (edgesOfFin edge); (∀ (f : Fin m), (¬∃ (e : Fin E), (edge e).1 = f) → d f = fun (x : Fin Q) => ⟨0, hr⟩) ∧ (∀ (u : (Fin Q → Fin r) × (Fin Q → Fin r)), occupancy (fun (e : Fin E) => (a (edge e).2, d (edge e).1)) u * (r ^ Q) ^ 2 ≤ 2 * E) ∧ ∀ (t : Fin Q) (g : Fin r), occupancy (fun (v : Fin n) => a v t) g * r ≤ 2 * n

Lemma 4.5 correctness for constructBalancedSchedules ([OAI26c], pp. 30–31): under degree bounds hb, hw, 0 < b + w, and size bounds (4.13) 2 * (b + w) * ((r ^ Q) ^ 2) ^ 2 ≤ E and 2 * Q * r ^ 2 ≤ n, the runtime output satisfies empty-factor normalization and both incidence and variable-group occupancy bounds.

Section 3: Hypergraph-valid bit-length bounds and native machine certificates

def Cslib.BalancedSchedules.encScheduleParams : ScheduleParams ↪ List Bool

Encoding of runtime inputs ((n, m, Q), (r, C), edges) to constructBalancedSchedules.

def Cslib.BalancedSchedules.encOuterAcc : ScheduleParams × List (Option (List ℕ)) × List (Option (List ℕ)) ↪ List Bool

Encoding of outer IndexFold accumulator (ScheduleParams, (varSched, facSched)).

theorem Cslib.BalancedSchedules.length_encEdges_le_of_lt {n m : ℕ} {edges : List (ℕ × ℕ)} (h : ∀ e ∈ edges, e.1 < m ∧ e.2 < n) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) edges).length ≤ edges.length * (6 * (Turing.MultiTapeTM.encNat (n + m)).length + 3)

Encoded bit-length bound for an incidence list edges with endpoints < m and < n.

theorem Cslib.BalancedSchedules.length_encPartialSchedules_le {n m Q r : ℕ} {scheds : List (Option (List ℕ)) × List (Option (List ℕ))} (h1 : scheds.1.length = n) (h2 : scheds.2.length = m) (hw1 : ∀ o ∈ scheds.1, ∀ (w : List ℕ), o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) (hw2 : ∀ o ∈ scheds.2, ∀ (w : List ℕ), o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) : (encPartialSchedules scheds).length ≤ 2 * (n + m) * (2 * Q * (2 * (Turing.MultiTapeTM.encNat r).length + 1) + 3) + 1

Encoded bit-length bound for partial schedule tables (varSched, facSched) of lengths n, m whose assigned words have length Q and digits < max r 1.

theorem Cslib.BalancedSchedules.length_encSlotSelectState_run_valid_le {n m Q r C : ℕ} {edges : List (ℕ × ℕ)} {scheds : List (Option (List ℕ)) × List (Option (List ℕ))} {slot : Bool × ℕ} {j : ℕ} (hj : j ≤ r ^ Q) (hslot : slot.2 ≤ n + m) (hedges : ∀ e ∈ edges, e.1 < m ∧ e.2 < n) (h1 : scheds.1.length = n) (h2 : scheds.2.length = m) (hw1 : ∀ o ∈ scheds.1, ∀ (w : List ℕ), o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) (hw2 : ∀ o ∈ scheds.2, ∀ (w : List ℕ), o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encSlotSelectAcc) (GenericRAM.IndexFold.run selectSlotStep j (((n, Q), (r, C), edges), slot, scheds, none))).length ≤ 36 * (n + m + 1) * (Q + 1) * ((Turing.MultiTapeTM.encNat r).length + 1) + 28 * edges.length * ((Turing.MultiTapeTM.encNat (n + m)).length + 1) + 9 * (Turing.MultiTapeTM.encNat C).length + 60

Explicit O((n + m + 1) * (Q + 1) * log(r + 2) + |E| * log(n + m + 2) + log(C + 2)) inner-loop prefix bit-length bound for valid hypergraph incidences and partial schedules.

theorem Cslib.BalancedSchedules.length_encOuterState_run_valid_le {n m Q r C : ℕ} {edges : List (ℕ × ℕ)} {s : ℕ} (hs : s ≤ n + m) (hedges : ∀ e ∈ edges, e.1 < m ∧ e.2 < n) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encOuterAcc) (GenericRAM.IndexFold.run greedySlotStepBody s (((n, m, Q), (r, C), edges), List.replicate n none, List.replicate m none))).length ≤ 24 * (n + m + 1) * (Q + 1) * ((Turing.MultiTapeTM.encNat r).length + 1) + 28 * edges.length * ((Turing.MultiTapeTM.encNat (n + m)).length + 1) + 8 * (Turing.MultiTapeTM.encNat C).length + 40

All-prefix live-state bit-length bound for the outer (n + m)-slot IndexFold.run loop across every visited slot prefix s ≤ n + m, in terms of input parameters and valid edges.

theorem Cslib.BalancedSchedules.length_encOuterState_run_le (p : ScheduleParams) {s : ℕ} (hs : s ≤ p.1.1 + p.1.2.1) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encOuterAcc) (GenericRAM.IndexFold.run greedySlotStepBody s (p, List.replicate p.1.1 none, List.replicate p.1.2.1 none))).length ≤ 8 * (encScheduleParams p).length ^ 3 + 4 * (encScheduleParams p).length ^ 2 + 10 * (encScheduleParams p).length + 3

Unconditional all-prefix live-state bit-length bound for the outer (n + m)-slot IndexFold.run loop in terms of input bit length L = |encScheduleParams p|.

theorem Cslib.BalancedSchedules.computableInPolyTime_slotOfIndex : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℕ) => slotOfIndex p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encUnary))

slotOfIndex is computable in polynomial time.

noncomputable def Cslib.BalancedSchedules.greedySchedulePassCertificate : GenericRAM.NativeCertificate (fun (p : ScheduleParams) => greedySchedulePass p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2) encScheduleParams encPartialSchedules

Uniform native machine certificate for greedySchedulePass.

noncomputable def Cslib.BalancedSchedules.constructBalancedSchedulesCertificate : GenericRAM.NativeCertificate (fun (p : ScheduleParams) => constructBalancedSchedules p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2) encScheduleParams (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))

Uniform native machine certificate for constructBalancedSchedules ([OAI26c], Lemma 4.5, p. 31).

theorem Cslib.BalancedSchedules.greedySchedulePassCertificate_bounds : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Monotone poly ∧ ∀ (p : ScheduleParams), greedySchedulePassCertificate.time p ≤ (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length ∧ greedySchedulePassCertificate.space p ≤ poly (encScheduleParams p).length

Trajectory-maximum time and polynomial-workspace bounds for greedySchedulePassCertificate: O((r ^ Q + 1) * poly(|input|)) native time and polynomial workspace.

theorem Cslib.BalancedSchedules.computableInO_greedySchedulePass : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (p : ScheduleParams) => greedySchedulePass p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2) encScheduleParams encPartialSchedules (fun (p : ScheduleParams) => (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length) fun (p : ScheduleParams) => poly (encScheduleParams p).length

greedySchedulePass runs in O((r ^ Q + 1) * poly(|input|)) native time and polynomial workspace.

theorem Cslib.BalancedSchedules.computableInPolySpace_greedySchedulePass : Turing.MultiTapeTM.ComputableInPolySpace (fun (p : ScheduleParams) => greedySchedulePass p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2) encScheduleParams encPartialSchedules

greedySchedulePass runs in polynomial workspace (ComputableInPolySpace).

theorem Cslib.BalancedSchedules.constructBalancedSchedulesCertificate_bounds : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Monotone poly ∧ ∀ (p : ScheduleParams), constructBalancedSchedulesCertificate.time p ≤ (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length ∧ constructBalancedSchedulesCertificate.space p ≤ poly (encScheduleParams p).length

Trajectory-maximum time and polynomial-workspace bounds for constructBalancedSchedulesCertificate ([OAI26c], Lemma 4.5, pp. 30–31).

theorem Cslib.BalancedSchedules.computableInO_constructBalancedSchedules : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (p : ScheduleParams) => constructBalancedSchedules p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2) encScheduleParams (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (fun (p : ScheduleParams) => (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length) fun (p : ScheduleParams) => poly (encScheduleParams p).length

constructBalancedSchedules runs in O((r ^ Q + 1) * poly(|input|)) native time and polynomial workspace. For valid incidence endpoints, this gives poly(n, m, |E|, D, Q, r, C) bit operations, where D = r ^ (2 * Q).

theorem Cslib.BalancedSchedules.computableInPolySpace_constructBalancedSchedules : Turing.MultiTapeTM.ComputableInPolySpace (fun (p : ScheduleParams) => constructBalancedSchedules p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2) encScheduleParams (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))

constructBalancedSchedules runs in polynomial workspace (ComputableInPolySpace) without materializing r ^ Q candidate words.