Greedy slot-score arithmetic and streaming candidate selection

In §4.4, Lemma 4.5 of [OAI26c] (printed pp. 30–32), schedules a_v, d_f ∈ [r]^Q are chosen one slot at a time over K = r ^ Q candidates per slot. Executing bestVariableLabel and bestFactorLabel on a native machine clears denominators to bounded integers and streams 0 .. r ^ Q - 1 in polynomial workspace.

Encoded ComputableInPolyTime, NativeCertificate, ComputableInO, and ComputableInPolySpace results in Cslib.BalancedSchedules govern the concrete list/integer algorithms (decodeLabelWord, clearedJointScore, updateSlotSchedules, readSlotSchedule, streamBestSlotLabel, streamBestSlotCertificate), while labelWordEquiv, wordToSchedule, scheduleToWord, candidateScheduleList, edgesOfFin, partialScheduleListOfFin, and candidateSlotScore are unencoded typed specification bridges. Total fallback conventions: wordToSchedule clamps digits ≥ r and missing positions to 0; streamBestSlotLabel returns List.replicate Q 0 when r ^ Q = 0; clearedPartialCollision, updateSlotSchedules, and readSlotSchedule use total List.getD / List.set defaults on out-of-bounds indices; and scoreDenom replaces zero normalizers numEdges * C or Q * n by 1.

Main definitions

• decodeLabelWord, labelWordEquiv, wordToSchedule, scheduleToWord, candidateScheduleList: radix-r candidate codec and Fin Q → Fin r schedule bridges.
• clearedPartialCollision, clearedIncidenceCollisions, clearedIncidencePotential, clearedGroupCollisions, clearedGroupPotential, scoreDenom, clearedJointScore: cleared-integer collision and joint score arithmetic.
• edgesOfFin, partialScheduleListOfFin, encPartialSchedules, encScoreParams, encSlotSelectAcc, StreamSlotIn, encStreamSlotIn: list bridges and machine encodings.
• updateSlotSchedules, readSlotSchedule, SlotSelectAcc, selectSlotStep, streamBestSlotLabel, candidateSlotScore, streamBestSlotCertificate: streaming IndexFold single-slot selector and its uniform NativeCertificate.

Main results

• decodeLabelWord_ofDigits, ofDigits_decodeLabelWord, wordToSchedule_decodeLabelWord_eq_finFunctionFinEquiv_symm, computableInPolyTime_decodeLabelWord: radix bijection and poly-time decoding.
• clearedJointScore_le, length_encNat_clearedJointScore_le, normalizedPartialScore_eq_clearedJointScore_div, clearedJointScore_lt_iff_normalizedPartialScore_lt, clearedJointScore_le_iff_normalizedPartialScore_le, computableInPolyTime_clearedJointScore: logarithmic bit bound, exact rational score equivalence, and poly-time score evaluation.
• exists_min_index_streamBestSlotLabel, streamBestSlotLabel_false_eq_bestVariableLabel, streamBestSlotLabel_true_eq_bestFactorLabel: first-minimizer and bestVariableLabel / bestFactorLabel bridges.
• length_encSlotSelectState_run_le, streamBestSlotCertificate_bounds, computableInO_streamBestSlotLabel, computableInPolySpace_streamBestSlotLabel: all-prefix live-state bit bound, O((r ^ Q + 1) * poly(|input|)) native time, and polynomial workspace.

References

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

Section 1: Radix-r candidate word decoder and bijections

theorem Cslib.BalancedSchedules.length_encNat_pow_le (r Q : ℕ) : (Turing.MultiTapeTM.encNat (r ^ Q)).length ≤ Q * (Turing.MultiTapeTM.encNat r).length + 1

Binary bit-length bound for r ^ Q: at most Q * |encNat r| + 1.

def Cslib.BalancedSchedules.decodeLabelWord (r Q j : ℕ) : List ℕ

Decode binary candidate index j into the length-Q radix-r word of digits via Cslib.Radix.digit ([OAI26c], Lemma 4.5, p. 31).

@[simp]

theorem Cslib.BalancedSchedules.decodeLabelWord_zero_right (r j : ℕ) : decodeLabelWord r 0 j = []

@[simp]

theorem Cslib.BalancedSchedules.decodeLabelWord_one_left (Q j : ℕ) : decodeLabelWord 1 Q j = List.replicate Q 0

@[simp]

theorem Cslib.BalancedSchedules.length_decodeLabelWord (r Q j : ℕ) : (decodeLabelWord r Q j).length = Q

theorem Cslib.BalancedSchedules.getElem_decodeLabelWord (r Q j t : ℕ) (ht : t < Q) : (decodeLabelWord r Q j)[t] = Radix.digit r j t

theorem Cslib.BalancedSchedules.mem_decodeLabelWord_lt {r Q j x : ℕ} (hr : 1 ≤ r) (hx : x ∈ decodeLabelWord r Q j) : x < r

Every digit of decodeLabelWord r Q j is strictly less than r whenever 1 ≤ r.

theorem Cslib.BalancedSchedules.mem_decodeLabelWord_lt_max {r Q j x : ℕ} (hj : j < r ^ Q) (hx : x ∈ decodeLabelWord r Q j) : x < max r 1

For any j < r ^ Q (even when r = 0, Q = 0), every digit of decodeLabelWord r Q j is < max r 1.

theorem Cslib.BalancedSchedules.decodeLabelWord_ofDigits {r : ℕ} (hr : 1 ≤ r) {w : List ℕ} (hw : ∀ x ∈ w, x < r) : decodeLabelWord r w.length (Nat.ofDigits r w) = w

Decoding Nat.ofDigits r w for any bounded word w recovers w.

theorem Cslib.BalancedSchedules.ofDigits_decodeLabelWord {r Q j : ℕ} (hj : j < r ^ Q) : Nat.ofDigits r (decodeLabelWord r Q j) = j

Nat.ofDigits r on decodeLabelWord r Q j recovers j for all j < r ^ Q (including Q = 0 and r = 1).

def Cslib.BalancedSchedules.labelWordEquiv {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) : Fin (r ^ Q) ≃ { w : List ℕ // w.length = Q ∧ ∀ x ∈ w, x < r }

Exact bijection between binary indices Fin (r ^ Q) and length-Q words over {0, …, r - 1} (including Q = 0 and r = 1).

def Cslib.BalancedSchedules.wordToSchedule {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) (w : List ℕ) (t : Fin Q) : Fin r

Convert a concrete digit list w : List ℕ into a typed schedule Fin Q → Fin r, clamping out-of-range digits to 0.

def Cslib.BalancedSchedules.scheduleToWord {r Q : ℕ} (a : Fin Q → Fin r) : List ℕ

Convert a typed schedule a : Fin Q → Fin r into its length-Q digit list.

@[simp]

theorem Cslib.BalancedSchedules.length_scheduleToWord {r Q : ℕ} (a : Fin Q → Fin r) : (scheduleToWord a).length = Q

theorem Cslib.BalancedSchedules.mem_scheduleToWord_lt {r Q : ℕ} (a : Fin Q → Fin r) {x : ℕ} (hx : x ∈ scheduleToWord a) : x < r

@[simp]

theorem Cslib.BalancedSchedules.wordToSchedule_scheduleToWord {r : ℕ} (hr : 1 ≤ r) {Q : ℕ} (a : Fin Q → Fin r) : wordToSchedule hr Q (scheduleToWord a) = a

theorem Cslib.BalancedSchedules.scheduleToWord_inj {r : ℕ} (hr : 1 ≤ r) {Q : ℕ} {a b : Fin Q → Fin r} (h : scheduleToWord a = scheduleToWord b) : a = b

theorem Cslib.BalancedSchedules.scheduleToWord_wordToSchedule {r : ℕ} (hr : 1 ≤ r) {Q : ℕ} {w : List ℕ} (hlen : w.length = Q) (hw : ∀ x ∈ w, x < r) : scheduleToWord (wordToSchedule hr Q w) = w

theorem Cslib.BalancedSchedules.wordToSchedule_decodeLabelWord_eq_finFunctionFinEquiv_symm {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) (j : Fin (r ^ Q)) : wordToSchedule hr Q (decodeLabelWord r Q ↑j) = finFunctionFinEquiv.symm j

wordToSchedule composed with decodeLabelWord agrees identically with the standard bijection finFunctionFinEquiv.symm : Fin (r ^ Q) ≃ (Fin Q → Fin r).

def Cslib.BalancedSchedules.candidateScheduleList {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) : List (Fin Q → Fin r)

Exhaustive list of candidate schedules Fin Q → Fin r in 0 .. r ^ Q - 1 radix order.

theorem Cslib.BalancedSchedules.mem_candidateScheduleList {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) (a : Fin Q → Fin r) : a ∈ candidateScheduleList hr Q

theorem Cslib.BalancedSchedules.length_encList_word_le {Q r : ℕ} {w : List ℕ} (hlen : w.length = Q) (hw : ∀ x ∈ w, x < max r 1) : ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) w).length ≤ Q * (2 * (Turing.MultiTapeTM.encNat r).length + 1)

Encoded bit-length bound for any word of length Q with digits < max r 1.

theorem Cslib.BalancedSchedules.computableInPolyTime_decodeLabelWord : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℕ) => decodeLabelWord p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

decodeLabelWord r Q j is computable in polynomial time from binary r, unary Q, and binary j.

theorem Cslib.BalancedSchedules.computableInPolyTime_decodeLabelWord' {α : Type} {input : α ↪ List Bool} {r Q j : α → ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encNat) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q input Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j input Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => decodeLabelWord (r a) (Q a) (j a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Section 2: Cleared-integer collision scores and exact rational bridge

def Cslib.BalancedSchedules.clearedPartialCollision {α : Type u_1} [DecidableEq α] (cardL : ℕ) (assigned : List (Option α)) (i j : ℕ) : ℕ

Cleared-integer collision count for two indices i, j over a label space of size cardL: returns cardL when i = j or both assigned values agree, 0 when both are assigned and distinct, and 1 when at least one slot is unassigned (1 = cardL * (1 / cardL)).

def Cslib.BalancedSchedules.clearedIncidenceCollisions (K : ℕ) (edges : List (ℕ × ℕ)) (varSched facSched : List (Option (List ℕ))) : ℕ

Sum of cleared incidence-pair collisions over edges : List (ℕ × ℕ) ((f, v) pairs), scaled by K ^ 2 = (r ^ Q) ^ 2.

def Cslib.BalancedSchedules.clearedIncidencePotential (K : ℕ) (edges : List (ℕ × ℕ)) (varSched facSched : List (Option (List ℕ))) : ℕ

Cleared-integer numerator of partialIncidencePotential over common denominator K ^ 2.

def Cslib.BalancedSchedules.clearedGroupCollisions (n Q r : ℕ) (varSched : List (Option (List ℕ))) : ℕ

Sum of cleared variable-coordinate collisions across t < Q and v, v' < n, scaled by r.

def Cslib.BalancedSchedules.clearedGroupPotential (n Q r : ℕ) (varSched : List (Option (List ℕ))) : ℕ

Cleared-integer numerator of partialGroupPotential over common denominator r.

def Cslib.BalancedSchedules.scoreDenom (numEdges n Q r C : ℕ) : ℕ

Common positive integer denominator clearing normalizedPartialScore across all candidate evaluations without rational GCD reductions ([OAI26c], Lemma 4.5, p. 31).

def Cslib.BalancedSchedules.clearedJointScore (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (varSched facSched : List (Option (List ℕ))) : ℕ

Exact natural-number numerator of normalizedPartialScore over scoreDenom.

theorem Cslib.BalancedSchedules.scoreDenom_pos (numEdges n Q : ℕ) {r : ℕ} (hr : 1 ≤ r) (C : ℕ) : 0 < scoreDenom numEdges n Q r C

def Cslib.BalancedSchedules.edgesOfFin {E m n : ℕ} (edge : Fin E → Fin m × Fin n) : List (ℕ × ℕ)

Concrete incidence list [(f₀, v₀), …] extracted from edge : Fin E → Fin m × Fin n.

@[simp]

theorem Cslib.BalancedSchedules.length_edgesOfFin {E m n : ℕ} (edge : Fin E → Fin m × Fin n) : (edgesOfFin edge).length = E

def Cslib.BalancedSchedules.partialScheduleListOfFin {N Q r : ℕ} (assigned : Fin N → Option (Fin Q → Fin r)) : List (Option (List ℕ))

Concrete partial schedule list extracted from Fin N → Option (Fin Q → Fin r).

@[simp]

theorem Cslib.BalancedSchedules.length_partialScheduleListOfFin {N Q r : ℕ} (assigned : Fin N → Option (Fin Q → Fin r)) : (partialScheduleListOfFin assigned).length = N

theorem Cslib.BalancedSchedules.clearedJointScore_le (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (varSched facSched : List (Option (List ℕ))) : clearedJointScore n Q r C edges varSched facSched ≤ edges.length ^ 2 * (r ^ Q + 1) ^ 2 * (r * (Q * n + 1)) + Q * n ^ 2 * (r + 1) * ((r ^ Q) ^ 2 * (edges.length * C + 1))

Unconditional upper bound on clearedJointScore, independent of (varSched, facSched).

theorem Cslib.BalancedSchedules.length_encNat_clearedJointScore_le (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (varSched facSched : List (Option (List ℕ))) : (Turing.MultiTapeTM.encNat (clearedJointScore n Q r C edges varSched facSched)).length ≤ 2 * Q * (Turing.MultiTapeTM.encNat r).length + 2 * (Turing.MultiTapeTM.encNat r).length + (Turing.MultiTapeTM.encNat C).length + 2 * (Turing.MultiTapeTM.encNat edges.length).length + 2 * (Turing.MultiTapeTM.encNat n).length + 2 * (Turing.MultiTapeTM.encNat Q).length + 18

Logarithmic bit-length bound on encNat (clearedJointScore ...) matching Lemma 4.5's O(log(2D) + log(2M) + log(2n) + log(2Q) + log(2 + b + w)) bit bound (p. 31), independent of (varSched, facSched).

theorem Cslib.BalancedSchedules.clearedPartialCollision_eq_mul_partialCollision {N Q r : ℕ} (hr : 1 ≤ r) (assigned : Fin N → Option (Fin Q → Fin r)) (i j : Fin N) : ↑(clearedPartialCollision (r ^ Q) (partialScheduleListOfFin assigned) ↑i ↑j) = ↑(r ^ Q) * partialCollision assigned i j

Exact rational collision identity on whole-word schedules (L = Fin Q → Fin r).

theorem Cslib.BalancedSchedules.normalizedPartialScore_eq_clearedJointScore_div {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (varLabels : Fin n → Option (Fin Q → Fin r)) (factorLabels : Fin m → Option (Fin Q → Fin r)) (C : ℕ) : normalizedPartialScore edge varLabels factorLabels C = ↑(clearedJointScore n Q r C (edgesOfFin edge) (partialScheduleListOfFin varLabels) (partialScheduleListOfFin factorLabels)) / ↑(scoreDenom E n Q r C)

Exact cleared-integer score identity: for any 1 ≤ r, normalizedPartialScore equals clearedJointScore / scoreDenom identically (including when E = 0, C = 0, Q = 0, or n = 0).

theorem Cslib.BalancedSchedules.clearedJointScore_lt_iff_normalizedPartialScore_lt {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (v₁ v₂ : Fin n → Option (Fin Q → Fin r)) (f₁ f₂ : Fin m → Option (Fin Q → Fin r)) (C : ℕ) : clearedJointScore n Q r C (edgesOfFin edge) (partialScheduleListOfFin v₁) (partialScheduleListOfFin f₁) < clearedJointScore n Q r C (edgesOfFin edge) (partialScheduleListOfFin v₂) (partialScheduleListOfFin f₂) ↔ normalizedPartialScore edge v₁ f₁ C < normalizedPartialScore edge v₂ f₂ C

Strict < on clearedJointScore : ℕ is equivalent to < on normalizedPartialScore : ℚ.

theorem Cslib.BalancedSchedules.clearedJointScore_le_iff_normalizedPartialScore_le {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (v₁ v₂ : Fin n → Option (Fin Q → Fin r)) (f₁ f₂ : Fin m → Option (Fin Q → Fin r)) (C : ℕ) : clearedJointScore n Q r C (edgesOfFin edge) (partialScheduleListOfFin v₁) (partialScheduleListOfFin f₁) ≤ clearedJointScore n Q r C (edgesOfFin edge) (partialScheduleListOfFin v₂) (partialScheduleListOfFin f₂) ↔ normalizedPartialScore edge v₁ f₁ C ≤ normalizedPartialScore edge v₂ f₂ C

Non-strict ≤ on clearedJointScore : ℕ is equivalent to ≤ on normalizedPartialScore : ℚ.

Polynomial-time certificate for clearedJointScore

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

Encoding of a pair (varSched, facSched) of partial schedule tables.

def Cslib.BalancedSchedules.encScoreParams : (ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ) ↪ List Bool

Encoding of score parameters ((n, Q), (r, C), edges).

theorem Cslib.BalancedSchedules.computableInPolyTime_clearedJointScore : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ)) × List (Option (List ℕ)) × List (Option (List ℕ))) => clearedJointScore p.1.1.1 p.1.1.2 p.1.2.1.1 p.1.2.1.2 p.1.2.2 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair encScoreParams encPartialSchedules) Turing.MultiTapeTM.encNat

clearedJointScore is computable in polynomial time in its encoded inputs.

Section 3: Streaming IndexFold slot selector and rational minimizer bridges

def Cslib.BalancedSchedules.updateSlotSchedules (slot : Bool × ℕ) (val : Option (List ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) : List (Option (List ℕ)) × List (Option (List ℕ))

Update a variable ((false, v)) or factor ((true, f)) slot in (varSched, facSched).

def Cslib.BalancedSchedules.readSlotSchedule (slot : Bool × ℕ) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) : Option (List ℕ)

Read a variable ((false, v)) or factor ((true, f)) slot from (varSched, facSched).

@[reducible, inline]

abbrev Cslib.BalancedSchedules.SlotSelectAcc : Type

Live accumulator for inner IndexFold.run candidate streaming over j ∈ 0 .. r ^ Q - 1.

def Cslib.BalancedSchedules.selectSlotStep (state : ℕ × SlotSelectAcc) : SlotSelectAcc

Inner IndexFold.run callback evaluating candidate decodeLabelWord r Q j under clearedJointScore and retaining the first strict minimizer (candScore < best.2).

def Cslib.BalancedSchedules.streamBestSlotLabel (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) : List ℕ

Stream j ∈ 0 .. r ^ Q - 1 via Cslib.GenericRAM.IndexFold.run to select the first candidate word minimizing clearedJointScore for slot, falling back to List.replicate Q 0 if r ^ Q = 0 ([OAI26c], Lemma 4.5, p. 31).

def Cslib.BalancedSchedules.candidateSlotScore (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) (j : ℕ) : ℕ

Cleared-integer score of candidate decodeLabelWord r Q j placed in slot.

theorem Cslib.BalancedSchedules.exists_min_index_streamBestSlotLabel (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) (hpos : 0 < r ^ Q) : ∃ jStar < r ^ Q, streamBestSlotLabel n Q r C edges scheds slot = decodeLabelWord r Q jStar ∧ (∀ j < r ^ Q, candidateSlotScore n Q r C edges scheds slot jStar ≤ candidateSlotScore n Q r C edges scheds slot j) ∧ ∀ j < jStar, candidateSlotScore n Q r C edges scheds slot jStar < candidateSlotScore n Q r C edges scheds slot j

First-minimizer characterization of streamBestSlotLabel when 0 < r ^ Q.

@[simp]

theorem Cslib.BalancedSchedules.length_streamBestSlotLabel (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) : (streamBestSlotLabel n Q r C edges scheds slot).length = Q

theorem Cslib.BalancedSchedules.mem_streamBestSlotLabel_lt_max (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) {x : ℕ} (hx : x ∈ streamBestSlotLabel n Q r C edges scheds slot) : x < max r 1

theorem Cslib.BalancedSchedules.mem_streamBestSlotLabel_lt {r : ℕ} (hr : 1 ≤ r) (n Q C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) {x : ℕ} (hx : x ∈ streamBestSlotLabel n Q r C edges scheds slot) : x < r

theorem Cslib.BalancedSchedules.set_partialScheduleListOfFin {N Q r : ℕ} {hr : 1 ≤ r} (assigned : Fin N → Option (Fin Q → Fin r)) (k : Fin N) (w : List ℕ) (hlen : w.length = Q) (hw : ∀ x ∈ w, x < r) : (partialScheduleListOfFin assigned).set (↑k) (some w) = partialScheduleListOfFin (Function.update assigned k (some (wordToSchedule hr Q w)))

Updating partialScheduleListOfFin at index k.val with a valid length-Q word w commutes with Function.update via wordToSchedule.

theorem Cslib.BalancedSchedules.streamBestSlotLabel_false_eq_bestVariableLabel {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (varLabels : Fin n → Option (Fin Q → Fin r)) (factorLabels : Fin m → Option (Fin Q → Fin r)) (C : ℕ) (v : Fin n) : some (wordToSchedule hr Q (streamBestSlotLabel n Q r C (edgesOfFin edge) (partialScheduleListOfFin varLabels, partialScheduleListOfFin factorLabels) (false, ↑v))) = bestVariableLabel edge varLabels factorLabels C v (candidateScheduleList hr Q)

Exact agreement between streamBestSlotLabel at variable slot (false, v.val) and bestVariableLabel over candidateScheduleList hr Q.

theorem Cslib.BalancedSchedules.streamBestSlotLabel_true_eq_bestFactorLabel {E m n Q r : ℕ} (hr : 1 ≤ r) (edge : Fin E → Fin m × Fin n) (varLabels : Fin n → Option (Fin Q → Fin r)) (factorLabels : Fin m → Option (Fin Q → Fin r)) (C : ℕ) (f : Fin m) : some (wordToSchedule hr Q (streamBestSlotLabel n Q r C (edgesOfFin edge) (partialScheduleListOfFin varLabels, partialScheduleListOfFin factorLabels) (true, ↑f))) = bestFactorLabel edge varLabels factorLabels C f (candidateScheduleList hr Q)

Exact agreement between streamBestSlotLabel at factor slot (true, f.val) and bestFactorLabel over candidateScheduleList hr Q.

Section 4: All-prefix bit-length bounds, NativeCertificate, and ComputableInPolySpace

def Cslib.BalancedSchedules.encSlotSelectAcc : SlotSelectAcc ↪ List Bool

Encoding of inner IndexFold accumulator SlotSelectAcc.

@[reducible, inline]

abbrev Cslib.BalancedSchedules.StreamSlotIn : Type

Runtime input tuple for streamBestSlotLabel.

def Cslib.BalancedSchedules.encStreamSlotIn : StreamSlotIn ↪ List Bool

Encoding of runtime inputs to streamBestSlotLabel.

theorem Cslib.BalancedSchedules.length_encSlotSelectState_run_le (n Q r C : ℕ) (edges : List (ℕ × ℕ)) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) {j : ℕ} (hj : j ≤ r ^ Q) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encSlotSelectAcc) (GenericRAM.IndexFold.run selectSlotStep j (((n, Q), (r, C), edges), slot, scheds, none))).length ≤ 2 * (encStreamSlotIn (((n, Q), (r, C), edges), slot, scheds)).length + 8 * Q * (Turing.MultiTapeTM.encNat r).length + 4 * Q + 2 * (Turing.MultiTapeTM.encNat r).length + (Turing.MultiTapeTM.encNat C).length + 2 * (Turing.MultiTapeTM.encNat edges.length).length + 2 * (Turing.MultiTapeTM.encNat n).length + 2 * (Turing.MultiTapeTM.encNat Q).length + 28

All-prefix live-state bit-length bound for the inner IndexFold.run selectSlotStep loop across every visited prefix j ≤ r ^ Q (never multiplying workspace by r ^ Q).

theorem Cslib.BalancedSchedules.computableInPolyTime_updateSlotSchedules : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((Bool × ℕ) × Option (List ℕ)) × List (Option (List ℕ)) × List (Option (List ℕ))) => updateSlotSchedules p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) encPartialSchedules) encPartialSchedules

updateSlotSchedules is computable in polynomial time.

theorem Cslib.BalancedSchedules.computableInPolyTime_readSlotSchedule : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Bool × ℕ) × List (Option (List ℕ)) × List (Option (List ℕ))) => readSlotSchedule p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encUnary) encPartialSchedules) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

readSlotSchedule is computable in polynomial time.

noncomputable def Cslib.BalancedSchedules.streamBestSlotCertificate : GenericRAM.NativeCertificate (fun (a : StreamSlotIn) => streamBestSlotLabel a.1.1.1 a.1.1.2 a.1.2.1.1 a.1.2.1.2 a.1.2.2 a.2.2 a.2.1) encStreamSlotIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Uniform native machine certificate for single-slot candidate streaming streamBestSlotLabel.

theorem Cslib.BalancedSchedules.streamBestSlotCertificate_bounds : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Monotone poly ∧ ∀ (a : StreamSlotIn), streamBestSlotCertificate.time a ≤ (a.1.2.1.1 ^ a.1.1.2 + 1) * poly (encStreamSlotIn a).length ∧ streamBestSlotCertificate.space a ≤ poly (encStreamSlotIn a).length

Trajectory-maximum time and polynomial-workspace bounds for streamBestSlotCertificate.

theorem Cslib.BalancedSchedules.computableInO_streamBestSlotLabel : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (a : StreamSlotIn) => streamBestSlotLabel a.1.1.1 a.1.1.2 a.1.2.1.1 a.1.2.1.2 a.1.2.2 a.2.2 a.2.1) encStreamSlotIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : StreamSlotIn) => (a.1.2.1.1 ^ a.1.1.2 + 1) * poly (encStreamSlotIn a).length) fun (a : StreamSlotIn) => poly (encStreamSlotIn a).length

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

theorem Cslib.BalancedSchedules.computableInPolySpace_streamBestSlotLabel : Turing.MultiTapeTM.ComputableInPolySpace (fun (a : StreamSlotIn) => streamBestSlotLabel a.1.1.1 a.1.1.2 a.1.2.1.1 a.1.2.1.2 a.1.2.2 a.2.2 a.2.1) encStreamSlotIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

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