From c20adaa8aeffcefa3f9f8949b4d24548a5e2c148 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Tue, 27 Oct 2026 07:37:56 +0000 Subject: [PATCH 1/4] feat(PolyTime): add greedy slot-score arithmetic and streaming candidate selector (#1226) --- Complexity.lean | 1 + .../PolyTime/GreedySlotScore.lean | 1267 +++++++++++++++++ ComplexityTests/GreedySlotScore.lean | 116 ++ 3 files changed, 1384 insertions(+) create mode 100644 Complexity/Computability/PolyTime/GreedySlotScore.lean create mode 100644 ComplexityTests/GreedySlotScore.lean diff --git a/Complexity.lean b/Complexity.lean index 9fe38d5cca..824839e0ac 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1382,6 +1382,7 @@ public import Complexity.Computability.PolyTime.CNF.GreedyParityContext public import Complexity.Computability.PolyTime.CNF.GreedyParitySearch public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck +public import Complexity.Computability.PolyTime.GreedySlotScore public import Complexity.Computability.PolyTime.Int.ExactDiv public import Complexity.Computability.PolyTime.Int.Jet public import Complexity.Computability.PolyTime.Int.Table diff --git a/Complexity/Computability/PolyTime/GreedySlotScore.lean b/Complexity/Computability/PolyTime/GreedySlotScore.lean new file mode 100644 index 0000000000..ed204d8cf3 --- /dev/null +++ b/Complexity/Computability/PolyTime/GreedySlotScore.lean @@ -0,0 +1,1267 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.GenericRAM.Native.IndexFold +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain +public import Complexity.Foundations.Combinatorics.GreedySchedules +public import Complexity.Foundations.Data.Nat.Radix +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Foundations.Data.List.Lookup +import Complexity.Foundations.Data.List.OfFn +import Mathlib.Data.List.GetD +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Greedy slot-score arithmetic and streaming candidate selection + +In §4.4, Lemma 4.5 of [OpenAI2026ETH] (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*][OpenAI2026ETH], §4.4, Lemma 4.5, pp. 30–32. +-/ + +@[expose] public section + +namespace Cslib.BalancedSchedules + +open Finset Cslib.GenericRAM Turing.MultiTapeTM +open scoped BigOperators + +/-! ### Section 1: Radix-`r` candidate word decoder and bijections -/ + +/-- Binary bit-length bound for `r ^ Q`: at most `Q * |encNat r| + 1`. -/ +theorem length_encNat_pow_le (r Q : ℕ) : + (encNat (r ^ Q)).length ≤ Q * (encNat r).length + 1 := by + simp only [encNat_apply, Nat.size_eq_bits_len]; exact Nat.size_pow_le r Q + +/-- Decode binary candidate index `j` into the length-`Q` radix-`r` word of digits via +`Cslib.Radix.digit` ([OpenAI2026ETH], Lemma 4.5, p. 31). -/ +def decodeLabelWord (r Q j : ℕ) : List ℕ := + (List.range Q).map fun t => Cslib.Radix.digit r j t + +@[simp] theorem decodeLabelWord_zero_right (r j : ℕ) : decodeLabelWord r 0 j = [] := rfl + +@[simp] theorem decodeLabelWord_one_left (Q j : ℕ) : + decodeLabelWord 1 Q j = List.replicate Q 0 := by + apply List.ext_getElem + (by simp only [decodeLabelWord, List.length_map, List.length_range, List.length_replicate]) + intro t _ _ + simp only [decodeLabelWord, List.getElem_map, List.getElem_replicate, + Cslib.Radix.digit_eq_div_pow_mod, Nat.mod_one] + +@[simp] theorem length_decodeLabelWord (r Q j : ℕ) : (decodeLabelWord r Q j).length = Q := by + simp only [decodeLabelWord, List.length_map, List.length_range] + +theorem getElem_decodeLabelWord (r Q j t : ℕ) (ht : t < Q) : + (decodeLabelWord r Q j)[t]'(by simp only [length_decodeLabelWord]; exact ht) = + Cslib.Radix.digit r j t := by + simp only [decodeLabelWord, List.getElem_map, List.getElem_range] + +/-- Every digit of `decodeLabelWord r Q j` is strictly less than `r` whenever `1 ≤ r`. -/ +theorem mem_decodeLabelWord_lt {r Q j x : ℕ} (hr : 1 ≤ r) (hx : x ∈ decodeLabelWord r Q j) : + x < r := by + simp only [decodeLabelWord, List.mem_map, List.mem_range] at hx + obtain ⟨t, _, rfl⟩ := hx; rw [Cslib.Radix.digit_eq_div_pow_mod]; exact Nat.mod_lt _ hr + +/-- For any `j < r ^ Q` (even when `r = 0, Q = 0`), every digit of `decodeLabelWord r Q j` is +`< max r 1`. -/ +theorem mem_decodeLabelWord_lt_max {r Q j x : ℕ} (hj : j < r ^ Q) + (hx : x ∈ decodeLabelWord r Q j) : x < max r 1 := by + rcases Nat.eq_zero_or_pos Q with rfl | hQ + · simp only [decodeLabelWord_zero_right, List.not_mem_nil] at hx + · rcases Nat.eq_zero_or_pos r with rfl | hr + · rw [Nat.zero_pow hQ] at hj; omega + · exact (mem_decodeLabelWord_lt hr hx).trans_le (le_max_left _ _) + +/-- Decoding `Nat.ofDigits r w` for any bounded word `w` recovers `w`. -/ +theorem decodeLabelWord_ofDigits {r : ℕ} (hr : 1 ≤ r) {w : List ℕ} (hw : ∀ x ∈ w, x < r) : + decodeLabelWord r w.length (Nat.ofDigits r w) = w := by + apply List.ext_getElem (length_decodeLabelWord _ _ _) + intro t _ ht; rw [getElem_decodeLabelWord _ _ _ _ ht] + exact Cslib.Radix.digit_ofDigits hr w hw t ht + +/-- `Nat.ofDigits r` on `decodeLabelWord r Q j` recovers `j` for all `j < r ^ Q` (including `Q = 0` +and `r = 1`). -/ +theorem ofDigits_decodeLabelWord {r Q j : ℕ} (hj : j < r ^ Q) : + Nat.ofDigits r (decodeLabelWord r Q j) = j := by + rcases Nat.eq_zero_or_pos Q with rfl | hQ + · simp only [pow_zero, Nat.lt_one_iff] at hj; subst hj; rfl + · obtain ⟨x, hx, rfl⟩ := Nat.exists_ofDigits_ofFn hj + have hr : 0 < r := Nat.zero_lt_of_lt (hx ⟨0, hQ⟩) + congr 1; apply List.ext_getElem (by simp only [length_decodeLabelWord, List.length_ofFn]) + intro t _ ht; have htQ : t < Q := by simpa only [List.length_ofFn] using ht + rw [getElem_decodeLabelWord _ _ _ _ htQ, Cslib.Radix.digit_ofDigits hr (List.ofFn x) + (fun a ha => by obtain ⟨i, rfl⟩ := List.mem_ofFn.mp ha; exact hx i) t ht] + +/-- Exact bijection between binary indices `Fin (r ^ Q)` and length-`Q` words over `{0, …, r - 1}` +(including `Q = 0` and `r = 1`). -/ +def labelWordEquiv {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) : + Fin (r ^ Q) ≃ {w : List ℕ // w.length = Q ∧ ∀ x ∈ w, x < r} where + toFun j := ⟨decodeLabelWord r Q j.val, length_decodeLabelWord r Q j.val, + fun _ hx => mem_decodeLabelWord_lt hr hx⟩ + invFun w := ⟨Nat.ofDigits r w.1, + by simpa only [w.2.1] using Nat.ofDigits_lt_base_pow_length_of_pos hr w.1 w.2.2⟩ + left_inv j := Fin.ext (ofDigits_decodeLabelWord j.isLt) + right_inv w := Subtype.ext (by have h := decodeLabelWord_ofDigits hr w.2.2; rwa [w.2.1] at h) + +/-- Convert a concrete digit list `w : List ℕ` into a typed schedule `Fin Q → Fin r`, clamping +out-of-range digits to `0`. -/ +def wordToSchedule {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) (w : List ℕ) (t : Fin Q) : Fin r := + if h : w.getD t.val 0 < r then ⟨w.getD t.val 0, h⟩ else ⟨0, hr⟩ + +/-- Convert a typed schedule `a : Fin Q → Fin r` into its length-`Q` digit list. -/ +def scheduleToWord {r Q : ℕ} (a : Fin Q → Fin r) : List ℕ := List.ofFn fun t => (a t).val + +@[simp] theorem length_scheduleToWord {r Q : ℕ} (a : Fin Q → Fin r) : + (scheduleToWord a).length = Q := List.length_ofFn + +theorem mem_scheduleToWord_lt {r Q : ℕ} (a : Fin Q → Fin r) {x : ℕ} (hx : x ∈ scheduleToWord a) : + x < r := by obtain ⟨t, rfl⟩ := List.mem_ofFn.mp hx; exact (a t).isLt + +@[simp] theorem wordToSchedule_scheduleToWord {r : ℕ} (hr : 1 ≤ r) {Q : ℕ} + (a : Fin Q → Fin r) : wordToSchedule hr Q (scheduleToWord a) = a := by + funext t; simp only [wordToSchedule, scheduleToWord, List.getD_ofFn, (a t).isLt, ↓reduceDIte, + Fin.eta] + +theorem scheduleToWord_inj {r : ℕ} (hr : 1 ≤ r) {Q : ℕ} {a b : Fin Q → Fin r} + (h : scheduleToWord a = scheduleToWord b) : a = b := by + rw [← wordToSchedule_scheduleToWord hr a, ← wordToSchedule_scheduleToWord hr b, h] + +theorem scheduleToWord_wordToSchedule {r : ℕ} (hr : 1 ≤ r) {Q : ℕ} {w : List ℕ} + (hlen : w.length = Q) (hw : ∀ x ∈ w, x < r) : + scheduleToWord (wordToSchedule hr Q w) = w := by + apply List.ext_getElem (by simp only [length_scheduleToWord, hlen]) + intro t _ ht; have hlt : w[t] < r := hw w[t] (List.getElem_mem ht) + simp only [scheduleToWord, List.getElem_ofFn, wordToSchedule, List.getD_eq_getElem w 0 ht, hlt, + ↓reduceDIte] + +/-- `wordToSchedule` composed with `decodeLabelWord` agrees identically with the standard +bijection `finFunctionFinEquiv.symm : Fin (r ^ Q) ≃ (Fin Q → Fin r)`. -/ +theorem wordToSchedule_decodeLabelWord_eq_finFunctionFinEquiv_symm {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) + (j : Fin (r ^ Q)) : + wordToSchedule hr Q (decodeLabelWord r Q j.val) = finFunctionFinEquiv.symm j := by + funext t; apply Fin.ext + have hget : (decodeLabelWord r Q j.val).getD t.val 0 = j.val / r ^ t.val % r := by + rw [decodeLabelWord, List.getD_map_range _ 0 t.isLt, Cslib.Radix.digit_eq_div_pow_mod] + simp only [wordToSchedule, hget, Nat.mod_lt _ hr, ↓reduceDIte, finFunctionFinEquiv_symm_apply_val] + +/-- Exhaustive list of candidate schedules `Fin Q → Fin r` in `0 .. r ^ Q - 1` radix order. -/ +def candidateScheduleList {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) : List (Fin Q → Fin r) := + (List.range (r ^ Q)).map fun j => wordToSchedule hr Q (decodeLabelWord r Q j) + +theorem mem_candidateScheduleList {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) (a : Fin Q → Fin r) : + a ∈ candidateScheduleList hr Q := by + let j := finFunctionFinEquiv a; refine List.mem_map.mpr ⟨j.val, List.mem_range.mpr j.isLt, ?_⟩ + rw [wordToSchedule_decodeLabelWord_eq_finFunctionFinEquiv_symm hr Q j] + exact Equiv.symm_apply_apply _ _ + +/-- Encoded bit-length bound for any word of length `Q` with digits `< max r 1`. -/ +theorem length_encList_word_le {Q r : ℕ} {w : List ℕ} (hlen : w.length = Q) + (hw : ∀ x ∈ w, x < max r 1) : + (encList encNat w).length ≤ Q * (2 * (encNat r).length + 1) := by + rw [length_encList] + have hdom : (w.map fun a => 2 * (encNat a).length + 1).sum ≤ + (w.map fun _ => 2 * (encNat r).length + 1).sum := List.sum_le_sum fun x hx => by + have hlt := hw x hx + have hsz := ComputableTidilyInO.length_encNat_mono (by omega : x ≤ r); omega + simpa only [List.map_const', hlen, List.sum_replicate, smul_eq_mul] using hdom + +/-- `decodeLabelWord r Q j` is computable in polynomial time from binary `r`, unary `Q`, and +binary `j`. -/ +@[fun_prop] theorem computableInPolyTime_decodeLabelWord : + ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ => decodeLabelWord p.1.1 p.1.2 p.2) + (encPair (encPair encNat encUnary) encNat) (encList encNat) := by + refine .of_tidy ?_; simp only [decodeLabelWord, Cslib.Radix.digit_eq_div_pow_mod]; fun_prop + +@[fun_prop] theorem computableInPolyTime_decodeLabelWord' {α : Type} {input : α ↪ List Bool} + {r Q j : α → ℕ} (hr : ComputableInPolyTime r input encNat) + (hQ : ComputableInPolyTime Q input encUnary) (hj : ComputableInPolyTime j input encNat) : + ComputableInPolyTime (fun a => decodeLabelWord (r a) (Q a) (j a)) input (encList encNat) := + computableInPolyTime_decodeLabelWord.comp ((hr.prod hQ).prod hj) + +/-! ### Section 2: Cleared-integer collision scores and exact rational bridge -/ + +/-- 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 clearedPartialCollision {α : Type*} [DecidableEq α] (cardL : ℕ) + (assigned : List (Option α)) (i j : ℕ) : ℕ := + if i = j then cardL + else match assigned.getD i none, assigned.getD j none with + | some x, some y => if x = y then cardL else 0 + | _, _ => 1 + +/-- Sum of cleared incidence-pair collisions over `edges : List (ℕ × ℕ)` (`(f, v)` pairs), scaled +by `K ^ 2 = (r ^ Q) ^ 2`. -/ +def clearedIncidenceCollisions (K : ℕ) (edges : List (ℕ × ℕ)) + (varSched facSched : List (Option (List ℕ))) : ℕ := + (edges.map fun e => (edges.map fun e' => + clearedPartialCollision K varSched e.2 e'.2 * + clearedPartialCollision K facSched e.1 e'.1).sum).sum + +/-- Cleared-integer numerator of `partialIncidencePotential` over common denominator `K ^ 2`. -/ +def clearedIncidencePotential (K : ℕ) (edges : List (ℕ × ℕ)) + (varSched facSched : List (Option (List ℕ))) : ℕ := + clearedIncidenceCollisions K edges varSched facSched - edges.length ^ 2 + +/-- Sum of cleared variable-coordinate collisions across `t < Q` and `v, v' < n`, scaled by `r`. -/ +def clearedGroupCollisions (n Q r : ℕ) (varSched : List (Option (List ℕ))) : ℕ := + ((List.range Q).map fun t => + let ct := varSched.map (Option.map fun w => w.getD t 0) + ((List.range n).map fun v => + ((List.range n).map fun v' => clearedPartialCollision r ct v v').sum).sum).sum + +/-- Cleared-integer numerator of `partialGroupPotential` over common denominator `r`. -/ +def clearedGroupPotential (n Q r : ℕ) (varSched : List (Option (List ℕ))) : ℕ := + clearedGroupCollisions n Q r varSched - Q * n ^ 2 + +/-- Common positive integer denominator clearing `normalizedPartialScore` across all candidate +evaluations without rational GCD reductions ([OpenAI2026ETH], Lemma 4.5, p. 31). -/ +def scoreDenom (numEdges n Q r C : ℕ) : ℕ := + (r ^ Q) ^ 2 * max (numEdges * C) 1 * r * max (Q * n) 1 + +/-- Exact natural-number numerator of `normalizedPartialScore` over `scoreDenom`. -/ +def clearedJointScore (n Q r C : ℕ) (edges : List (ℕ × ℕ)) + (varSched facSched : List (Option (List ℕ))) : ℕ := + (if edges.length * C = 0 then 0 + else clearedIncidencePotential (r ^ Q) edges varSched facSched * (r * max (Q * n) 1)) + + (if Q * n = 0 then 0 + else clearedGroupPotential n Q r varSched * ((r ^ Q) ^ 2 * max (edges.length * C) 1)) + +theorem scoreDenom_pos (numEdges n Q : ℕ) {r : ℕ} (hr : 1 ≤ r) (C : ℕ) : + 0 < scoreDenom numEdges n Q r C := by + unfold scoreDenom; have : 0 < (r ^ Q) ^ 2 := Nat.pow_pos (Nat.pow_pos hr) + have : 0 < max (numEdges * C) 1 := Nat.lt_of_lt_of_le Nat.zero_lt_one (le_max_right _ _) + have : 0 < max (Q * n) 1 := Nat.lt_of_lt_of_le Nat.zero_lt_one (le_max_right _ _); positivity + +/-- Concrete incidence list `[(f₀, v₀), …]` extracted from `edge : Fin E → Fin m × Fin n`. -/ +def edgesOfFin {E m n : ℕ} (edge : Fin E → Fin m × Fin n) : List (ℕ × ℕ) := + List.ofFn fun e => ((edge e).1.val, (edge e).2.val) + +@[simp] theorem length_edgesOfFin {E m n : ℕ} (edge : Fin E → Fin m × Fin n) : + (edgesOfFin edge).length = E := List.length_ofFn + +/-- Concrete partial schedule list extracted from `Fin N → Option (Fin Q → Fin r)`. -/ +def partialScheduleListOfFin {N Q r : ℕ} + (assigned : Fin N → Option (Fin Q → Fin r)) : List (Option (List ℕ)) := + List.ofFn fun i => (assigned i).map scheduleToWord + +@[simp] theorem length_partialScheduleListOfFin {N Q r : ℕ} + (assigned : Fin N → Option (Fin Q → Fin r)) : + (partialScheduleListOfFin assigned).length = N := List.length_ofFn + +private theorem clearedPartialCollision_le {α : Type*} [DecidableEq α] (cardL : ℕ) + (assigned : List (Option α)) (i j : ℕ) : + clearedPartialCollision cardL assigned i j ≤ cardL + 1 := by + unfold clearedPartialCollision; split_ifs + · omega + · rcases assigned.getD i none with _ | x <;> rcases assigned.getD j none with _ | y <;> + dsimp only <;> (try split_ifs) <;> omega + +private theorem clearedIncidenceCollisions_le (K : ℕ) (edges : List (ℕ × ℕ)) + (varSched facSched : List (Option (List ℕ))) : + clearedIncidenceCollisions K edges varSched facSched ≤ edges.length ^ 2 * (K + 1) ^ 2 := by + unfold clearedIncidenceCollisions + refine (List.sum_le_length_nsmul _ (edges.length * (K + 1) ^ 2) + (List.forall_mem_map.mpr fun e _ => ?_)).trans + (by simp only [List.length_map, smul_eq_mul, sq, Nat.mul_assoc]; exact le_rfl) + refine (List.sum_le_length_nsmul _ ((K + 1) ^ 2) + (List.forall_mem_map.mpr fun e' _ => ?_)).trans + (by simp only [List.length_map, smul_eq_mul]; exact le_rfl) + simpa only [sq] using Nat.mul_le_mul (clearedPartialCollision_le K varSched e.2 e'.2) + (clearedPartialCollision_le K facSched e.1 e'.1) + +private theorem clearedGroupCollisions_le (n Q r : ℕ) (varSched : List (Option (List ℕ))) : + clearedGroupCollisions n Q r varSched ≤ Q * n ^ 2 * (r + 1) := by + unfold clearedGroupCollisions + refine (List.sum_le_length_nsmul _ (n ^ 2 * (r + 1)) + (List.forall_mem_map.mpr fun t _ => ?_)).trans + (by simp only [List.length_map, List.length_range, smul_eq_mul, Nat.mul_assoc]; exact le_rfl) + refine (List.sum_le_length_nsmul _ (n * (r + 1)) + (List.forall_mem_map.mpr fun v _ => ?_)).trans + (by simp only [List.length_map, List.length_range, smul_eq_mul, sq, Nat.mul_assoc]; exact + le_rfl) + exact (List.sum_le_length_nsmul _ (r + 1) (List.forall_mem_map.mpr fun v' _ => + clearedPartialCollision_le r _ v v')).trans + (by simp only [List.length_map, List.length_range, smul_eq_mul]; exact le_rfl) + +/-- Unconditional upper bound on `clearedJointScore`, independent of `(varSched, facSched)`. -/ +theorem 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)) := by + unfold clearedJointScore clearedIncidencePotential clearedGroupPotential + have hinc := (Nat.sub_le (clearedIncidenceCollisions (r ^ Q) edges varSched facSched) + (edges.length ^ 2)).trans (clearedIncidenceCollisions_le (r ^ Q) edges varSched facSched) + have hgrp := (Nat.sub_le (clearedGroupCollisions n Q r varSched) (Q * n ^ 2)).trans + (clearedGroupCollisions_le n Q r varSched) + have hm1 : max (Q * n) 1 ≤ Q * n + 1 := max_le (by omega) (by omega) + have hm2 : max (edges.length * C) 1 ≤ edges.length * C + 1 := max_le (by omega) (by omega) + refine Nat.add_le_add + (by split_ifs; exacts [Nat.zero_le _, Nat.mul_le_mul hinc (Nat.mul_le_mul_left r hm1)]) + (by split_ifs; exacts [Nat.zero_le _, Nat.mul_le_mul hgrp (Nat.mul_le_mul_left _ hm2)]) + +/-- 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 length_encNat_clearedJointScore_le (n Q r C : ℕ) (edges : List (ℕ × ℕ)) + (varSched facSched : List (Option (List ℕ))) : + (encNat (clearedJointScore n Q r C edges varSched facSched)).length ≤ + 2 * Q * (encNat r).length + 2 * (encNat r).length + (encNat C).length + + 2 * (encNat edges.length).length + 2 * (encNat n).length + 2 * (encNat Q).length + 18 := by + refine (ComputableTidilyInO.length_encNat_mono + (clearedJointScore_le n Q r C edges varSched facSched)).trans ?_ + simp only [encNat_apply, Nat.size_eq_bits_len] + have hs1 (a : ℕ) : (a + 1).size ≤ a.size + 2 := + (Nat.size_add_le a 1).trans (by rw [show (1 : ℕ).size = 1 by decide]) + have h2Q : 2 * Q * r.size = 2 * (Q * r.size) := Nat.mul_assoc 2 Q r.size + have := Nat.size_pow_le r Q; have := hs1 (r ^ Q) + have := Nat.size_pow_le (r ^ Q + 1) 2; have := Nat.size_pow_le (r ^ Q) 2 + have := Nat.size_pow_le edges.length 2; have := Nat.size_pow_le n 2 + have := Nat.size_mul_le Q n; have := hs1 (Q * n); have := Nat.size_mul_le r (Q * n + 1) + have := Nat.size_mul_le edges.length C; have := hs1 (edges.length * C); have := hs1 r + have := Nat.size_mul_le (edges.length ^ 2) ((r ^ Q + 1) ^ 2) + have := Nat.size_mul_le (edges.length ^ 2 * (r ^ Q + 1) ^ 2) (r * (Q * n + 1)) + have := Nat.size_mul_le Q (n ^ 2); have := Nat.size_mul_le (Q * n ^ 2) (r + 1) + have := Nat.size_mul_le ((r ^ Q) ^ 2) (edges.length * C + 1) + have := Nat.size_mul_le (Q * n ^ 2 * (r + 1)) ((r ^ Q) ^ 2 * (edges.length * C + 1)) + have := Nat.size_add_le_max (edges.length ^ 2 * (r ^ Q + 1) ^ 2 * (r * (Q * n + 1))) + (Q * n ^ 2 * (r + 1) * ((r ^ Q) ^ 2 * (edges.length * C + 1))) + omega + +/-- Exact rational collision identity on whole-word schedules (`L = Fin Q → Fin r`). -/ +theorem 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.val j.val : ℚ) = + ((r ^ Q : ℕ) : ℚ) * partialCollision assigned i j := by + have hcard : Fintype.card (Fin Q → Fin r) = r ^ Q := by + simp only [Fintype.card_fun, Fintype.card_fin] + have hK0 : ((r ^ Q : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (Nat.pow_pos hr).ne' + have hget (u : Fin N) : (partialScheduleListOfFin assigned).getD u.val none = + (assigned u).map scheduleToWord := List.getD_ofFn _ u none + by_cases hij : i = j + · subst j; simp only [clearedPartialCollision, ↓reduceIte, partialCollision, mul_one] + · have hij_val : i.val ≠ j.val := fun h => hij (Fin.ext h) + simp only [clearedPartialCollision, hij_val, ↓reduceIte, hget i, hget j, partialCollision, + hij, hcard] + rcases assigned i with _ | x + · simp only [Option.map_none, Nat.cast_one]; field_simp [hK0] + · rcases assigned j with _ | y + · simp only [Option.map_some, Option.map_none, Nat.cast_one]; field_simp [hK0] + · simp only [Option.map_some]; by_cases hxy : x = y + · subst y; simp only [↓reduceIte, mul_one] + · simp only [show scheduleToWord x ≠ scheduleToWord y from fun h => + hxy (scheduleToWord_inj hr h), hxy, ↓reduceIte, Nat.cast_zero, mul_zero] + +private theorem clearedCoordCollision_eq_mul {n Q r : ℕ} (hr : 1 ≤ r) + (varLabels : Fin n → Option (Fin Q → Fin r)) (t : Fin Q) (v v' : Fin n) : + (clearedPartialCollision r + ((partialScheduleListOfFin varLabels).map (Option.map fun w => w.getD t.val 0)) + v.val v'.val : ℚ) = (r : ℚ) * partialCoordinateCollision varLabels t v v' := by + let ct := (partialScheduleListOfFin varLabels).map (Option.map fun w => w.getD t.val 0) + have hct_get (u : Fin n) : ct.getD u.val none = (varLabels u).map fun word => (word t).val := by + rw [List.getD_eq_getElem _ _ + (by simp only [ct, List.length_map, length_partialScheduleListOfFin]; exact u.isLt)] + simp only [ct, List.getElem_map, partialScheduleListOfFin, List.getElem_ofFn, Option.map_map] + rcases varLabels u with _ | word + · rfl + · simp only [Option.map_some, Function.comp_apply, scheduleToWord, List.getD_ofFn] + have hr0 : (r : ℚ) ≠ 0 := by exact_mod_cast (by omega : r ≠ 0) + by_cases hvv : v = v' + · subst v' + simp only [clearedPartialCollision, ↓reduceIte, partialCoordinateCollision, partialCollision, + mul_one] + · simp only [clearedPartialCollision, show v.val ≠ v'.val from fun h => hvv (Fin.ext h), + ↓reduceIte, show ((partialScheduleListOfFin varLabels).map + (Option.map fun w => w.getD t.val 0)) = ct from rfl, hct_get v, hct_get v', + partialCoordinateCollision, partialCollision, hvv, Fintype.card_fin] + rcases varLabels v with _ | x + · simp only [Option.map_none, Nat.cast_one]; field_simp [hr0] + · rcases varLabels v' with _ | y + · simp only [Option.map_some, Option.map_none, Nat.cast_one]; field_simp [hr0] + · simp only [Option.map_some, Fin.ext_iff] + by_cases hxy : (x t).val = (y t).val <;> + simp only [hxy, ↓reduceIte, mul_one, Nat.cast_zero, mul_zero] + +private theorem clearedIncidencePotential_eq_mul {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)) : + (clearedIncidencePotential (r ^ Q) (edgesOfFin edge) + (partialScheduleListOfFin varLabels) (partialScheduleListOfFin factorLabels) : ℚ) = + (((r ^ Q : ℕ) : ℚ) ^ 2) * partialIncidencePotential edge varLabels factorLabels := by + let : Nonempty (Fin Q → Fin r) := ⟨fun _ => ⟨0, hr⟩⟩ + have hcol : (clearedIncidenceCollisions (r ^ Q) (edgesOfFin edge) + (partialScheduleListOfFin varLabels) (partialScheduleListOfFin factorLabels) : ℚ) = + (((r ^ Q : ℕ) : ℚ) ^ 2) * ∑ e : Fin E, ∑ e' : Fin E, + partialIncidenceCollision varLabels factorLabels + (edge e).2 (edge e').2 (edge e).1 (edge e').1 := by + simp only [clearedIncidenceCollisions, edgesOfFin, List.map_ofFn, Function.comp_def, + List.sum_ofFn, Nat.cast_sum, Nat.cast_mul, clearedPartialCollision_eq_mul_partialCollision hr, + partialIncidenceCollision, Finset.mul_sum] + exact Finset.sum_congr rfl fun e _ => Finset.sum_congr rfl fun e' _ => by ring + have hnonneg : 0 ≤ partialIncidencePotential edge varLabels factorLabels := by + rw [partialIncidencePotential_eq_expect] + exact Finset.expect_nonneg fun _ _ => Finset.expect_nonneg fun _ _ => potential_nonneg _ + have hcard : (Fintype.card ((Fin Q → Fin r) × (Fin Q → Fin r)) : ℚ) = ((r ^ Q : ℕ) : ℚ) ^ 2 := by + simp only [Fintype.card_prod, Fintype.card_fun, Fintype.card_fin, Nat.cast_mul, sq] + have hK2 : (0 : ℚ) < ((r ^ Q : ℕ) : ℚ) ^ 2 := by + have : (0 : ℚ) < ((r ^ Q : ℕ) : ℚ) := by exact_mod_cast Nat.pow_pos hr + positivity + have hpot_mul : (((r ^ Q : ℕ) : ℚ) ^ 2) * partialIncidencePotential edge varLabels factorLabels = + (clearedIncidenceCollisions (r ^ Q) (edgesOfFin edge) + (partialScheduleListOfFin varLabels) (partialScheduleListOfFin factorLabels) : ℚ) - + (E : ℚ) ^ 2 := by + rw [partialIncidencePotential, Fintype.card_fin, hcard, mul_sub, ← hcol]; field_simp [hK2.ne'] + have hge : E ^ 2 ≤ clearedIncidenceCollisions (r ^ Q) (edgesOfFin edge) + (partialScheduleListOfFin varLabels) (partialScheduleListOfFin factorLabels) := by + have : ((E ^ 2 : ℕ) : ℚ) ≤ (clearedIncidenceCollisions (r ^ Q) (edgesOfFin edge) + (partialScheduleListOfFin varLabels) (partialScheduleListOfFin factorLabels) : ℚ) := by + have := mul_nonneg hK2.le hnonneg; simp only [Nat.cast_pow]; linarith + exact_mod_cast this + rw [clearedIncidencePotential, length_edgesOfFin, Nat.cast_sub hge, Nat.cast_pow, hpot_mul] + +private theorem clearedGroupPotential_eq_mul {n Q r : ℕ} (hr : 1 ≤ r) + (varLabels : Fin n → Option (Fin Q → Fin r)) : + (clearedGroupPotential n Q r (partialScheduleListOfFin varLabels) : ℚ) = + (r : ℚ) * partialGroupPotential varLabels := by + let : Nonempty (Fin r) := ⟨⟨0, hr⟩⟩ + have hcol : (clearedGroupCollisions n Q r (partialScheduleListOfFin varLabels) : ℚ) = + (r : ℚ) * ∑ t : Fin Q, ∑ v : Fin n, ∑ v' : Fin n, + partialCoordinateCollision varLabels t v v' := by + unfold clearedGroupCollisions + simp only [List.sum_map_range, Nat.cast_sum, clearedCoordCollision_eq_mul hr, Finset.mul_sum] + have hnonneg : 0 ≤ partialGroupPotential varLabels := by + rw [partialGroupPotential_eq_expect] + exact Finset.expect_nonneg fun _ _ => Finset.sum_nonneg fun _ _ => potential_nonneg _ + have hr_pos : (0 : ℚ) < r := by exact_mod_cast hr + have hpot_mul : (r : ℚ) * partialGroupPotential varLabels = + (clearedGroupCollisions n Q r (partialScheduleListOfFin varLabels) : ℚ) - + (Q : ℚ) * (n : ℚ) ^ 2 := by + rw [partialGroupPotential, Fintype.card_fin, Fintype.card_fin, Fintype.card_fin, mul_sub, + ← hcol]; field_simp [hr_pos.ne'] + have hge : Q * n ^ 2 ≤ clearedGroupCollisions n Q r (partialScheduleListOfFin varLabels) := by + have : ((Q * n ^ 2 : ℕ) : ℚ) ≤ + (clearedGroupCollisions n Q r (partialScheduleListOfFin varLabels) : ℚ) := by + have := mul_nonneg hr_pos.le hnonneg; simp only [Nat.cast_mul, Nat.cast_pow]; linarith + exact_mod_cast this + rw [clearedGroupPotential, Nat.cast_sub hge, Nat.cast_mul, Nat.cast_pow, hpot_mul] + +/-- **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 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 : ℚ) := by + have hinc := clearedIncidencePotential_eq_mul hr edge varLabels factorLabels + have hgrp := clearedGroupPotential_eq_mul hr varLabels + have hK0 : ((r ^ Q : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (Nat.pow_pos hr).ne' + have hr0 : (r : ℚ) ≠ 0 := by exact_mod_cast (by omega : r ≠ 0) + have hm (k : ℕ) : ((max k 1 : ℕ) : ℚ) ≠ 0 := by + exact_mod_cast (Nat.lt_of_lt_of_le Nat.zero_lt_one (le_max_right k 1)).ne' + rw [normalizedPartialScore, clearedJointScore, length_edgesOfFin, Fintype.card_fin, + Fintype.card_fin, Fintype.card_fin, Nat.cast_add, add_div] + congr 1 + · by_cases hEC : E * C = 0 + · simp only [hEC, ↓reduceIte, (by exact_mod_cast hEC : (E : ℚ) * (C : ℚ) = 0), div_zero, + Nat.cast_zero, zero_div] + · have hEC_rat : (E : ℚ) * (C : ℚ) ≠ 0 := by exact_mod_cast hEC + simp only [hEC, ↓reduceIte, scoreDenom, max_eq_left (Nat.one_le_iff_ne_zero.mpr hEC), + Nat.cast_mul, Nat.cast_pow, hinc] + field_simp [hEC_rat, hK0, hr0, hm (Q * n)] + · by_cases hQn : Q * n = 0 + · simp only [hQn, ↓reduceIte, (by exact_mod_cast hQn : (Q : ℚ) * (n : ℚ) = 0), div_zero, + Nat.cast_zero, zero_div] + · have hQn_rat : (Q : ℚ) * (n : ℚ) ≠ 0 := by exact_mod_cast hQn + simp only [hQn, ↓reduceIte, scoreDenom, max_eq_left (Nat.one_le_iff_ne_zero.mpr hQn), + Nat.cast_mul, Nat.cast_pow, hgrp] + field_simp [hQn_rat, hK0, hr0, hm (E * C)] + +/-- Strict `<` on `clearedJointScore : ℕ` is equivalent to `<` on `normalizedPartialScore : ℚ`. -/ +theorem 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 := by + have hD : (0 : ℚ) < scoreDenom E n Q r C := by exact_mod_cast scoreDenom_pos E n Q hr C + rw [normalizedPartialScore_eq_clearedJointScore_div hr edge v₁ f₁ C, + normalizedPartialScore_eq_clearedJointScore_div hr edge v₂ f₂ C, + div_lt_div_iff_of_pos_right hD, Nat.cast_lt] + +/-- Non-strict `≤` on `clearedJointScore : ℕ` is equivalent to `≤` on +`normalizedPartialScore : ℚ`. -/ +theorem 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 := by + have hD : (0 : ℚ) < scoreDenom E n Q r C := by exact_mod_cast scoreDenom_pos E n Q hr C + rw [normalizedPartialScore_eq_clearedJointScore_div hr edge v₁ f₁ C, + normalizedPartialScore_eq_clearedJointScore_div hr edge v₂ f₂ C, + div_le_div_iff_of_pos_right hD, Nat.cast_le] + +/-! ### Polynomial-time certificate for `clearedJointScore` -/ + +private theorem tidy_clearedPartialCollision {α γ : Type} [DecidableEq α] + {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} + {cardL i j : γ → ℕ} {assigned : γ → List (Option α)} + (hc : ComputableTidilyInPolyTime cardL encIn encNat) + (ha : ComputableTidilyInPolyTime assigned encIn (encList (encOption encA))) + (hi : ComputableTidilyInPolyTime i encIn encNat) + (hj : ComputableTidilyInPolyTime j encIn encNat) : + ComputableTidilyInPolyTime + (fun g => clearedPartialCollision (cardL g) (assigned g) (i g) (j g)) encIn encNat := by + have hgi := ComputableTidilyInPolyTime.listGetD_binary (encA := encOption encA) none ha hi + have hgj := ComputableTidilyInPolyTime.listGetD_binary (encA := encOption encA) none ha hj + have hboth : ComputableTidilyInPolyTime + (fun g => ((assigned g).getD (i g) none).isSome && ((assigned g).getD (j g) none).isSome) + encIn encBool := by fun_prop + have hinner := ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.decide_eq' hgi hgj) hc (ComputableTidilyInPolyTime.const 0) + have hmatch := hboth.cond hinner (ComputableTidilyInPolyTime.const 1) + refine (ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.decide_eq' hi hj) hc hmatch).of_enc_eq fun g => congrArg encNat ?_ + dsimp only [clearedPartialCollision]; by_cases hij : i g = j g + · simp only [hij, ↓reduceIte] + · simp only [hij, ↓reduceIte] + rcases (assigned g).getD (i g) none with _ | x <;> + rcases (assigned g).getD (j g) none with _ | y <;> + first | rfl | simp only [Option.isSome_some, Bool.and_self, ↓reduceIte, Option.some.injEq] + +private theorem tidy_binary_max1 {γ : Type} {encIn : γ ↪ List Bool} {x : γ → ℕ} + (hx : ComputableTidilyInPolyTime x encIn encNat) : + ComputableTidilyInPolyTime (fun g => max (x g) 1) encIn encNat := by + convert (show ComputableTidilyInPolyTime (fun g => if x g = 0 then 1 else x g) encIn encNat by + fun_prop) using 1 + funext g; rcases Nat.eq_zero_or_pos (x g) with h0 | hpos + · simp only [h0, ↓reduceIte]; omega + · simp only [hpos.ne', ↓reduceIte]; omega + +/-- Encoding of a pair `(varSched, facSched)` of partial schedule tables. -/ +def encPartialSchedules : (List (Option (List ℕ)) × List (Option (List ℕ))) ↪ List Bool := + encPair (encList (encOption (encList encNat))) (encList (encOption (encList encNat))) + +/-- Encoding of score parameters `((n, Q), (r, C), edges)`. -/ +def encScoreParams : ((ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ)) ↪ List Bool := + encPair (encPair encUnary encUnary) + (encPair (encPair encNat encNat) (encList (encPair encNat encNat))) + +/-- `clearedJointScore` is computable in polynomial time in its encoded inputs. -/ +@[fun_prop] theorem computableInPolyTime_clearedJointScore : + 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) + (encPair encScoreParams encPartialSchedules) encNat := by + refine .of_tidy ?_; unfold encScoreParams encPartialSchedules + let ePar := encPair (encPair encUnary encUnary) + (encPair (encPair encNat encNat) (encList (encPair encNat encNat))) + let eIn := encPair ePar + (encPair (encList (encOption (encList encNat))) (encList (encOption (encList encNat)))) + have hK : ComputableTidilyInPolyTime (fun p : _ × _ => p.1.2.1.1 ^ p.1.1.2) eIn encNat := by + fun_prop + have hincCol : ComputableTidilyInPolyTime (fun p : _ × _ => + clearedIncidenceCollisions (p.1.2.1.1 ^ p.1.1.2) p.1.2.2 p.2.1 p.2.2) eIn encNat := by + unfold clearedIncidenceCollisions + refine ComputableTidilyInPolyTime.binary_sum.comp (ComputableTidilyInPolyTime.mapWithInput + (by fun_prop) (ComputableTidilyInPolyTime.binary_sum.comp + (ComputableTidilyInPolyTime.mapWithInput (by fun_prop) ?_))) + exact ComputableTidilyInPolyTime.binary_mul' + (tidy_clearedPartialCollision (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop)) + (tidy_clearedPartialCollision (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop)) + have hgrpCol : ComputableTidilyInPolyTime (fun p : _ × _ => + clearedGroupCollisions p.1.1.1 p.1.1.2 p.1.2.1.1 p.2.1) eIn encNat := by + unfold clearedGroupCollisions + refine ComputableTidilyInPolyTime.binary_sum.comp + (ComputableTidilyInPolyTime.mapWithInput (by fun_prop) ?_) + have hct : ComputableTidilyInPolyTime (fun q : _ × ℕ => + q.1.2.1.map (Option.map fun w => w.getD q.2 0)) + (encPair eIn encUnary) (encList (encOption encNat)) := by + refine (show ComputableTidilyInPolyTime + (fun q : _ × ℕ => q.1.2.1.map fun o => o.elim none fun w => some (w.getD q.2 0)) + (encPair eIn encUnary) (encList (encOption encNat)) by fun_prop).of_enc_eq fun q => ?_ + congr 1; apply List.map_congr_left; intro o _; cases o <;> rfl + refine ComputableTidilyInPolyTime.binary_sum.comp (ComputableTidilyInPolyTime.mapWithInput + (by fun_prop) (ComputableTidilyInPolyTime.binary_sum.comp + (ComputableTidilyInPolyTime.mapWithInput (by fun_prop) ?_))) + exact tidy_clearedPartialCollision (by fun_prop) (hct.comp (by fun_prop)) + (ComputableTidilyInPolyTime.unary_to_binary.comp (by fun_prop)) + (ComputableTidilyInPolyTime.unary_to_binary.comp (by fun_prop)) + have heLen := ComputableTidilyInPolyTime.unary_to_binary.comp + (show ComputableTidilyInPolyTime (fun p : _ × _ => p.1.2.2.length) eIn encUnary by fun_prop) + have hnBin := ComputableTidilyInPolyTime.unary_to_binary.comp + (show ComputableTidilyInPolyTime (fun p : _ × _ => p.1.1.1) eIn encUnary by fun_prop) + have hQBin := ComputableTidilyInPolyTime.unary_to_binary.comp + (show ComputableTidilyInPolyTime (fun p : _ × _ => p.1.1.2) eIn encUnary by fun_prop) + have hC : ComputableTidilyInPolyTime (fun p : _ × _ => p.1.2.1.2) eIn encNat := by fun_prop + have hrBin : ComputableTidilyInPolyTime (fun p : _ × _ => p.1.2.1.1) eIn encNat := by fun_prop + have hK2 := ComputableTidilyInPolyTime.binary_pow' hK (ComputableTidilyInPolyTime.const 2) + have he2 := ComputableTidilyInPolyTime.binary_pow' heLen (ComputableTidilyInPolyTime.const 2) + have hn2 := ComputableTidilyInPolyTime.binary_pow' hnBin (ComputableTidilyInPolyTime.const 2) + have hqn := ComputableTidilyInPolyTime.binary_mul' hQBin hnBin + have hec := ComputableTidilyInPolyTime.binary_mul' heLen hC + have hincPot := ComputableTidilyInPolyTime.binary_sub' hincCol he2 + have hgrpPot := ComputableTidilyInPolyTime.binary_sub' hgrpCol + (ComputableTidilyInPolyTime.binary_mul' hQBin hn2) + unfold clearedJointScore clearedIncidencePotential clearedGroupPotential + exact ComputableTidilyInPolyTime.binary_add' + (ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.decide_eq' hec (ComputableTidilyInPolyTime.const 0)) + (ComputableTidilyInPolyTime.const 0) (ComputableTidilyInPolyTime.binary_mul' hincPot + (ComputableTidilyInPolyTime.binary_mul' hrBin (tidy_binary_max1 hqn)))) + (ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.decide_eq' hqn (ComputableTidilyInPolyTime.const 0)) + (ComputableTidilyInPolyTime.const 0) (ComputableTidilyInPolyTime.binary_mul' hgrpPot + (ComputableTidilyInPolyTime.binary_mul' hK2 (tidy_binary_max1 hec)))) + +/-! ### Section 3: Streaming `IndexFold` slot selector and rational minimizer bridges -/ + +/-- Update a variable (`(false, v)`) or factor (`(true, f)`) slot in `(varSched, facSched)`. -/ +def updateSlotSchedules (slot : Bool × ℕ) (val : Option (List ℕ)) + (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) : + List (Option (List ℕ)) × List (Option (List ℕ)) := + if slot.1 then (scheds.1, scheds.2.set slot.2 val) else (scheds.1.set slot.2 val, scheds.2) + +/-- Read a variable (`(false, v)`) or factor (`(true, f)`) slot from `(varSched, facSched)`. -/ +def readSlotSchedule (slot : Bool × ℕ) + (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) : Option (List ℕ) := + if slot.1 then scheds.2.getD slot.2 none else scheds.1.getD slot.2 none + +/-- Live accumulator for inner `IndexFold.run` candidate streaming over `j ∈ 0 .. r ^ Q - 1`. -/ +abbrev SlotSelectAcc : Type := + ((ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ)) × + ((Bool × ℕ) × ((List (Option (List ℕ)) × List (Option (List ℕ))) × Option (List ℕ × ℕ))) + +/-- Inner `IndexFold.run` callback evaluating candidate `decodeLabelWord r Q j` under +`clearedJointScore` and retaining the first strict minimizer (`candScore < best.2`). -/ +def selectSlotStep (state : ℕ × SlotSelectAcc) : SlotSelectAcc := + let sparams := state.2.1; let slot := state.2.2.1; let scheds := state.2.2.2.1 + let candWord := decodeLabelWord sparams.2.1.1 sparams.1.2 state.1 + let candScheds := updateSlotSchedules slot (some candWord) scheds + let candScore := clearedJointScore sparams.1.1 sparams.1.2 sparams.2.1.1 sparams.2.1.2 + sparams.2.2 candScheds.1 candScheds.2 + let nextBest := state.2.2.2.2.elim (some (candWord, candScore)) fun best => + if decide (candScore < best.2) then some (candWord, candScore) else some best + (sparams, (slot, (scheds, nextBest))) + +/-- 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` +([OpenAI2026ETH], Lemma 4.5, p. 31). -/ +def streamBestSlotLabel (n Q r C : ℕ) (edges : List (ℕ × ℕ)) + (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) : List ℕ := + let init : SlotSelectAcc := (((n, Q), (r, C), edges), (slot, (scheds, none))) + ((IndexFold.run selectSlotStep (r ^ Q) init).2.2.2.2).elim (List.replicate Q 0) Prod.fst + +private theorem run_selectSlotStep_params (sparams : (ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ)) + (slot : Bool × ℕ) (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (k : ℕ) : + let r := IndexFold.run selectSlotStep k (sparams, (slot, (scheds, none))) + r.2.1 = sparams ∧ r.2.2.1 = slot ∧ r.2.2.2.1 = scheds := by + induction k with + | zero => exact ⟨rfl, rfl, rfl⟩ + | succ k ih => + rw [IndexFold.run_succ]; simp only [IndexFold.step, selectSlotStep, ih.1, ih.2.1, ih.2.2, + and_self] + +/-- Cleared-integer score of candidate `decodeLabelWord r Q j` placed in `slot`. -/ +def candidateSlotScore (n Q r C : ℕ) (edges : List (ℕ × ℕ)) + (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) (j : ℕ) : ℕ := + let candScheds := updateSlotSchedules slot (some (decodeLabelWord r Q j)) scheds + clearedJointScore n Q r C edges candScheds.1 candScheds.2 + +private theorem run_selectSlotStep_spec (n Q r C : ℕ) (edges : List (ℕ × ℕ)) + (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) : + ∀ {k : ℕ}, 0 < k → + ∃ jStar < k, + (IndexFold.run selectSlotStep k + (((n, Q), (r, C), edges), (slot, (scheds, none)))).2.2.2.2 = + some (decodeLabelWord r Q jStar, candidateSlotScore n Q r C edges scheds slot jStar) ∧ + (∀ j < k, 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) ∧ + (∀ {α : Type} (g : ℕ → α) (f : α → ℚ), + (∀ i < k, ∀ j < k, + candidateSlotScore n Q r C edges scheds slot i < + candidateSlotScore n Q r C edges scheds slot j ↔ f (g i) < f (g j)) → + ((List.range k).map g).argmin f = some (g jStar)) := by + intro k hk; let init : SlotSelectAcc := (((n, Q), (r, C), edges), (slot, (scheds, none))) + induction k with + | zero => omega + | succ k ih => + rcases Nat.eq_zero_or_pos k with rfl | hkpos + · refine ⟨0, Nat.zero_lt_one, by rw [IndexFold.run_succ, IndexFold.run_zero]; rfl, + fun j hj => by rw [show j = 0 by omega], fun _ hj => by omega, fun _ _ _ => rfl⟩ + · obtain ⟨jStar, hjStar_lt, hopt, hle, hlt, harg⟩ := ih hkpos + have hp := run_selectSlotStep_params ((n, Q), (r, C), edges) slot scheds k + have hidx := IndexFold.run_index selectSlotStep k init + let scK := candidateSlotScore n Q r C edges scheds slot k + let scBest := candidateSlotScore n Q r C edges scheds slot jStar + by_cases hcmp : scK < scBest + · refine ⟨k, Nat.lt_succ_self k, ?_, ?_, fun j hj => lt_of_lt_of_le hcmp (hle j hj), ?_⟩ + · rw [IndexFold.run_succ] + simp only [IndexFold.step, selectSlotStep, init, hidx, hp.1, hp.2.1, hp.2.2, hopt, + Option.elim_some] + split_ifs with h + · rfl + · exact absurd (decide_eq_true hcmp) h + · intro j hj; rcases Nat.lt_succ_iff_lt_or_eq.mp hj with hj' | rfl + · exact hcmp.le.trans (hle j hj') + · exact le_rfl + · intro α g f hiff + rw [List.range_succ, List.map_append, List.map_singleton, List.argmin_concat, + harg g f (fun i hi j hj => hiff i (Nat.lt_succ_of_lt hi) j (Nat.lt_succ_of_lt hj))] + have hf_lt := (hiff k (Nat.lt_succ_self k) jStar (Nat.lt_succ_of_lt hjStar_lt)).mp hcmp + simp only [hf_lt, ↓reduceIte] + · refine ⟨jStar, Nat.lt_succ_of_lt hjStar_lt, ?_, ?_, hlt, ?_⟩ + · rw [IndexFold.run_succ] + simp only [IndexFold.step, selectSlotStep, init, hidx, hp.1, hp.2.1, hp.2.2, hopt, + Option.elim_some] + split_ifs with h + · exact absurd (of_decide_eq_true h) hcmp + · rfl + · intro j hj; rcases Nat.lt_succ_iff_lt_or_eq.mp hj with hj' | rfl + · exact hle j hj' + · exact Nat.le_of_not_lt hcmp + · intro α g f hiff + rw [List.range_succ, List.map_append, List.map_singleton, List.argmin_concat, + harg g f (fun i hi j hj => hiff i (Nat.lt_succ_of_lt hi) j (Nat.lt_succ_of_lt hj))] + have hf_nlt : ¬ f (g k) < f (g jStar) := fun h => + hcmp ((hiff k (Nat.lt_succ_self k) jStar (Nat.lt_succ_of_lt hjStar_lt)).mpr h) + simp only [hf_nlt, ↓reduceIte] + +/-- First-minimizer characterization of `streamBestSlotLabel` when `0 < r ^ Q`. -/ +theorem 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) := by + obtain ⟨jStar, hj, hopt, hle, hlt, _⟩ := run_selectSlotStep_spec n Q r C edges scheds slot hpos + exact ⟨jStar, hj, by simp only [streamBestSlotLabel, hopt, Option.elim_some], hle, hlt⟩ + +@[simp] theorem 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 := by + rcases Nat.eq_zero_or_pos (r ^ Q) with h0 | hpos + · simp only [streamBestSlotLabel, h0, IndexFold.run_zero, Option.elim_none, List.length_replicate] + · obtain ⟨_, _, hw, _, _⟩ := exists_min_index_streamBestSlotLabel n Q r C edges scheds slot hpos + rw [hw, length_decodeLabelWord] + +theorem 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 := by + rcases Nat.eq_zero_or_pos (r ^ Q) with h0 | hpos + · simp only [streamBestSlotLabel, h0, IndexFold.run_zero, Option.elim_none, + List.mem_replicate] at hx + rcases hx with ⟨_, rfl⟩; omega + · obtain ⟨_, hj, hw, _, _⟩ := exists_min_index_streamBestSlotLabel n Q r C edges scheds slot hpos + rw [hw] at hx; exact mem_decodeLabelWord_lt_max hj hx + +theorem 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 := by + simpa only [max_eq_left hr] using mem_streamBestSlotLabel_lt_max n Q r C edges scheds slot hx + +/-- Updating `partialScheduleListOfFin` at index `k.val` with a valid length-`Q` word `w` commutes +with `Function.update` via `wordToSchedule`. -/ +theorem 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.val (some w) = + partialScheduleListOfFin (Function.update assigned k (some (wordToSchedule hr Q w))) := by + apply List.ext_getElem (by simp only [List.length_set, length_partialScheduleListOfFin]) + intro i hi _ + have hiN : i < N := by simpa only [List.length_set, length_partialScheduleListOfFin] using hi + rw [List.getElem_set]; simp only [partialScheduleListOfFin, List.getElem_ofFn] + by_cases hki : k.val = i + · have hfin : (⟨i, hiN⟩ : Fin N) = k := Fin.ext hki.symm + simp only [hki, ↓reduceIte, hfin, Function.update_self, Option.map_some, + scheduleToWord_wordToSchedule hr hlen hw] + · have hfin : (⟨i, hiN⟩ : Fin N) ≠ k := fun h => hki (congrArg Fin.val h).symm + simp only [hki, ↓reduceIte, Function.update_of_ne hfin] + +/-- Exact agreement between `streamBestSlotLabel` at variable slot `(false, v.val)` and +`bestVariableLabel` over `candidateScheduleList hr Q`. -/ +theorem 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.val))) = + bestVariableLabel edge varLabels factorLabels C v (candidateScheduleList hr Q) := by + obtain ⟨jStar, _, hopt, _, _, harg⟩ := run_selectSlotStep_spec n Q r C (edgesOfFin edge) + (partialScheduleListOfFin varLabels, partialScheduleListOfFin factorLabels) + (false, v.val) (Nat.pow_pos (n := Q) hr) + simp only [streamBestSlotLabel, hopt, Option.elim_some, bestVariableLabel, candidateScheduleList] + refine (harg (fun j => wordToSchedule hr Q (decodeLabelWord r Q j)) + (fun word => normalizedPartialScore edge (Function.update varLabels v (some word)) + factorLabels C) fun i _ j _ => ?_).symm + have hset (k : ℕ) := set_partialScheduleListOfFin (hr := hr) varLabels v (decodeLabelWord r Q k) + (length_decodeLabelWord r Q k) (fun _ hx => mem_decodeLabelWord_lt hr hx) + simp only [candidateSlotScore, updateSlotSchedules, Bool.false_eq_true, ↓reduceIte, hset i, + hset j] + exact clearedJointScore_lt_iff_normalizedPartialScore_lt hr edge _ _ _ _ C + +/-- Exact agreement between `streamBestSlotLabel` at factor slot `(true, f.val)` and +`bestFactorLabel` over `candidateScheduleList hr Q`. -/ +theorem 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.val))) = + bestFactorLabel edge varLabels factorLabels C f (candidateScheduleList hr Q) := by + obtain ⟨jStar, _, hopt, _, _, harg⟩ := run_selectSlotStep_spec n Q r C (edgesOfFin edge) + (partialScheduleListOfFin varLabels, partialScheduleListOfFin factorLabels) + (true, f.val) (Nat.pow_pos (n := Q) hr) + simp only [streamBestSlotLabel, hopt, Option.elim_some, bestFactorLabel, candidateScheduleList] + refine (harg (fun j => wordToSchedule hr Q (decodeLabelWord r Q j)) + (fun word => normalizedPartialScore edge varLabels + (Function.update factorLabels f (some word)) C) fun i _ j _ => ?_).symm + have hset (k : ℕ) := set_partialScheduleListOfFin (hr := hr) factorLabels f + (decodeLabelWord r Q k) (length_decodeLabelWord r Q k) + (fun _ hx => mem_decodeLabelWord_lt hr hx) + simp only [candidateSlotScore, updateSlotSchedules, ↓reduceIte, hset i, hset j] + exact clearedJointScore_lt_iff_normalizedPartialScore_lt hr edge _ _ _ _ C + +/-! ### Section 4: All-prefix bit-length bounds, `NativeCertificate`, and `ComputableInPolySpace` -/ + +/-- Encoding of inner `IndexFold` accumulator `SlotSelectAcc`. -/ +def encSlotSelectAcc : SlotSelectAcc ↪ List Bool := + encPair encScoreParams + (encPair (encPair encBool encUnary) + (encPair encPartialSchedules (encOption (encPair (encList encNat) encNat)))) + +/-- Runtime input tuple for `streamBestSlotLabel`. -/ +abbrev StreamSlotIn : Type := + ((ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ)) × + ((Bool × ℕ) × (List (Option (List ℕ)) × List (Option (List ℕ)))) + +/-- Encoding of runtime inputs to `streamBestSlotLabel`. -/ +def encStreamSlotIn : StreamSlotIn ↪ List Bool := + encPair encScoreParams (encPair (encPair encBool encUnary) encPartialSchedules) + +end Cslib.BalancedSchedules +end + +public section +namespace Cslib.BalancedSchedules +open Finset Cslib.GenericRAM Turing.MultiTapeTM + +/-- 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 length_encSlotSelectState_run_le (n Q r C : ℕ) (edges : List (ℕ × ℕ)) + (scheds : List (Option (List ℕ)) × List (Option (List ℕ))) (slot : Bool × ℕ) + {j : ℕ} (hj : j ≤ r ^ Q) : + (encPair encNat encSlotSelectAcc + (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 * (encNat r).length + 4 * Q + 2 * (encNat r).length + (encNat C).length + + 2 * (encNat edges.length).length + 2 * (encNat n).length + 2 * (encNat Q).length + 28 := by + let init : SlotSelectAcc := (((n, Q), (r, C), edges), (slot, (scheds, none))) + have hp := run_selectSlotStep_params ((n, Q), (r, C), edges) slot scheds j + have hj_len : (encNat j).length ≤ Q * (encNat r).length + 1 := + (ComputableTidilyInO.length_encNat_mono hj).trans (length_encNat_pow_le r Q) + have hbest : (encOption (encPair (encList encNat) encNat) + (IndexFold.run selectSlotStep j init).2.2.2.2).length ≤ + 6 * Q * (encNat r).length + 4 * Q + 2 * (encNat r).length + (encNat C).length + + 2 * (encNat edges.length).length + 2 * (encNat n).length + 2 * (encNat Q).length + 20 := by + rcases Nat.eq_zero_or_pos j with rfl | hjpos + · simp only [IndexFold.run_zero, init, encOption_none, List.length_nil]; omega + · obtain ⟨jStar, hjStar_lt, hopt, _, _, _⟩ := + run_selectSlotStep_spec n Q r C edges scheds slot hjpos + rw [hopt, encOption_some, List.length_cons, length_encPair] + dsimp only [candidateSlotScore] + have hw := length_encList_word_le (length_decodeLabelWord r Q jStar) + (fun _ hx => mem_decodeLabelWord_lt_max (lt_of_lt_of_le hjStar_lt hj) hx) + have hsc := length_encNat_clearedJointScore_le n Q r C edges + (updateSlotSchedules slot (some (decodeLabelWord r Q jStar)) scheds).1 + (updateSlotSchedules slot (some (decodeLabelWord r Q jStar)) scheds).2 + linarith + rw [IndexFold.length_run] + rcases hst : (IndexFold.run selectSlotStep j init).2 with ⟨sp, sl, sc, bo⟩ + have hsp : sp = ((n, Q), (r, C), edges) := by simpa only [init, hst] using hp.1 + have hsl : sl = slot := by simpa only [init, hst] using hp.2.1 + have hsc_eq : sc = scheds := by simpa only [init, hst] using hp.2.2 + have hbo : bo = (IndexFold.run selectSlotStep j init).2.2.2.2 := by simp only [hst] + subst hsp hsl hsc_eq; rw [← hbo] at hbest + simp only [encSlotSelectAcc, encStreamSlotIn, length_encPair]; linarith + +private theorem list_set_eq_range_map {α : Type*} (d : α) (l : List α) (i : ℕ) (val : α) : + l.set i val = + (List.range l.length).map fun k => if decide (i = k) then val else l.getD k d := by + apply List.ext_getElem (by simp only [List.length_set, List.length_map, List.length_range]) + intro k hk _; have hkl : k < l.length := by simpa only [List.length_set] using hk + rw [List.getElem_set, List.getElem_map, List.getElem_range, List.getD_eq_getElem l d hkl] + by_cases hik : i = k <;> + simp only [hik, decide_true, decide_false, Bool.false_eq_true, ↓reduceIte] + +/-- `updateSlotSchedules` is computable in polynomial time. -/ +@[fun_prop] theorem computableInPolyTime_updateSlotSchedules : + ComputableInPolyTime (fun p : ((Bool × ℕ) × Option (List ℕ)) × + (List (Option (List ℕ)) × List (Option (List ℕ))) => updateSlotSchedules p.1.1 p.1.2 p.2) + (encPair (encPair (encPair encBool encUnary) (encOption (encList encNat))) + encPartialSchedules) encPartialSchedules := by + refine .of_tidy ?_; unfold encPartialSchedules; let eOpt := encOption (encList encNat) + let eIn := encPair (encPair (encPair encBool encUnary) eOpt) + (encPair (encList eOpt) (encList eOpt)) + have hset1 : ComputableTidilyInPolyTime (fun p : (_ × _) × (_ × _) => + (List.range p.2.1.length).map fun k => + if decide (p.1.1.2 = k) then p.1.2 else p.2.1.getD k none) + eIn (encList eOpt) := ComputableTidilyInPolyTime.mapWithInput (by fun_prop) + (ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.decide_eq' (by fun_prop) (by fun_prop)) + (by fun_prop) (by fun_prop)) + have hset2 : ComputableTidilyInPolyTime (fun p : (_ × _) × (_ × _) => + (List.range p.2.2.length).map fun k => + if decide (p.1.1.2 = k) then p.1.2 else p.2.2.getD k none) + eIn (encList eOpt) := ComputableTidilyInPolyTime.mapWithInput (by fun_prop) + (ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.decide_eq' (by fun_prop) (by fun_prop)) + (by fun_prop) (by fun_prop)) + refine (ComputableTidilyInPolyTime.cond (show ComputableTidilyInPolyTime + (fun p : _ => p.1.1.1) eIn encBool by fun_prop) + ((show ComputableTidilyInPolyTime (fun p : _ => p.2.1) eIn (encList eOpt) by + fun_prop).prod hset2) + (hset1.prod (show ComputableTidilyInPolyTime (fun p : _ => p.2.2) eIn (encList eOpt) by + fun_prop))).of_enc_eq fun p => ?_ + dsimp only [updateSlotSchedules] + rw [list_set_eq_range_map none p.2.1 p.1.1.2 p.1.2, + list_set_eq_range_map none p.2.2 p.1.1.2 p.1.2] + +/-- `readSlotSchedule` is computable in polynomial time. -/ +@[fun_prop] theorem computableInPolyTime_readSlotSchedule : + ComputableInPolyTime (fun p : (Bool × ℕ) × (List (Option (List ℕ)) × List (Option (List ℕ))) => + readSlotSchedule p.1 p.2) + (encPair (encPair encBool encUnary) encPartialSchedules) (encOption (encList encNat)) := by + refine .of_tidy ?_; unfold readSlotSchedule encPartialSchedules; fun_prop + +private theorem computableInPolyTime_selectSlotStep : + ComputableInPolyTime selectSlotStep (encPair encNat encSlotSelectAcc) encSlotSelectAcc := by + let eIn := encPair encNat encSlotSelectAcc + have hw : ComputableInPolyTime (fun s : ℕ × SlotSelectAcc => + decodeLabelWord s.2.1.2.1.1 s.2.1.1.2 s.1) eIn (encList encNat) := + computableInPolyTime_decodeLabelWord' + (.of_tidy (by unfold eIn encSlotSelectAcc encScoreParams; fun_prop)) + (.of_tidy (by unfold eIn encSlotSelectAcc encScoreParams; fun_prop)) + (.of_tidy (by unfold eIn; fun_prop)) + have hupd_in : ComputableInPolyTime (fun s : ℕ × SlotSelectAcc => + ((s.2.2.1, some (decodeLabelWord s.2.1.2.1.1 s.2.1.1.2 s.1)), s.2.2.2.1)) + eIn (encPair (encPair (encPair encBool encUnary) (encOption (encList encNat))) + encPartialSchedules) := by + refine .of_tidy ?_; have hwT := hw.tidy; unfold eIn encSlotSelectAcc; fun_prop + have hcs := computableInPolyTime_updateSlotSchedules.comp hupd_in + have hsc_in : ComputableInPolyTime (fun s : ℕ × SlotSelectAcc => + (s.2.1, updateSlotSchedules s.2.2.1 + (some (decodeLabelWord s.2.1.2.1.1 s.2.1.1.2 s.1)) s.2.2.2.1)) + eIn (encPair encScoreParams encPartialSchedules) := + (ComputableInPolyTime.of_tidy (by unfold eIn encSlotSelectAcc; fun_prop)).prod hcs + have hsc := computableInPolyTime_clearedJointScore.comp hsc_in + refine .of_tidy ?_; have hwT := hw.tidy; have hscT := hsc.tidy + let eBest := encPair (encList encNat) encNat + let candW (s : ℕ × SlotSelectAcc) := decodeLabelWord s.2.1.2.1.1 s.2.1.1.2 s.1 + let candSc (s : ℕ × SlotSelectAcc) := + clearedJointScore s.2.1.1.1 s.2.1.1.2 s.2.1.2.1.1 s.2.1.2.1.2 s.2.1.2.2 + (updateSlotSchedules s.2.2.1 (some (candW s)) s.2.2.2.1).1 + (updateSlotSchedules s.2.2.1 (some (candW s)) s.2.2.2.1).2 + have hsomeCand : ComputableTidilyInPolyTime (fun s => some (candW s, candSc s)) + eIn (encOption eBest) := (ComputableTidilyInPolyTime.optionSome eBest).comp (hwT.prod hscT) + have hbest : ComputableTidilyInPolyTime + (fun s : ℕ × SlotSelectAcc => s.2.2.2.2.elim (some (candW s, candSc s)) fun best => + if decide (candSc s < best.2) then some (candW s, candSc s) else some best) + eIn (encOption eBest) := by + refine ComputableTidilyInPolyTime.optionElimWithInput + (by unfold eIn encSlotSelectAcc; fun_prop) hsomeCand ?_ + have hq1 := ComputableTidilyInPolyTime.fst eIn eBest + have hq2 := ComputableTidilyInPolyTime.snd eIn eBest + exact ComputableTidilyInPolyTime.ite_decide + (ComputableTidilyInPolyTime.binary_lt' (hscT.comp hq1) + ((ComputableTidilyInPolyTime.snd (encList encNat) encNat).comp hq2)) + (hsomeCand.comp hq1) ((ComputableTidilyInPolyTime.optionSome eBest).comp hq2) + unfold selectSlotStep + exact (show ComputableTidilyInPolyTime (fun s : ℕ × SlotSelectAcc => s.2.1) eIn encScoreParams by + unfold eIn encSlotSelectAcc; fun_prop).prod + ((show ComputableTidilyInPolyTime (fun s : ℕ × SlotSelectAcc => s.2.2.1) + eIn (encPair encBool encUnary) by unfold eIn encSlotSelectAcc; fun_prop).prod + ((show ComputableTidilyInPolyTime (fun s : ℕ × SlotSelectAcc => s.2.2.2.1) + eIn encPartialSchedules by unfold eIn encSlotSelectAcc; fun_prop).prod hbest)) + +private def streamSlotCount (a : StreamSlotIn) : ℕ := a.1.2.1.1 ^ a.1.1.2 +private def streamSlotInit (a : StreamSlotIn) : SlotSelectAcc := (a.1, (a.2.1, (a.2.2, none))) +private def extractBestSlotWord (st : ℕ × SlotSelectAcc) : List ℕ := + st.2.2.2.2.elim (List.replicate st.2.1.1.2 0) Prod.fst + +private theorem computableInPolyTime_streamSlotCount : + ComputableInPolyTime streamSlotCount encStreamSlotIn encNat := by + refine .of_tidy ?_; unfold streamSlotCount encStreamSlotIn encScoreParams; fun_prop + +private theorem computableInPolyTime_streamSlotInit : + ComputableInPolyTime streamSlotInit encStreamSlotIn encSlotSelectAcc := by + refine .of_tidy ?_; unfold streamSlotInit encStreamSlotIn encSlotSelectAcc; fun_prop + +private theorem computableInPolyTime_extractBestSlotWord : + ComputableInPolyTime extractBestSlotWord + (encPair encNat encSlotSelectAcc) (encList encNat) := by + refine .of_tidy ?_; unfold extractBestSlotWord encSlotSelectAcc encScoreParams; fun_prop + +private noncomputable def mkSlotCert + (cn : NativeCertificate streamSlotCount encStreamSlotIn encNat) + (ci : NativeCertificate streamSlotInit encStreamSlotIn encSlotSelectAcc) + (cb : NativeCertificate selectSlotStep (encPair encNat encSlotSelectAcc) encSlotSelectAcc) + (cEx : NativeCertificate extractBestSlotWord + (encPair encNat encSlotSelectAcc) (encList encNat)) : + 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 (encList encNat) := + (cEx.comp (IndexFold.certificate cn ci cb)).congr + fun ⟨⟨⟨n, Q⟩, ⟨r, C⟩, edges⟩, ⟨slot, scheds⟩⟩ => by + have hp := (run_selectSlotStep_params ((n, Q), (r, C), edges) slot scheds (r ^ Q)).1 + simp only [Function.comp_apply, extractBestSlotWord, streamSlotCount, streamSlotInit, + streamBestSlotLabel, hp] + +/-- Uniform native machine certificate for single-slot candidate streaming `streamBestSlotLabel`. -/ +noncomputable def streamBestSlotCertificate : + 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 (encList encNat) := + mkSlotCert (NativeCertificate.ofPolyTime computableInPolyTime_streamSlotCount) + (NativeCertificate.ofPolyTime computableInPolyTime_streamSlotInit) + (NativeCertificate.ofPolyTime computableInPolyTime_selectSlotStep) + (NativeCertificate.ofPolyTime computableInPolyTime_extractBestSlotWord) + +private theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) : + ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ ∀ a, u a ≤ p (size a) := by + obtain ⟨c, d, h⟩ := hu.exists_le + exact ⟨fun n => c * (n + 1) ^ d, by fun_prop, + fun _ _ hxy => Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) d), h⟩ + +private theorem exists_mono_poly_cert {α β : Type} {f : α → β} + {ei : α ↪ List Bool} {eo : β ↪ List Bool} (hf : ComputableInPolyTime f ei eo) : + ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ + ∀ a, (NativeCertificate.ofPolyTime hf).time a ≤ p (ei a).length ∧ + (NativeCertificate.ofPolyTime hf).space a ≤ p (ei a).length := by + have hc := NativeCertificate.ofPolyTime_isPolynomial hf + obtain ⟨p, hp, hmono, hle⟩ := exists_mono_poly (hc.1.add hc.2) + exact ⟨p, hp, hmono, fun a => ⟨by have := hle a; omega, by have := hle a; omega⟩⟩ + +private theorem streamSlotIn_parts_le (a : StreamSlotIn) : + a.1.1.1 ≤ (encStreamSlotIn a).length ∧ a.1.1.2 ≤ (encStreamSlotIn a).length ∧ + (encNat a.1.2.1.1).length ≤ (encStreamSlotIn a).length ∧ + (encNat a.1.2.1.2).length ≤ (encStreamSlotIn a).length ∧ + a.1.2.2.length ≤ (encStreamSlotIn a).length := by + have hed : a.1.2.2.length ≤ (encList (encPair encNat encNat) a.1.2.2).length := by + rw [length_encList]; generalize a.1.2.2 = l; induction l with + | nil => simp only [List.length_nil, List.map_nil, List.sum_nil, le_rfl] + | cons _ _ ih => simp only [List.length_cons, List.map_cons, List.sum_cons]; omega + simp only [encStreamSlotIn, encScoreParams, length_encPair, encUnary_apply, List.length_replicate] + exact ⟨by omega, by omega, by omega, by omega, by omega⟩ + +private theorem hbFull_run_streamSlotInit_le (a : StreamSlotIn) {j : ℕ} + (hj : j ≤ streamSlotCount a) : + (encPair encNat encSlotSelectAcc (IndexFold.run selectSlotStep j (streamSlotInit a))).length ≤ + 8 * (encStreamSlotIn a).length * (encStreamSlotIn a).length + + 15 * (encStreamSlotIn a).length + 28 := by + have hparts := streamSlotIn_parts_le a + rcases a with ⟨⟨⟨n, Q⟩, ⟨r, C⟩, edges⟩, ⟨slot, scheds⟩⟩ + let L := (encStreamSlotIn (((n, Q), (r, C), edges), (slot, scheds))).length + have hsz {x : ℕ} (hx : x ≤ L) : (encNat x).length ≤ L := by + rw [encNat_apply, Nat.size_eq_bits_len]; exact (Nat.size_le_self x).trans hx + have hnL := hsz hparts.1; have hQL := hsz hparts.2.1; have heL := hsz hparts.2.2.2.2 + have hrL := hparts.2.2.1; have hCL := hparts.2.2.2.1 + have hQr : 8 * Q * (encNat r).length ≤ 8 * L * L := by + simpa only [Nat.mul_assoc] using Nat.mul_le_mul_left 8 (Nat.mul_le_mul hparts.2.1 hrL) + have hst := length_encSlotSelectState_run_le n Q r C edges scheds slot hj + change (encPair encNat encSlotSelectAcc + (IndexFold.run selectSlotStep j (((n, Q), (r, C), edges), (slot, (scheds, none))))).length ≤ + 8 * L * L + 15 * L + 28; linarith + +private theorem mkSlotCert_bounds + (cn : NativeCertificate streamSlotCount encStreamSlotIn encNat) + (ci : NativeCertificate streamSlotInit encStreamSlotIn encSlotSelectAcc) + (cb : NativeCertificate selectSlotStep (encPair encNat encSlotSelectAcc) encSlotSelectAcc) + (cEx : NativeCertificate extractBestSlotWord + (encPair encNat encSlotSelectAcc) (encList encNat)) + {pCn pCi pCb pEx : ℕ → ℕ} + (hpCn : Cslib.PolynomiallyBounded pCn) + (hCn : ∀ a, cn.time a ≤ pCn (encStreamSlotIn a).length ∧ + cn.space a ≤ pCn (encStreamSlotIn a).length) + (hpCi : Cslib.PolynomiallyBounded pCi) + (hCi : ∀ a, ci.time a ≤ pCi (encStreamSlotIn a).length ∧ + ci.space a ≤ pCi (encStreamSlotIn a).length) + (hpCb : Cslib.PolynomiallyBounded pCb) (hmCb : Monotone pCb) + (hCb : ∀ s, cb.time s ≤ pCb (encPair encNat encSlotSelectAcc s).length ∧ + cb.space s ≤ pCb (encPair encNat encSlotSelectAcc s).length) + (hpEx : Cslib.PolynomiallyBounded pEx) (hmEx : Monotone pEx) + (hEx : ∀ s, cEx.time s ≤ pEx (encPair encNat encSlotSelectAcc s).length ∧ + cEx.space s ≤ pEx (encPair encNat encSlotSelectAcc s).length) : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ Monotone poly ∧ + ∀ a, (mkSlotCert cn ci cb cEx).time a ≤ + (a.1.2.1.1 ^ a.1.1.2 + 1) * poly (encStreamSlotIn a).length ∧ + (mkSlotCert cn ci cb cEx).space a ≤ poly (encStreamSlotIn a).length := by + let bFull (L : ℕ) := 8 * L * L + 15 * L + 28; let lIdx (L : ℕ) := L * L + 1 + let roundOver (L : ℕ) := 3 * bFull L + 2 * (lIdx L + 1) ^ 2 + pCb (bFull L) + let initExt (L : ℕ) := pCn L + L + pCi L + pEx (bFull L) + lIdx L + have hraw : Cslib.PolynomiallyBounded (fun L => initExt L + roundOver L) := by + dsimp only [initExt, roundOver, bFull, lIdx]; fun_prop + obtain ⟨poly, hpoly, hmpoly, h0⟩ := exists_mono_poly (.of_polynomiallyBounded id hraw) + refine ⟨poly, hpoly, hmpoly, fun a => ?_⟩ + let L := (encStreamSlotIn a).length; let K := streamSlotCount a + have hpolyL : initExt L + roundOver L ≤ poly L := h0 L; have hparts := streamSlotIn_parts_le a + have hlIdx : (encNat K).length ≤ lIdx L := (length_encNat_pow_le a.1.2.1.1 a.1.1.2).trans + (Nat.add_le_add_right (Nat.mul_le_mul hparts.2.1 hparts.2.2.1) 1) + let runAt (j : ℕ) := IndexFold.run selectSlotStep j (streamSlotInit a) + have hbFull (j : ℕ) (hj : j ≤ K) : (encPair encNat encSlotSelectAcc (runAt j)).length ≤ bFull L := + hbFull_run_streamSlotInit_le a hj + let rstep := IndexFold.roundCertificate cb; let initPair := (0, streamSlotInit a) + let M := NativeCertificate.maxStateLength (encPair encNat encSlotSelectAcc) + (IndexFold.step selectSlotStep) K initPair + let RT := NativeCertificate.maxRoundTime rstep K initPair + let RS := NativeCertificate.maxRoundSpace rstep K initPair + have hmaxS : M ≤ bFull L := NativeCertificate.maxStateLength_le _ _ _ _ hbFull + have hcn_a : cn.time a ≤ pCn L ∧ cn.space a ≤ pCn L := hCn a + have hci_a : ci.time a ≤ pCi L ∧ ci.space a ≤ pCi L := hCi a + have hexT : cEx.time (runAt K) ≤ pEx (bFull L) := (hEx _).1.trans (hmEx (hbFull K le_rfl)) + have hexS : cEx.space (runAt K) ≤ pEx (bFull L) := (hEx _).2.trans (hmEx (hbFull K le_rfl)) + refine ⟨?_, ?_⟩ + · have hmaxRT : RT ≤ bFull L + (lIdx L + 1) ^ 2 + pCb (bFull L) := by + refine NativeCertificate.maxRoundTime_le _ _ _ fun j hj => ?_ + have hj_len : (encNat (runAt j).1).length ≤ lIdx L := by + rw [IndexFold.run_index]; exact (ComputableTidilyInO.length_encNat_mono hj).trans hlIdx + have hsq := Nat.pow_le_pow_left (Nat.add_le_add_right hj_len 1) 2 + have hcbT : cb.time (runAt j) ≤ pCb (bFull L) := (hCb _).1.trans (hmCb (hbFull j hj)) + have hst_len := hbFull j hj + change (encPair encNat encSlotSelectAcc (runAt j)).length + + ((encNat (runAt j).1).length + 1) ^ 2 + cb.time (runAt j) ≤ _; omega + have hsqK : ((encNat K).length + 1) ^ 2 ≤ (lIdx L + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hround : RT + M + ((encNat K).length + 1) ^ 2 ≤ roundOver L := by + dsimp only [roundOver]; omega + calc (mkSlotCert cn ci cb cEx).time a + = (cn.time a + (L + ci.time a) + + (K + 1) * (RT + M + ((encNat K).length + 1) ^ 2)) + cEx.time (runAt K) := rfl + _ ≤ initExt L + (K + 1) * roundOver L := by + have := Nat.mul_le_mul_left (K + 1) hround; dsimp only [initExt]; omega + _ ≤ (K + 1) * initExt L + (K + 1) * roundOver L := + Nat.add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos _)) _ + _ = (K + 1) * (initExt L + roundOver L) := by ring + _ ≤ (K + 1) * poly L := Nat.mul_le_mul_left _ hpolyL + · have hmaxRS : RS ≤ bFull L + (lIdx L + 1) + pCb (bFull L) := by + refine NativeCertificate.maxRoundSpace_le _ _ _ fun j hj => ?_ + have hj_len : (encNat (runAt j).1).length ≤ lIdx L := by + rw [IndexFold.run_index]; exact (ComputableTidilyInO.length_encNat_mono hj).trans hlIdx + have hcbS : cb.space (runAt j) ≤ pCb (bFull L) := (hCb _).2.trans (hmCb (hbFull j hj)) + have hst_len := hbFull j hj + change (encPair encNat encSlotSelectAcc (runAt j)).length + + ((encNat (runAt j).1).length + 1) + cb.space (runAt j) ≤ _; omega + have hlin_sq : lIdx L + 1 ≤ 2 * (lIdx L + 1) ^ 2 := + (Nat.le_mul_self _).trans (by rw [sq]; omega) + calc (mkSlotCert cn ci cb cEx).space a + = (cn.space a + (L + ci.space a) + RS + M + (encNat K).length) + cEx.space (runAt K) := rfl + _ ≤ initExt L + roundOver L := by dsimp only [initExt, roundOver]; omega + _ ≤ poly L := hpolyL + +/-- Trajectory-maximum time and polynomial-workspace bounds for `streamBestSlotCertificate`. -/ +theorem streamBestSlotCertificate_bounds : + ∃ poly : ℕ → ℕ, Cslib.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 := by + obtain ⟨pCn, hpCn, _, hCn⟩ := exists_mono_poly_cert computableInPolyTime_streamSlotCount + obtain ⟨pCi, hpCi, _, hCi⟩ := exists_mono_poly_cert computableInPolyTime_streamSlotInit + obtain ⟨pCb, hpCb, hmCb, hCb⟩ := exists_mono_poly_cert computableInPolyTime_selectSlotStep + obtain ⟨pEx, hpEx, hmEx, hEx⟩ := exists_mono_poly_cert computableInPolyTime_extractBestSlotWord + exact mkSlotCert_bounds _ _ _ _ hpCn hCn hpCi hCi hpCb hmCb hCb hpEx hmEx hEx + +/-- `streamBestSlotLabel` runs in `O((r ^ Q + 1) * poly(|input|))` native time and polynomial +workspace. -/ +theorem computableInO_streamBestSlotLabel : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + 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 (encList encNat) + (fun a => (a.1.2.1.1 ^ a.1.1.2 + 1) * poly (encStreamSlotIn a).length) + (fun a => poly (encStreamSlotIn a).length) := by + obtain ⟨poly, hpoly, _, hB⟩ := streamBestSlotCertificate_bounds + exact ⟨poly, hpoly, streamBestSlotCertificate.computes.mono_le + (fun a => (hB a).1) (fun a => (hB a).2)⟩ + +/-- `streamBestSlotLabel` runs in polynomial workspace (`ComputableInPolySpace`) without +materializing `r ^ Q` candidate words. -/ +theorem computableInPolySpace_streamBestSlotLabel : + 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 (encList encNat) := by + obtain ⟨poly, hpoly, c, hc, hl⟩ := computableInO_streamBestSlotLabel + exact ⟨_, fun n => c * (poly n + 1), by fun_prop, hc, hl⟩ + +end Cslib.BalancedSchedules + +end diff --git a/ComplexityTests/GreedySlotScore.lean b/ComplexityTests/GreedySlotScore.lean new file mode 100644 index 0000000000..a5aab15611 --- /dev/null +++ b/ComplexityTests/GreedySlotScore.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +import Complexity.Computability.PolyTime.GreedySlotScore +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Mathlib.Tactic.NormNum + +/-! +# Concrete tests for greedy slot-score arithmetic and streaming candidate selection +-/ + +namespace ComplexityTests.GreedySlotScore + +open Finset Cslib.BalancedSchedules Cslib.GenericRAM Turing.MultiTapeTM + +-- Boundary regimes: Q = 0, r = 1, r = 0 (with Q > 0 triggering r ^ Q = 0 fallback), E = 0, C = 0. +example : decodeLabelWord 3 0 17 = [] := rfl +example : decodeLabelWord 1 4 29 = [0, 0, 0, 0] := by decide +example : streamBestSlotLabel 2 3 0 4 [(0, 1)] ([none, none], [none]) (false, 0) = [0, 0, 0] := by + decide +example : clearedJointScore 0 2 3 4 [] [] [] = 0 := by decide +example : clearedJointScore 3 2 2 0 [(0, 1)] [some [1, 0], none, none] [none] = + clearedGroupPotential 3 2 2 [some [1, 0], none, none] * (4 ^ 2 * 1) := by decide +example : scoreDenom 0 0 2 3 0 = 81 * 1 * 3 * 1 := by decide + +-- Radix-r candidate codec round-trips and full r ^ Q = 9 bijection at r = 3, Q = 2. +example : decodeLabelWord 3 3 19 = [1, 0, 2] := by decide +example : Nat.ofDigits 3 (decodeLabelWord 3 3 19) = 19 := by decide +example : ((List.range 9).map fun j => Nat.ofDigits 3 (decodeLabelWord 3 2 j)) = + List.range 9 := by decide +example : (List.ofFn fun j : Fin (3 ^ 2) => + scheduleToWord (wordToSchedule (by decide : 1 ≤ 3) 2 (decodeLabelWord 3 2 j.val))) = + (List.ofFn fun j : Fin (3 ^ 2) => + scheduleToWord ((finFunctionFinEquiv (m := 3) (n := 2)).symm j)) := by + congr 1; funext j; rw [wordToSchedule_decodeLabelWord_eq_finFunctionFinEquiv_symm] + +-- Out-of-range digit clamping in wordToSchedule defaults digits ≥ r to 0. +example : scheduleToWord (wordToSchedule (by decide : 1 ≤ 3) 3 [2, 7, 1]) = [2, 0, 1] := by decide + +-- Concrete clearedPartialCollision cases: diagonal, matching, distinct, and unassigned. +example : clearedPartialCollision 4 [some [1, 0], some [1, 1], none] 2 2 = 4 := rfl +example : clearedPartialCollision 4 [some [1, 0], some [1, 0], none] 0 1 = 4 := by decide +example : clearedPartialCollision 4 [some [1, 0], some [1, 1], none] 0 1 = 0 := by decide +example : clearedPartialCollision 4 [some [1, 0], some [1, 1], none] 0 2 = 1 := by decide + +-- Concrete 2-variable, 2-factor hypergraph on r = 2, Q = 2: exact rational bridge check. +private def testEdge : Fin 3 → Fin 2 × Fin 2 + | ⟨0, _⟩ => (0, 0) | ⟨1, _⟩ => (0, 1) | ⟨2, _⟩ => (1, 0) +private def testVars : Fin 2 → Option (Fin 2 → Fin 2) | ⟨0, _⟩ => some ![0, 1] | ⟨1, _⟩ => none +private def testFacs : Fin 2 → Option (Fin 2 → Fin 2) | ⟨0, _⟩ => some ![1, 0] | ⟨1, _⟩ => none + +example : edgesOfFin testEdge = [(0, 0), (0, 1), (1, 0)] := by decide +example : partialScheduleListOfFin testVars = [some [0, 1], none] := by decide +example : normalizedPartialScore testEdge testVars testFacs 4 = 51 / 64 := by + rw [normalizedPartialScore_eq_clearedJointScore_div (by decide) testEdge testVars testFacs 4, + show clearedJointScore 2 2 2 4 (edgesOfFin testEdge) + (partialScheduleListOfFin testVars) (partialScheduleListOfFin testFacs) = 1224 by decide, + show scoreDenom 3 2 2 2 4 = 1536 by decide]; norm_num + +-- Strictly better candidate reduces clearedJointScore; symmetric slot breaks ties by index 0. +example : decodeLabelWord 2 2 1 = [1, 0] ∧ decodeLabelWord 2 2 2 = [0, 1] := by decide +example : let scheds := (partialScheduleListOfFin testVars, partialScheduleListOfFin testFacs) + candidateSlotScore 2 2 2 4 (edgesOfFin testEdge) scheds (false, 1) 1 < + candidateSlotScore 2 2 2 4 (edgesOfFin testEdge) scheds (false, 1) 2 := by decide +example : let emptyScheds := ([none, none], [none, none]) + candidateSlotScore 2 2 2 4 [(0, 0), (1, 1)] emptyScheds (false, 0) 0 = + candidateSlotScore 2 2 2 4 [(0, 0), (1, 1)] emptyScheds (false, 0) 3 ∧ + streamBestSlotLabel 2 2 2 4 [(0, 0), (1, 1)] emptyScheds (false, 0) = [0, 0] := by decide + +-- Concrete evaluation of bestVariableLabel and bestFactorLabel via streamBestSlotLabel bridges. +example : bestVariableLabel testEdge testVars testFacs 4 ⟨1, by decide⟩ + (candidateScheduleList (by decide : 1 ≤ 2) 2) = some ![1, 0] := by + rw [← streamBestSlotLabel_false_eq_bestVariableLabel (by decide) testEdge testVars testFacs 4 + ⟨1, by decide⟩, Option.some.injEq] + apply scheduleToWord_inj (by decide : 1 ≤ 2) + rw [scheduleToWord_wordToSchedule (by decide) (length_streamBestSlotLabel ..) + (fun _ hx => mem_streamBestSlotLabel_lt (by decide) _ _ _ _ _ _ hx)]; decide + +example : bestFactorLabel testEdge testVars testFacs 4 ⟨1, by decide⟩ + (candidateScheduleList (by decide : 1 ≤ 2) 2) = some ![0, 0] := by + rw [← streamBestSlotLabel_true_eq_bestFactorLabel (by decide) testEdge testVars testFacs 4 + ⟨1, by decide⟩, Option.some.injEq] + apply scheduleToWord_inj (by decide : 1 ≤ 2) + rw [scheduleToWord_wordToSchedule (by decide) (length_streamBestSlotLabel ..) + (fun _ hx => mem_streamBestSlotLabel_lt (by decide) _ _ _ _ _ _ hx)]; decide + +-- Concrete all-prefix live-state bit-length bound check across j = 0 .. 4. +example : ∀ j ≤ 2 ^ 2, + (encPair encNat encSlotSelectAcc + (IndexFold.run selectSlotStep j (((2, 2), (2, 4), [(0, 0), (0, 1)]), + ((false, 1), (([some [0, 1], none], [none]), none))))).length ≤ + 2 * (encStreamSlotIn (((2, 2), (2, 4), [(0, 0), (0, 1)]), + ((false, 1), ([some [0, 1], none], [none])))).length + 96 := + fun _ hj => (length_encSlotSelectState_run_le 2 2 2 4 [(0, 0), (0, 1)] + ([some [0, 1], none], [none]) (false, 1) hj).trans (by + simp only [Nat.add_assoc]; exact Nat.add_le_add_left (by decide) _) + +-- Compositional fun_prop and polynomial-space checks on nontrivial expressions. +example : ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ => decodeLabelWord (p.1.1 + 1) p.1.2 p.2) + (encPair (encPair encNat encUnary) encNat) (encList encNat) := by fun_prop +example : ComputableInPolyTime (fun p : ((Bool × ℕ) × Option (List ℕ)) × + (List (Option (List ℕ)) × List (Option (List ℕ))) => + readSlotSchedule p.1.1 (updateSlotSchedules p.1.1 p.1.2 p.2)) + (encPair (encPair (encPair encBool encUnary) (encOption (encList encNat))) + encPartialSchedules) (encOption (encList encNat)) := by fun_prop +example : ComputableInPolySpace (fun p : StreamSlotIn × ℕ => + streamBestSlotLabel p.1.1.1.1 p.1.1.1.2 p.1.1.2.1.1 p.1.1.2.1.2 p.1.1.2.2 p.1.2.2 p.1.2.1) + (encPair encStreamSlotIn encNat) (encList encNat) := + computableInPolySpace_streamBestSlotLabel.comp + (.of_polyTime (ComputableInPolyTime.fst encStreamSlotIn encNat)) + +end ComplexityTests.GreedySlotScore From ce162a215ef0786dbdca02c7f433c1daac51f642 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Tue, 27 Oct 2026 08:57:43 +0000 Subject: [PATCH 2/4] feat(PolyTime): add greedy balanced schedule pass and certificates (#1226) --- Complexity.lean | 1 + .../PolyTime/GreedyLabelSchedule.lean | 1319 +++++++++++++++++ ComplexityTests/GreedyLabelSchedule.lean | 117 ++ 3 files changed, 1437 insertions(+) create mode 100644 Complexity/Computability/PolyTime/GreedyLabelSchedule.lean create mode 100644 ComplexityTests/GreedyLabelSchedule.lean diff --git a/Complexity.lean b/Complexity.lean index 824839e0ac..45d01ae03a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1382,6 +1382,7 @@ public import Complexity.Computability.PolyTime.CNF.GreedyParityContext public import Complexity.Computability.PolyTime.CNF.GreedyParitySearch public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck +public import Complexity.Computability.PolyTime.GreedyLabelSchedule public import Complexity.Computability.PolyTime.GreedySlotScore public import Complexity.Computability.PolyTime.Int.ExactDiv public import Complexity.Computability.PolyTime.Int.Jet diff --git a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean new file mode 100644 index 0000000000..6610a4c2da --- /dev/null +++ b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean @@ -0,0 +1,1319 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.PolyTime.GreedySlotScore +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Foundations.Data.List.Lookup +import Mathlib.Data.List.GetD +import Mathlib.Data.List.OfFn +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Runtime construction of balanced label schedules + +Completes the `(n + m)`-slot greedy pass and empty-scope factor normalization of Lemma 4.5 of +[OpenAI2026ETH] (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`). + +Encoded `ComputableInPolyTime`, `NativeCertificate`, `ComputableInO`, and `ComputableInPolySpace` +theorems govern the concrete list/integer operations (`slotOfIndex`, `pendingSlotOfState`, +`greedySlotStepBody`, `greedySchedulePass`, `normalizeEmptyFactorSchedules`, +`constructBalancedSchedules`, and their certificates) 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 `NativeCertificate`s. + +## 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*][OpenAI2026ETH], §4.4, Lemma 4.5, pp. 30–32. +-/ + +@[expose] public section + +namespace Cslib.BalancedSchedules + +open Finset Cslib.GenericRAM Turing.MultiTapeTM +open scoped BigOperators + +/-! ### Section 1: `(n + m)`-slot pass and empty-scope factor normalization -/ + +/-- 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. -/ +def slotOfIndex (n m s : ℕ) : Option (Bool × ℕ) := + let sCap := min (n + m) s + if s < n then some (false, sCap) + else if s < n + m then some (true, sCap - n) + else none + +/-- Runtime input tuple `((n, m, Q), (r, C), edges)` for full schedule construction. -/ +abbrev ScheduleParams : Type := (ℕ × ℕ × ℕ) × (ℕ × ℕ) × List (ℕ × ℕ) + +/-- Return `some slot` when `s < n + m` points to a still-unassigned slot, or `none` otherwise. -/ +def pendingSlotOfState + (state : ℕ × (ScheduleParams × (List (Option (List ℕ)) × List (Option (List ℕ))))) : + Option (Bool × ℕ) := + (slotOfIndex state.2.1.1.1 state.2.1.1.2.1 state.1).elim none fun slot => + if (readSlotSchedule slot state.2.2).isSome then none else some slot + +/-- Outer `IndexFold.run` callback fixing unassigned slot `s < n + m` via `streamBestSlotLabel`. -/ +def greedySlotStepBody + (state : ℕ × (ScheduleParams × (List (Option (List ℕ)) × List (Option (List ℕ))))) : + ScheduleParams × (List (Option (List ℕ)) × List (Option (List ℕ))) := + (pendingSlotOfState state).elim state.2 fun slot => + let p := state.2.1 + let chosen := streamBestSlotLabel p.1.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2 state.2.2 slot + (p, updateSlotSchedules slot (some chosen) state.2.2) + +/-- Full `(n + m)`-slot greedy partial-schedule pass implemented with `IndexFold.run`. -/ +def greedySchedulePass (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : + List (Option (List ℕ)) × List (Option (List ℕ)) := + (IndexFold.run greedySlotStepBody (n + m) + (((n, m, Q), (r, C), edges), (List.replicate n none, List.replicate m none))).2.2 + +/-- Replace schedules of empty-scope factors (`∀ e ∈ edges, e.1 ≠ f`) with `List.replicate Q 0`. -/ +def normalizeEmptyFactorSchedules (Q : ℕ) (edges : List (ℕ × ℕ)) + (facWords : List (List ℕ)) : List (List ℕ) := + (List.range facWords.length).map fun f => + if edges.any (fun e => decide (e.1 = f)) then facWords.getD f [] else List.replicate Q 0 + +/-- 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). -/ +def constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : + List (List ℕ) × List (List ℕ) := + let raw := greedySchedulePass n m Q r C edges + (raw.1.map fun o => o.getD (List.replicate Q 0), + normalizeEmptyFactorSchedules Q edges (raw.2.map fun o => o.getD (List.replicate Q 0))) + +/-! ### Section 2: Prefix invariants and Lemma 4.5 occupancy bounds -/ + +private theorem run_greedySlotStepBody_params (params : ScheduleParams) + (initScheds : List (Option (List ℕ)) × List (Option (List ℕ))) (s : ℕ) : + (IndexFold.run greedySlotStepBody s (params, initScheds)).2.1 = params := by + induction s with + | zero => rfl + | succ s ih => + rw [IndexFold.run_succ]; simp only [IndexFold.step, greedySlotStepBody] + cases pendingSlotOfState _ <;> simp only [Option.elim_none, Option.elim_some, ih] + +/-- 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`. -/ +theorem run_greedySlotStepBody_wf (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) (s : ℕ) : + let scheds := (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, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) ∧ + (∀ o ∈ scheds.2, ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) := by + induction s with + | zero => + simp only [IndexFold.run_zero, List.length_replicate, true_and] + have hnone (N : ℕ) : ∀ o ∈ List.replicate N (none : Option (List ℕ)), + ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1 := fun o ho _ hw => by + rcases List.mem_replicate.mp ho with ⟨_, rfl⟩; cases hw + exact ⟨hnone n, hnone m⟩ + | succ s ih => + have hp := run_greedySlotStepBody_params ((n, m, Q), (r, C), edges) + (List.replicate n none, List.replicate m none) s + rw [IndexFold.run_succ]; simp only [IndexFold.step, greedySlotStepBody] + cases pendingSlotOfState _ with + | none => exact ih + | some slot => + simp only [Option.elim_some]; rw [hp] + have hset {L : List (Option (List ℕ))} {idx : ℕ} {chosen : List ℕ} + (hL : ∀ o ∈ L, ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) + (hcl : chosen.length = Q) (hcm : ∀ x ∈ chosen, x < max r 1) : + ∀ o ∈ L.set idx (some chosen), ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1 := + fun o ho w hw => by + rcases List.mem_or_eq_of_mem_set ho with hmem | heq + · exact hL o hmem w hw + · rw [heq] at hw; injection hw with hw'; subst hw'; exact ⟨hcl, hcm⟩ + rcases slot with ⟨isFac, idx⟩; cases isFac + · simp only [updateSlotSchedules, Bool.false_eq_true, ↓reduceIte, List.length_set] + exact ⟨ih.1, ih.2.1, hset ih.2.2.1 (length_streamBestSlotLabel _ _ _ _ _ _ _) + (fun _ hx => mem_streamBestSlotLabel_lt_max _ _ _ _ _ _ _ hx), ih.2.2.2⟩ + · simp only [updateSlotSchedules, ↓reduceIte, List.length_set] + exact ⟨ih.1, ih.2.1, ih.2.2.1, hset ih.2.2.2 (length_streamBestSlotLabel _ _ _ _ _ _ _) + (fun _ hx => mem_streamBestSlotLabel_lt_max _ _ _ _ _ _ _ hx)⟩ + +@[simp] theorem length_fst_constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : + (constructBalancedSchedules n m Q r C edges).1.length = n := by + simp only [constructBalancedSchedules, greedySchedulePass, List.length_map, + (run_greedySlotStepBody_wf n m Q r C edges (n + m)).1] + +@[simp] theorem length_snd_constructBalancedSchedules (n m Q r C : ℕ) (edges : List (ℕ × ℕ)) : + (constructBalancedSchedules n m Q r C edges).2.length = m := by + simp only [constructBalancedSchedules, normalizeEmptyFactorSchedules, List.length_map, + List.length_range, greedySchedulePass, (run_greedySlotStepBody_wf n m Q r C edges (n + m)).2.1] + +/-- Every variable and factor word produced by `constructBalancedSchedules` has exact length `Q` +and digits `< max r 1` (hence `< r` whenever `1 ≤ r`). -/ +theorem 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) := by + obtain ⟨_, hm_len, hwf1, hwf2⟩ := run_greedySlotStepBody_wf n m Q r C edges (n + m) + have hrep : (List.replicate Q 0).length = Q ∧ ∀ x ∈ List.replicate Q 0, x < max r 1 := + ⟨List.length_replicate, fun x hx => by rcases List.mem_replicate.mp hx with ⟨_, rfl⟩; omega⟩ + refine ⟨fun w hw => ?_, fun w hw => ?_⟩ + · simp only [constructBalancedSchedules, greedySchedulePass, List.mem_map] at hw + obtain ⟨o, ho, rfl⟩ := hw; cases o with + | none => simpa only [Option.getD_none] using hrep + | some u => simpa only [Option.getD_some] using hwf1 (some u) ho u rfl + · simp only [constructBalancedSchedules, normalizeEmptyFactorSchedules, List.mem_map, + List.mem_range, List.length_map, greedySchedulePass, hm_len] at hw + obtain ⟨f, hf, hw_eq⟩ := hw; split_ifs at hw_eq + · subst hw_eq + let raw2 := (IndexFold.run greedySlotStepBody (n + m) + (((n, m, Q), (r, C), edges), (List.replicate n none, List.replicate m none))).2.2.2 + rw [List.getD_eq_getElem _ _ (by simp only [List.length_map, hm_len]; exact hf), + List.getElem_map] + have hmem : raw2[f] ∈ raw2 := List.getElem_mem (by rw [hm_len]; exact hf) + cases ho : raw2[f] with + | none => simpa only [Option.getD_none] using hrep + | some u => rw [ho] at hmem; simpa only [Option.getD_some] using hwf2 (some u) hmem u rfl + · subst hw_eq; exact hrep + +/-- Concrete empty-factor normalization: any factor `f < m` absent from `edges` gets +`List.replicate Q 0`. -/ +theorem 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 := by + have hm := (run_greedySlotStepBody_wf n m Q r C edges (n + m)).2.1 + simp only [constructBalancedSchedules, normalizeEmptyFactorSchedules, greedySchedulePass] + rw [List.getD_map_range _ [] (by simp only [List.length_map, hm]; exact hf)] + have hany : edges.any (fun e => decide (e.1 = f)) = false := + List.any_eq_false.mpr fun e he => by + simp only [Bool.not_eq_true, decide_eq_false_iff_not]; exact hempty e he + simp only [hany, Bool.false_eq_true, ↓reduceIte] + +/-- Exact bridge between the runtime `IndexFold.run` schedule pass `greedySchedulePass` and the +combinatorial specification `greedyLabelPass`. -/ +theorem 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) = + let slots : List (Fin n ⊕ Fin m) := + (List.ofFn fun v : Fin n => Sum.inl v) ++ (List.ofFn fun f : Fin m => Sum.inr f) + let res := greedyLabelPass edge C (candidateScheduleList hr Q) slots + (fun _ => none, fun _ => none) + (partialScheduleListOfFin res.1, partialScheduleListOfFin res.2) := by + dsimp only + let toLists (assigned : (Fin n → Option (Fin Q → Fin r)) × (Fin m → Option (Fin Q → Fin r))) := + (partialScheduleListOfFin assigned.1, partialScheduleListOfFin assigned.2) + have hstep_var (assigned : (Fin n → Option (Fin Q → Fin r)) × (Fin m → Option (Fin Q → Fin r))) + (v : Fin n) : + (if (readSlotSchedule (false, v.val) (toLists assigned)).isSome then toLists assigned + else updateSlotSchedules (false, v.val) + (some (streamBestSlotLabel n Q r C (edgesOfFin edge) (toLists assigned) (false, v.val))) + (toLists assigned)) = + toLists (greedyLabelStep edge C (candidateScheduleList hr Q) assigned (.inl v)) := by + have hread : readSlotSchedule (false, v.val) (toLists assigned) = + (assigned.1 v).map scheduleToWord := by + simp only [toLists, readSlotSchedule, Bool.false_eq_true, ↓reduceIte, + partialScheduleListOfFin, List.getD_ofFn] + rw [hread]; dsimp only [toLists] + cases hv : assigned.1 v with + | some _ => simp only [Option.map_some, Option.isSome_some, ↓reduceIte, greedyLabelStep, hv] + | none => + simp only [Option.map_none, Option.isSome_none, Bool.false_eq_true, ↓reduceIte, + greedyLabelStep, hv, updateSlotSchedules, + set_partialScheduleListOfFin (hr := hr) assigned.1 v _ + (length_streamBestSlotLabel _ _ _ _ _ _ _) + (fun _ hx => mem_streamBestSlotLabel_lt hr _ _ _ _ _ _ hx)] + rw [streamBestSlotLabel_false_eq_bestVariableLabel hr edge assigned.1 assigned.2 C v] + have hstep_fac (assigned : (Fin n → Option (Fin Q → Fin r)) × (Fin m → Option (Fin Q → Fin r))) + (f : Fin m) : + (if (readSlotSchedule (true, f.val) (toLists assigned)).isSome then toLists assigned + else updateSlotSchedules (true, f.val) + (some (streamBestSlotLabel n Q r C (edgesOfFin edge) (toLists assigned) (true, f.val))) + (toLists assigned)) = + toLists (greedyLabelStep edge C (candidateScheduleList hr Q) assigned (.inr f)) := by + have hread : readSlotSchedule (true, f.val) (toLists assigned) = + (assigned.2 f).map scheduleToWord := by + simp only [toLists, readSlotSchedule, ↓reduceIte, partialScheduleListOfFin, List.getD_ofFn] + rw [hread]; dsimp only [toLists] + cases hf : assigned.2 f with + | some _ => simp only [Option.map_some, Option.isSome_some, ↓reduceIte, greedyLabelStep, hf] + | none => + simp only [Option.map_none, Option.isSome_none, Bool.false_eq_true, ↓reduceIte, + greedyLabelStep, hf, updateSlotSchedules, + set_partialScheduleListOfFin (hr := hr) assigned.2 f _ + (length_streamBestSlotLabel _ _ _ _ _ _ _) + (fun _ hx => mem_streamBestSlotLabel_lt hr _ _ _ _ _ _ hx)] + rw [streamBestSlotLabel_true_eq_bestFactorLabel hr edge assigned.1 assigned.2 C f] + let slotFin (s : ℕ) (hs : s < n + m) : Fin n ⊕ Fin m := + if h : s < n then .inl ⟨s, h⟩ else .inr ⟨s - n, by omega⟩ + have hslots_eq : (List.ofFn fun v : Fin n => (Sum.inl v : Fin n ⊕ Fin m)) ++ + (List.ofFn fun f : Fin m => Sum.inr f) = + List.ofFn fun i : Fin (n + m) => slotFin i.val i.isLt := by + apply List.ext_getElem (by simp only [List.length_append, List.length_ofFn]) + intro s _ hsm; simp only [List.length_ofFn] at hsm + simp only [List.getElem_ofFn]; by_cases hsn : s < n + · rw [List.getElem_append_left (by simp only [List.length_ofFn]; exact hsn)] + simp only [List.getElem_ofFn, slotFin, hsn, ↓reduceDIte] + · rw [List.getElem_append_right (by simp only [List.length_ofFn]; omega)] + simp only [List.length_ofFn, List.getElem_ofFn, slotFin, hsn, ↓reduceDIte] + rw [hslots_eq, greedySchedulePass] + let params : ScheduleParams := ((n, m, Q), (r, C), edgesOfFin edge) + let initScheds := (List.replicate n (none : Option (List ℕ)), + List.replicate m (none : Option (List ℕ))) + have hrep_ofFn (N : ℕ) : List.replicate N (none : Option (List ℕ)) = + partialScheduleListOfFin (Q := Q) (r := r) (fun _ : Fin N => none) := by + simp only [partialScheduleListOfFin, Option.map_none, List.ofFn_const] + have hloop : ∀ k (hk : k ≤ n + m), + (IndexFold.run greedySlotStepBody k (params, initScheds)).2.2 = + toLists (greedyLabelPass edge C (candidateScheduleList hr Q) + (List.ofFn fun i : Fin k => slotFin i.val (lt_of_lt_of_le i.isLt hk)) + (fun _ => none, fun _ => none)) := by + intro k hk; induction k with + | zero => + simp only [IndexFold.run_zero, List.ofFn_zero, greedyLabelPass, List.foldl_nil, initScheds, + toLists] + exact Prod.ext (hrep_ofFn n) (hrep_ofFn m) + | succ k ih => + have hk_lt : k < n + m := by omega + let prev := greedyLabelPass edge C (candidateScheduleList hr Q) + (List.ofFn fun i : Fin k => slotFin i.val (lt_trans i.isLt hk_lt)) + (fun _ => none, fun _ => none) + have hst_eta : IndexFold.run greedySlotStepBody k (params, initScheds) = + (k, (params, toLists prev)) := + Prod.ext (IndexFold.run_index _ _ _) + (Prod.ext (run_greedySlotStepBody_params _ _ _) (ih (Nat.le_of_lt hk_lt))) + have hsnoc : greedyLabelPass edge C (candidateScheduleList hr Q) + (List.ofFn fun i : Fin (k + 1) => slotFin i.val (lt_of_lt_of_le i.isLt hk)) + (fun _ => none, fun _ => none) = + greedyLabelStep edge C (candidateScheduleList hr Q) prev (slotFin k hk_lt) := by + rw [List.ofFn_succ', List.concat_eq_append] + simp only [Fin.val_castSucc, Fin.val_last, greedyLabelPass, List.foldl_append, + List.foldl_cons, List.foldl_nil, prev] + rw [hsnoc, IndexFold.run_succ, hst_eta] + simp only [IndexFold.step, greedySlotStepBody, pendingSlotOfState, params] + by_cases hkn : k < n + · have hsl : slotOfIndex n m k = some (false, k) := by + simp only [slotOfIndex, min_eq_right (Nat.le_of_lt hk_lt), hkn, ↓reduceIte] + have hv := hstep_var prev ⟨k, hkn⟩ + simp only [hsl, Option.elim_some, slotFin, hkn, ↓reduceDIte] + cases hcond : (readSlotSchedule (false, k) (toLists prev)).isSome <;> + simpa only [hcond, ↓reduceIte, Bool.false_eq_true, Option.elim_none, + Option.elim_some] using hv + · have hsl : slotOfIndex n m k = some (true, k - n) := by + simp only [slotOfIndex, min_eq_right (Nat.le_of_lt hk_lt), hkn, hk_lt, ↓reduceIte] + have hf := hstep_fac prev ⟨k - n, by omega⟩ + simp only [hsl, Option.elim_some, slotFin, hkn, ↓reduceDIte] + cases hcond : (readSlotSchedule (true, k - n) (toLists prev)).isSome <;> + simpa only [hcond, ↓reduceIte, Bool.false_eq_true, Option.elim_none, + Option.elim_some] using hf + exact hloop (n + m) le_rfl + +/-- Typed variable schedule `Fin n → Fin Q → Fin r` extracted from `constructBalancedSchedules`. -/ +def constructedVarSchedule {r : ℕ} (hr : 1 ≤ r) (n m Q C : ℕ) (edges : List (ℕ × ℕ)) + (v : Fin n) : Fin Q → Fin r := + wordToSchedule hr Q (((constructBalancedSchedules n m Q r C edges).1).getD v.val []) + +/-- Typed factor schedule `Fin m → Fin Q → Fin r` extracted from `constructBalancedSchedules`. -/ +def constructedFactorSchedule {r : ℕ} (hr : 1 ≤ r) (n m Q C : ℕ) (edges : List (ℕ × ℕ)) + (f : Fin m) : Fin Q → Fin r := + wordToSchedule hr Q (((constructBalancedSchedules n m Q r C edges).2).getD f.val []) + +/-- Typed schedules extracted from `constructBalancedSchedules` coincide with completing and +normalizing `greedyLabelPass`. -/ +theorem constructedSchedules_eq_pass {E m n Q r : ℕ} (hr : 1 ≤ r) + (edge : Fin E → Fin m × Fin n) (C : ℕ) : + let g₀ : Fin r := ⟨0, hr⟩ + let slots : List (Fin n ⊕ Fin m) := + (List.ofFn fun v : Fin n => Sum.inl v) ++ (List.ofFn fun f : Fin m => Sum.inr f) + let raw := greedyLabelPass edge C (candidateScheduleList hr Q) slots + (fun _ => none, fun _ => none) + constructedVarSchedule hr n m Q C (edgesOfFin edge) = + completeLabels raw.1 (fun _ _ => g₀) ∧ + constructedFactorSchedule hr n m Q C (edgesOfFin edge) = + normalizeEmptyFactors (fun e => (edge e).1) g₀ (completeLabels raw.2 (fun _ _ => g₀)) := by + dsimp only + let slots : List (Fin n ⊕ Fin m) := + (List.ofFn fun v : Fin n => Sum.inl v) ++ (List.ofFn fun f : Fin m => Sum.inr f) + let raw := greedyLabelPass edge C (candidateScheduleList hr Q) slots + (fun _ => none, fun _ => none) + have hpass := greedySchedulePass_eq_greedyLabelPass (Q := Q) hr edge C + have hw0 : wordToSchedule hr Q (List.replicate Q 0) = fun _ => ⟨0, hr⟩ := by + funext t; rw [wordToSchedule] + have hget : (List.replicate Q 0).getD t.val 0 = 0 := by + rw [List.getD_eq_getElem _ _ (by simp only [List.length_replicate]; exact t.isLt)] + simp only [List.getElem_replicate] + rw [hget]; split_ifs <;> rfl + refine ⟨funext fun v => ?_, funext fun f => ?_⟩ + · simp only [constructedVarSchedule] + rw [List.getD_eq_getElem _ _ (by rw [length_fst_constructBalancedSchedules]; exact v.isLt)] + simp only [constructBalancedSchedules, hpass, List.getElem_map, partialScheduleListOfFin, + List.getElem_ofFn, completeLabels] + cases raw.1 v <;> simp only [Option.map_none, Option.map_some, Option.getD_none, + Option.getD_some, hw0, wordToSchedule_scheduleToWord] + · simp only [constructedFactorSchedule] + rw [List.getD_eq_getElem _ _ (by rw [length_snd_constructBalancedSchedules]; exact f.isLt)] + simp only [constructBalancedSchedules, normalizeEmptyFactorSchedules, hpass, + List.getElem_map, List.getElem_range] + have hany_iff : (edgesOfFin edge).any (fun e => decide (e.1 = f.val)) = true ↔ + ∃ e : Fin E, (edge e).1 = f := by + simp only [edgesOfFin, List.any_eq_true, List.mem_ofFn, decide_eq_true_eq, Fin.ext_iff] + exact ⟨fun ⟨_, ⟨e, rfl⟩, he⟩ => ⟨e, he⟩, fun ⟨e, he⟩ => ⟨_, ⟨e, rfl⟩, he⟩⟩ + by_cases hex : ∃ e : Fin E, (edge e).1 = f + · simp only [hany_iff.mpr hex, ↓reduceIte]; obtain ⟨e, rfl⟩ := hex + rw [normalizeEmptyFactors_factorOf (factorOf := fun e => (edge e).1), + List.getD_eq_getElem _ _ + (by simp only [List.length_map, length_partialScheduleListOfFin]; exact (edge e).1.isLt)] + simp only [List.getElem_map, partialScheduleListOfFin, List.getElem_ofFn, completeLabels] + cases raw.2 (edge e).1 <;> simp only [Option.map_none, Option.map_some, Option.getD_none, + Option.getD_some, hw0, wordToSchedule_scheduleToWord] + · have hany : (edgesOfFin edge).any (fun e => decide (e.1 = f.val)) = false := + Bool.eq_false_iff.mpr fun h => hex (hany_iff.mp h) + rw [normalizeEmptyFactors_of_not_exists _ _ _ hex] + simp only [hany, Bool.false_eq_true, ↓reduceIte, hw0] + +/-- Empty-scope factor schedules are normalized to the constant zero group `⟨0, hr⟩`. -/ +theorem 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 _ => ⟨0, hr⟩ := by + rw [(constructedSchedules_eq_pass (Q := Q) hr edge C).2] + exact normalizeEmptyFactors_of_not_exists _ _ _ hf + +/-- `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 constructBalancedSchedules_score_le {E m n Q r : ℕ} (hr : 1 ≤ r) + (edge : Fin E → Fin m × Fin n) (C : ℕ) : + let a := constructedVarSchedule hr n m Q C (edgesOfFin edge) + let d := constructedFactorSchedule hr n m Q C (edgesOfFin edge) + potential (fun e => (a (edge e).2, d (edge e).1)) / ((E : ℚ) * C) + + (∑ t : Fin Q, potential (fun v => a v t)) / ((Q : ℚ) * n) ≤ + 𝔼 a' : Fin n → Fin Q → Fin r, 𝔼 d' : Fin m → Fin Q → Fin r, + (potential (fun e => (a' (edge e).2, d' (edge e).1)) / ((E : ℚ) * C) + + (∑ t : Fin Q, potential (fun v => a' v t)) / ((Q : ℚ) * n)) := by + dsimp only + let g₀ : Fin r := ⟨0, hr⟩; let : Nonempty (Fin r) := ⟨g₀⟩ + let slots : List (Fin n ⊕ Fin m) := + (List.ofFn fun v : Fin n => Sum.inl v) ++ (List.ofFn fun f : Fin m => Sum.inr f) + let raw := greedyLabelPass edge C (candidateScheduleList hr Q) slots + (fun _ => none, fun _ => none) + obtain ⟨hscore, hfill, -⟩ := greedyLabelPass_spec edge C (candidateScheduleList hr Q) + (mem_candidateScheduleList hr Q) slots (fun _ => none, fun _ => none) + have hvar (a' : Fin n → Fin Q → Fin r) : + completeLabels raw.1 a' = completeLabels raw.1 (fun _ _ => g₀) := funext fun v => by + obtain ⟨word, hw⟩ := hfill (.inl v) (List.mem_append_left _ (List.mem_ofFn.mpr ⟨v, rfl⟩)) + change raw.1 v = some word at hw; simp only [completeLabels, hw, Option.getD_some] + have hfac (d' : Fin m → Fin Q → Fin r) : + completeLabels raw.2 d' = completeLabels raw.2 (fun _ _ => g₀) := funext fun f => by + obtain ⟨word, hw⟩ := hfill (.inr f) (List.mem_append_right _ (List.mem_ofFn.mpr ⟨f, rfl⟩)) + change raw.2 f = some word at hw; simp only [completeLabels, hw, Option.getD_some] + have hout := normalizedPartialScore_eq_expect edge raw.1 raw.2 C + simp only [hvar, hfac, Fintype.expect_const, Fintype.card_fin] at hout + have hin := normalizedPartialScore_eq_expect (T := Fin Q) (G := Fin r) edge + (fun _ => none) (fun _ => none) C + simp only [completeLabels, Option.getD_none, Fintype.card_fin] at hin + obtain ⟨ha_eq, hd_eq⟩ := constructedSchedules_eq_pass (Q := Q) hr edge C + have hinc : (fun e => (constructedVarSchedule hr n m Q C (edgesOfFin edge) (edge e).2, + constructedFactorSchedule hr n m Q C (edgesOfFin edge) (edge e).1)) = + (fun e => (completeLabels raw.1 (fun _ _ => g₀) (edge e).2, + completeLabels raw.2 (fun _ _ => g₀) (edge e).1)) := funext fun e => by + rw [ha_eq, hd_eq, normalizeEmptyFactors_factorOf (factorOf := fun e => (edge e).1)] + rw [hinc, ha_eq, ← hin]; exact hout.symm.trans_le hscore + +/-- Under Lemma 4.5's degree hypotheses (`hb`, `hw`), `constructBalancedSchedules` achieves joint +normalized potential at most `2`. -/ +theorem 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} ≤ b) + (hw : ∀ e : Fin E, #{e' : Fin E | (edge e').1 = (edge e).1} ≤ w) + (hbw : 0 < b + w) : + let a := constructedVarSchedule hr n m Q (b + w) (edgesOfFin edge) + let d := constructedFactorSchedule hr n m Q (b + w) (edgesOfFin edge) + potential (fun e => (a (edge e).2, d (edge e).1)) / ((E : ℚ) * (b + w : ℕ)) + + (∑ t : Fin Q, potential (fun v => a v t)) / ((Q : ℚ) * n) ≤ 2 := by + dsimp only; let : Nonempty (Fin r) := ⟨⟨0, hr⟩⟩ + have hx : (0 : ℚ) < (E : ℚ) * (b + w : ℕ) := by positivity + have hy : (0 : ℚ) < (Q : ℚ) * n := by positivity + have h1 : (𝔼 a' : Fin n → Fin Q → Fin r, 𝔼 d' : Fin m → Fin Q → Fin r, + potential (fun e => (a' (edge e).2, d' (edge e).1)) / ((E : ℚ) * (b + w : ℕ))) ≤ 1 := by + simp_rw [div_eq_mul_inv, ← Finset.expect_mul, ← div_eq_mul_inv]; rw [div_le_one hx] + have h := expect_incidence_potential_le (L := Fin Q → Fin r) + (fun e => (edge e).2) (fun e => (edge e).1) hb hw + unfold incidenceLabel at h; simpa only [Fintype.card_fin, Nat.cast_add] using h + have h2 : (𝔼 a' : Fin n → Fin Q → Fin r, + (∑ t : Fin Q, potential (fun v => a' v t)) / ((Q : ℚ) * n)) ≤ 1 := by + simp_rw [div_eq_mul_inv, ← Finset.expect_mul, ← div_eq_mul_inv]; rw [div_le_one hy] + simpa only [Fintype.card_fin] using + (expect_group_potential_le (T := Fin Q) (V := Fin n) (G := Fin r)) + apply (constructBalancedSchedules_score_le hr edge (b + w)).trans + simp only [Finset.expect_add_distrib, Fintype.expect_const]; linarith + +/-- **Lemma 4.5 correctness for `constructBalancedSchedules` ([OpenAI2026ETH], 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. -/ +theorem 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} ≤ b) + (hw : ∀ e : Fin E, #{e' : Fin E | (edge e').1 = (edge e).1} ≤ w) + (hbw : 0 < b + w) + (hincidenceSize : 2 * (b + w) * ((r ^ Q) ^ 2) ^ 2 ≤ E) + (hgroupSize : 2 * Q * r ^ 2 ≤ n) : + let a := constructedVarSchedule hr n m Q (b + w) (edgesOfFin edge) + let d := constructedFactorSchedule hr n m Q (b + w) (edgesOfFin edge) + (∀ f : Fin m, (¬ ∃ e : Fin E, (edge e).1 = f) → d f = fun _ => ⟨0, hr⟩) ∧ + (∀ u : (Fin Q → Fin r) × (Fin Q → Fin r), + occupancy (fun e => (a (edge e).2, d (edge e).1)) u * (r ^ Q) ^ 2 ≤ 2 * E) ∧ + (∀ t : Fin Q, ∀ g : Fin r, + occupancy (fun v => a v t) g * r ≤ 2 * n) := by + dsimp only + have hD : 0 < (r ^ Q) ^ 2 := Nat.pow_pos (Nat.pow_pos hr) + have hE : 0 < E := + (by positivity : 0 < 2 * (b + w) * ((r ^ Q) ^ 2) ^ 2).trans_le hincidenceSize + have hcardB : Fintype.card ((Fin Q → Fin r) × (Fin Q → Fin r)) = (r ^ Q) ^ 2 := by + simp only [Fintype.card_prod, Fintype.card_fun, Fintype.card_fin, sq] + have hbounds := incidence_and_group_bounds + (fun e => (constructedVarSchedule hr n m Q (b + w) (edgesOfFin edge) (edge e).2, + constructedFactorSchedule hr n m Q (b + w) (edgesOfFin edge) (edge e).1)) + (fun t v => constructedVarSchedule hr n m Q (b + w) (edgesOfFin edge) v t) + (b + w) (by simp only [Fintype.card_fin]; exact hE) (by rw [hcardB]; exact hD) hbw + (by simp only [Fintype.card_fin]; omega) (by simp only [Fintype.card_fin]; omega) + (by simp only [Fintype.card_fin]; omega) + (by simpa only [Fintype.card_fin, hcardB] using hincidenceSize) + (by simpa only [Fintype.card_fin] using hgroupSize) + (by simpa only [Fintype.card_fin] using + constructBalancedSchedules_score_le_two hr hQ hn hE edge hb hw hbw) + refine ⟨fun f hf => constructedFactorSchedule_empty_factor hr edge (b + w) hf, + fun u => ?_, fun t g => ?_⟩ + · simpa only [hcardB, Fintype.card_fin] using hbounds.1 u + · simpa only [Fintype.card_fin] using hbounds.2 t g + +/-! ### Section 3: Hypergraph-valid bit-length bounds and native machine certificates -/ + +/-- Encoding of runtime inputs `((n, m, Q), (r, C), edges)` to `constructBalancedSchedules`. -/ +def encScheduleParams : ScheduleParams ↪ List Bool := + encPair (encPair encUnary (encPair encUnary encUnary)) + (encPair (encPair encNat encNat) (encList (encPair encNat encNat))) + +/-- Encoding of outer `IndexFold` accumulator `(ScheduleParams, (varSched, facSched))`. -/ +def encOuterAcc : + (ScheduleParams × (List (Option (List ℕ)) × List (Option (List ℕ)))) ↪ List Bool := + encPair encScheduleParams encPartialSchedules + +end Cslib.BalancedSchedules + +end + +public section + +namespace Cslib.BalancedSchedules + +open Finset Cslib.GenericRAM Turing.MultiTapeTM + +private theorem length_encNat_le_self (k : ℕ) : (encNat k).length ≤ k := by + rw [encNat_apply, Nat.size_eq_bits_len]; exact Nat.size_le_self k + +/-- Encoded bit-length bound for an incidence list `edges` with endpoints `< m` and `< n`. -/ +theorem length_encEdges_le_of_lt {n m : ℕ} {edges : List (ℕ × ℕ)} + (h : ∀ e ∈ edges, e.1 < m ∧ e.2 < n) : + (encList (encPair encNat encNat) edges).length ≤ + edges.length * (6 * (encNat (n + m)).length + 3) := by + rw [length_encList] + have hle : ∀ x ∈ edges.map (fun e => 2 * (encPair encNat encNat e).length + 1), + x ≤ 6 * (encNat (n + m)).length + 3 := by + intro x hx; obtain ⟨e, he, rfl⟩ := List.mem_map.mp hx; obtain ⟨hf, hv⟩ := h e he + have h1 := ComputableTidilyInO.length_encNat_mono (by omega : e.1 ≤ n + m) + have h2 := ComputableTidilyInO.length_encNat_mono (by omega : e.2 ≤ n + m) + rw [length_encPair]; omega + simpa only [List.length_map, smul_eq_mul] using + List.sum_le_length_nsmul _ (6 * (encNat (n + m)).length + 3) hle + +/-- 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 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, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) + (hw2 : ∀ o ∈ scheds.2, ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) : + (encPartialSchedules scheds).length ≤ + 2 * (n + m) * (2 * Q * (2 * (encNat r).length + 1) + 3) + 1 := by + have hlist {L : List (Option (List ℕ))} {N : ℕ} (hN : L.length = N) + (hw : ∀ o ∈ L, ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) : + (encList (encOption (encList encNat)) L).length ≤ + N * (2 * Q * (2 * (encNat r).length + 1) + 3) := by + rw [length_encList, ← hN] + have hle : ∀ x ∈ L.map (fun o => 2 * (encOption (encList encNat) o).length + 1), + x ≤ 2 * Q * (2 * (encNat r).length + 1) + 3 := by + intro x hx; obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hx; cases o with + | none => simp only [encOption_none, List.length_nil]; omega + | some w => + obtain ⟨hlw, hmw⟩ := hw (some w) ho w rfl + have hwl := length_encList_word_le hlw hmw + simp only [encOption_some, List.length_cons] + linarith [show 2 * Q * (2 * (encNat r).length + 1) = + 2 * (Q * (2 * (encNat r).length + 1)) by ring] + simpa only [List.length_map, smul_eq_mul] using + List.sum_le_length_nsmul _ (2 * Q * (2 * (encNat r).length + 1) + 3) hle + rw [encPartialSchedules, length_encPair] + have hb1 := hlist h1 hw1; have hb2 := hlist h2 hw2 + have hnm : 2 * n + m ≤ 2 * (n + m) := by omega + calc 2 * (encList (encOption (encList encNat)) scheds.1).length + 1 + + (encList (encOption (encList encNat)) scheds.2).length + ≤ 2 * (n * (2 * Q * (2 * (encNat r).length + 1) + 3)) + 1 + + m * (2 * Q * (2 * (encNat r).length + 1) + 3) := by omega + _ = (2 * n + m) * (2 * Q * (2 * (encNat r).length + 1) + 3) + 1 := by ring + _ ≤ 2 * (n + m) * (2 * Q * (2 * (encNat r).length + 1) + 3) + 1 := + Nat.add_le_add_right (Nat.mul_le_mul_right _ hnm) 1 + +/-- 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 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, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) + (hw2 : ∀ o ∈ scheds.2, ∀ w, o = some w → w.length = Q ∧ ∀ x ∈ w, x < max r 1) : + (encPair encNat encSlotSelectAcc + (IndexFold.run selectSlotStep j + (((n, Q), (r, C), edges), (slot, (scheds, none))))).length ≤ + 36 * (n + m + 1) * (Q + 1) * ((encNat r).length + 1) + + 28 * edges.length * ((encNat (n + m)).length + 1) + 9 * (encNat C).length + 60 := by + have hed := length_encEdges_le_of_lt hedges + have hsch := length_encPartialSchedules_le h1 h2 hw1 hw2 + have helen := length_encNat_le_self edges.length + have hnlen := length_encNat_le_self n; have hQlen := length_encNat_le_self Q + refine (length_encSlotSelectState_run_le n Q r C edges scheds slot hj).trans ?_ + simp only [encStreamSlotIn, encScoreParams, length_encPair, encUnary_apply, List.length_replicate, + encBool_apply, List.length_singleton] + have hcub : 16 * ((n + m) * Q * (encNat r).length) + 8 * ((n + m) * Q) + + 8 * (Q * (encNat r).length) + 34 * (n + m) + 14 * Q + 18 * (encNat r).length + 36 ≤ + 36 * (n + m + 1) * (Q + 1) * ((encNat r).length + 1) := by + have h0 := Nat.zero_le (20 * ((n + m) * Q * (encNat r).length) + 28 * ((n + m) * Q) + + 36 * ((n + m) * (encNat r).length) + 28 * (Q * (encNat r).length)) + linarith [show 36 * (n + m + 1) * (Q + 1) * ((encNat r).length + 1) = + (16 * ((n + m) * Q * (encNat r).length) + 8 * ((n + m) * Q) + + 8 * (Q * (encNat r).length) + 34 * (n + m) + 14 * Q + 18 * (encNat r).length + 36) + + (20 * ((n + m) * Q * (encNat r).length) + 28 * ((n + m) * Q) + + 36 * ((n + m) * (encNat r).length) + 28 * (Q * (encNat r).length)) + + 2 * (n + m) + 22 * Q + 18 * (encNat r).length by ring] + have hsch' : (encPartialSchedules scheds).length ≤ + 8 * ((n + m) * Q * (encNat r).length) + 4 * ((n + m) * Q) + 6 * (n + m) + 1 := by + linarith [hsch, show 2 * (n + m) * (2 * Q * (2 * (encNat r).length + 1) + 3) + 1 = + 8 * ((n + m) * Q * (encNat r).length) + 4 * ((n + m) * Q) + 6 * (n + m) + 1 by ring] + have hed' : 4 * (encList (encPair encNat encNat) edges).length + + 2 * (encNat edges.length).length ≤ 28 * edges.length * ((encNat (n + m)).length + 1) := by + linarith [hed, helen, show 28 * edges.length * ((encNat (n + m)).length + 1) = + 4 * (edges.length * (6 * (encNat (n + m)).length + 3)) + + 4 * (edges.length * (encNat (n + m)).length) + 16 * edges.length by ring, + Nat.zero_le (edges.length * (encNat (n + m)).length)] + linarith + +/-- 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 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) : + (encPair encNat encOuterAcc + (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) * ((encNat r).length + 1) + + 28 * edges.length * ((encNat (n + m)).length + 1) + 8 * (encNat C).length + 40 := by + let init := (List.replicate n (none : Option (List ℕ)), + List.replicate m (none : Option (List ℕ))) + have hp := run_greedySlotStepBody_params ((n, m, Q), (r, C), edges) init s + obtain ⟨h1, h2, hw1, hw2⟩ := run_greedySlotStepBody_wf n m Q r C edges s + have hsch := length_encPartialSchedules_le h1 h2 hw1 hw2 + have hed := length_encEdges_le_of_lt hedges + have hslen := (length_encNat_le_self s).trans hs + rw [IndexFold.length_run] + rcases hst : (IndexFold.run greedySlotStepBody s (((n, m, Q), (r, C), edges), init)).2 with + ⟨par, sc⟩ + have hpar : par = ((n, m, Q), (r, C), edges) := by simpa only [init, hst] using hp + have hsc_eq : sc = (IndexFold.run greedySlotStepBody s + (((n, m, Q), (r, C), edges), init)).2.2 := by simp only [hst] + subst hpar; rw [← hsc_eq] at hsch + simp only [encOuterAcc, encScheduleParams, length_encPair, encUnary_apply, List.length_replicate] + have hcub : 8 * ((n + m) * Q * (encNat r).length) + 4 * ((n + m) * Q) + + 16 * (n + m) + 4 * Q + 8 * (encNat r).length + 24 ≤ + 24 * (n + m + 1) * (Q + 1) * ((encNat r).length + 1) := by + have h0 := Nat.zero_le (16 * ((n + m) * Q * (encNat r).length) + 20 * ((n + m) * Q) + + 24 * ((n + m) * (encNat r).length) + 24 * (Q * (encNat r).length)) + linarith [show 24 * (n + m + 1) * (Q + 1) * ((encNat r).length + 1) = + (8 * ((n + m) * Q * (encNat r).length) + 4 * ((n + m) * Q) + + 16 * (n + m) + 4 * Q + 8 * (encNat r).length + 24) + + (16 * ((n + m) * Q * (encNat r).length) + 20 * ((n + m) * Q) + + 24 * ((n + m) * (encNat r).length) + 24 * (Q * (encNat r).length)) + + 8 * (n + m) + 20 * Q + 16 * (encNat r).length by ring] + have hsch' : (encPartialSchedules sc).length ≤ + 8 * ((n + m) * Q * (encNat r).length) + 4 * ((n + m) * Q) + 6 * (n + m) + 1 := by + linarith [hsch, show 2 * (n + m) * (2 * Q * (2 * (encNat r).length + 1) + 3) + 1 = + 8 * ((n + m) * Q * (encNat r).length) + 4 * ((n + m) * Q) + 6 * (n + m) + 1 by ring] + have hed' : 2 * (encList (encPair encNat encNat) edges).length ≤ + 28 * edges.length * ((encNat (n + m)).length + 1) := by + linarith [hed, show 28 * edges.length * ((encNat (n + m)).length + 1) = + 2 * (edges.length * (6 * (encNat (n + m)).length + 3)) + + 16 * (edges.length * (encNat (n + m)).length) + 22 * edges.length by ring, + Nat.zero_le (edges.length * (encNat (n + m)).length)] + linarith + +private theorem scheduleParams_parts_le (p : ScheduleParams) : + p.1.1 + p.1.2.1 ≤ (encScheduleParams p).length ∧ + p.1.2.2 ≤ (encScheduleParams p).length ∧ + (encNat p.2.1.1).length ≤ (encScheduleParams p).length ∧ + (encNat p.2.1.2).length ≤ (encScheduleParams p).length ∧ + (encList (encPair encNat encNat) p.2.2).length ≤ (encScheduleParams p).length := by + simp only [encScheduleParams, length_encPair, encUnary_apply, List.length_replicate] + exact ⟨by omega, by omega, by omega, by omega, by omega⟩ + +/-- 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 length_encOuterState_run_le (p : ScheduleParams) {s : ℕ} (hs : s ≤ p.1.1 + p.1.2.1) : + (encPair encNat encOuterAcc + (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 := by + let L := (encScheduleParams p).length; have hparts := scheduleParams_parts_le p + let init := (List.replicate p.1.1 (none : Option (List ℕ)), + List.replicate p.1.2.1 (none : Option (List ℕ))) + have hp := run_greedySlotStepBody_params p init s + obtain ⟨h1, h2, hw1, hw2⟩ := + run_greedySlotStepBody_wf p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2 s + have hsch := length_encPartialSchedules_le h1 h2 hw1 hw2 + have hslen : (encNat s).length ≤ L := (length_encNat_le_self s).trans (hs.trans hparts.1) + have hprod : 2 * (p.1.1 + p.1.2.1) * (2 * p.1.2.2 * (2 * (encNat p.2.1.1).length + 1) + 3) ≤ + 2 * L * (2 * L * (2 * L + 1) + 3) := + Nat.mul_le_mul (Nat.mul_le_mul_left 2 hparts.1) + (Nat.add_le_add_right (Nat.mul_le_mul (Nat.mul_le_mul_left 2 hparts.2.1) + (Nat.add_le_add_right (Nat.mul_le_mul_left 2 hparts.2.2.1) 1)) 3) + rw [IndexFold.length_run] + rcases hst : (IndexFold.run greedySlotStepBody s (p, init)).2 with ⟨par, sc⟩ + have hpar : par = p := by simpa only [init, hst] using hp + have hsc_eq : sc = (IndexFold.run greedySlotStepBody s (p, init)).2.2 := by simp only [hst] + subst hpar; rw [← hsc_eq] at hsch + simp only [encOuterAcc, length_encPair] + change 2 * (encNat s).length + 1 + (2 * L + 1 + (encPartialSchedules sc).length) ≤ + 8 * L ^ 3 + 4 * L ^ 2 + 10 * L + 3 + linarith [hprod, show 2 * L * (2 * L * (2 * L + 1) + 3) = 8 * L ^ 3 + 4 * L ^ 2 + 6 * L by ring] + +/-- `slotOfIndex` is computable in polynomial time. -/ +@[fun_prop] theorem computableInPolyTime_slotOfIndex : + ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ => slotOfIndex p.1.1 p.1.2 p.2) + (encPair (encPair encUnary encUnary) encNat) (encOption (encPair encBool encUnary)) := by + have hsCap : ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ => min (p.1.1 + p.1.2) p.2) + (encPair (encPair encUnary encUnary) encNat) encUnary := by fun_prop + refine .of_tidy ?_ + have hsCapT := hsCap.tidy; let eIn := encPair (encPair encUnary encUnary) encNat + have hnBin : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.1) eIn encNat := + ComputableTidilyInPolyTime.unary_to_binary.comp (by fun_prop) + have hnmBin : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.1 + p.1.2) eIn encNat := + ComputableTidilyInPolyTime.unary_to_binary.comp (by fun_prop) + have hsBin : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.2) eIn encNat := by fun_prop + have hlt1 := ComputableTidilyInPolyTime.binary_lt' hsBin hnBin + have hlt2 := ComputableTidilyInPolyTime.binary_lt' hsBin hnmBin + have hb1 : ComputableTidilyInPolyTime + (fun p : (ℕ × ℕ) × ℕ => (some (false, min (p.1.1 + p.1.2) p.2) : Option (Bool × ℕ))) + eIn (encOption (encPair encBool encUnary)) := by fun_prop + have hb2 : ComputableTidilyInPolyTime + (fun p : (ℕ × ℕ) × ℕ => (some (true, min (p.1.1 + p.1.2) p.2 - p.1.1) : Option (Bool × ℕ))) + eIn (encOption (encPair encBool encUnary)) := by fun_prop + convert ComputableTidilyInPolyTime.ite_decide hlt1 hb1 + (ComputableTidilyInPolyTime.ite_decide hlt2 hb2 (ComputableTidilyInPolyTime.const none)) using 1 + funext p; unfold slotOfIndex + by_cases h1 : p.2 < p.1.1 + · simp only [h1, ↓reduceIte] + · by_cases h2 : p.2 < p.1.1 + p.1.2 <;> simp only [h1, h2, ↓reduceIte] + +private abbrev OuterAcc : Type := + ScheduleParams × (List (Option (List ℕ)) × List (Option (List ℕ))) +private abbrev OuterSt : Type := ℕ × OuterAcc +private abbrev encOuterSt : OuterSt ↪ List Bool := encPair encNat encOuterAcc +private abbrev encSlotOpt : Option (Bool × ℕ) ↪ List Bool := encOption (encPair encBool encUnary) +private abbrev encOuterSlot : (OuterSt × (Bool × ℕ)) ↪ List Bool := + encPair encOuterSt (encPair encBool encUnary) +private abbrev encFinIn : ((OuterSt × (Bool × ℕ)) × List ℕ) ↪ List Bool := + encPair encOuterSlot (encList encNat) +private abbrev encOutWords : (List (List ℕ) × List (List ℕ)) ↪ List Bool := + encPair (encList (encList encNat)) (encList (encList encNat)) + +private theorem computableInPolyTime_pendingSlotOfState : + ComputableInPolyTime pendingSlotOfState encOuterSt encSlotOpt := by + have hsl : ComputableInPolyTime + (fun st : OuterSt => slotOfIndex st.2.1.1.1 st.2.1.1.2.1 st.1) encOuterSt encSlotOpt := + computableInPolyTime_slotOfIndex.comp + (show ComputableInPolyTime (fun st : OuterSt => ((st.2.1.1.1, st.2.1.1.2.1), st.1)) + encOuterSt (encPair (encPair encUnary encUnary) encNat) from + .of_tidy (by unfold encOuterSt encOuterAcc encScheduleParams; fun_prop)) + have hrd := computableInPolyTime_readSlotSchedule.tidy; refine .of_tidy ?_ + have hslT := hsl.tidy; unfold pendingSlotOfState encSlotOpt + refine ComputableTidilyInPolyTime.optionElimWithInput hslT + (ComputableTidilyInPolyTime.const none) ?_ + have his : ComputableTidilyInPolyTime + (fun q : OuterSt × (Bool × ℕ) => (readSlotSchedule q.2 q.1.2.2).isSome) + (encPair encOuterSt (encPair encBool encUnary)) encBool := + ComputableTidilyInPolyTime.optionIsSome (hrd.comp + (show ComputableTidilyInPolyTime (fun q : OuterSt × (Bool × ℕ) => (q.2, q.1.2.2)) + (encPair encOuterSt (encPair encBool encUnary)) _ by + unfold encOuterSt encOuterAcc; fun_prop)) + exact his.cond (ComputableTidilyInPolyTime.const none) (by fun_prop) + +private def streamSlotInOfOuter (q : OuterSt × (Bool × ℕ)) : StreamSlotIn := + (((q.1.2.1.1.1, q.1.2.1.1.2.2), q.1.2.1.2), (q.2, q.1.2.2)) + +private def finishGreedySlotStep (q : (OuterSt × (Bool × ℕ)) × List ℕ) : OuterAcc := + (q.1.1.2.1, updateSlotSchedules q.1.2 (some q.2) q.1.1.2.2) + +private theorem computableInPolyTime_streamSlotInOfOuter : + ComputableInPolyTime streamSlotInOfOuter encOuterSlot encStreamSlotIn := by + refine .of_tidy ?_ + unfold streamSlotInOfOuter encOuterSlot encOuterSt encOuterAcc encScheduleParams encStreamSlotIn + encScoreParams + fun_prop + +private theorem computableInPolyTime_finishGreedySlotStep : + ComputableInPolyTime finishGreedySlotStep encFinIn encOuterAcc := by + have hupd := computableInPolyTime_updateSlotSchedules.comp + (show ComputableInPolyTime (fun q : _ => ((q.1.2, some q.2), q.1.1.2.2)) encFinIn + (encPair (encPair (encPair encBool encUnary) (encOption (encList encNat))) + encPartialSchedules) by + refine .of_tidy ?_; unfold encFinIn encOuterSlot encOuterSt encOuterAcc; fun_prop) + exact (show ComputableInPolyTime (fun q : _ => q.1.1.2.1) encFinIn encScheduleParams by + refine .of_tidy ?_; unfold encFinIn encOuterSlot encOuterSt encOuterAcc; fun_prop).prod hupd + +private noncomputable def mkGreedyStepCert + (cPend : NativeCertificate pendingSlotOfState encOuterSt encSlotOpt) + (cIn : NativeCertificate streamSlotInOfOuter encOuterSlot encStreamSlotIn) + (cSlot : 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 (encList encNat)) + (cFin : NativeCertificate finishGreedySlotStep encFinIn encOuterAcc) : + NativeCertificate greedySlotStepBody encOuterSt encOuterAcc := + let cId : NativeCertificate id encOuterSlot encOuterSlot := + NativeCertificate.linear (ComputableInO.of_linear (.of_eq fun _ => rfl)) + NativeCertificate.option cPend (NativeCertificate.linear (ComputableInO.snd encNat encOuterAcc)) + ((cFin.comp (cId.prod (cSlot.comp cIn))).congr fun _ => rfl) + +private noncomputable def greedySlotStepBodyCertificate : + NativeCertificate greedySlotStepBody encOuterSt encOuterAcc := + mkGreedyStepCert + (NativeCertificate.ofPolyTime computableInPolyTime_pendingSlotOfState) + (NativeCertificate.ofPolyTime computableInPolyTime_streamSlotInOfOuter) + streamBestSlotCertificate + (NativeCertificate.ofPolyTime computableInPolyTime_finishGreedySlotStep) + +private def outerCount (p : ScheduleParams) : ℕ := p.1.1 + p.1.2.1 + +private def outerInit (p : ScheduleParams) : OuterAcc := + (p, (List.replicate p.1.1 none, List.replicate p.1.2.1 none)) + +private def finalizeBalancedSchedules (q : OuterAcc) : List (List ℕ) × List (List ℕ) := + let Q := q.1.1.2.2; let edges := q.1.2.2 + (q.2.1.map fun o => o.getD (List.replicate Q 0), + normalizeEmptyFactorSchedules Q edges (q.2.2.map fun o => o.getD (List.replicate Q 0))) + +private theorem computableInPolyTime_outerCount : + ComputableInPolyTime outerCount encScheduleParams encNat := by + refine .of_tidy ?_; unfold outerCount encScheduleParams + exact ComputableTidilyInPolyTime.unary_to_binary.comp (by fun_prop) + +private theorem computableInPolyTime_outerInit : + ComputableInPolyTime outerInit encScheduleParams encOuterAcc := by + refine .of_tidy ?_; unfold outerInit encOuterAcc encScheduleParams encPartialSchedules; fun_prop + +private theorem computableInPolyTime_finalizeBalancedSchedules : + ComputableInPolyTime finalizeBalancedSchedules encOuterAcc encOutWords := by + refine .of_tidy ?_ + unfold finalizeBalancedSchedules normalizeEmptyFactorSchedules encOuterAcc encScheduleParams + encPartialSchedules encOutWords + let eEdges := encList (encPair encNat encNat) + let ePar := encPair (encPair encUnary (encPair encUnary encUnary)) + (encPair (encPair encNat encNat) eEdges) + let eOpt := encOption (encList encNat) + let eIn := encPair ePar (encPair (encList eOpt) (encList eOpt)) + have hvar : ComputableTidilyInPolyTime + (fun q : OuterAcc => q.2.1.map fun o => o.getD (List.replicate q.1.1.2.2 0)) + eIn (encList (encList encNat)) := by fun_prop + have hraw2 : ComputableTidilyInPolyTime + (fun q : OuterAcc => q.2.2.map fun o => o.getD (List.replicate q.1.1.2.2 0)) + eIn (encList (encList encNat)) := by fun_prop + have hfac : ComputableTidilyInPolyTime + (fun q : OuterAcc => + (List.range (q.2.2.map fun o => o.getD (List.replicate q.1.1.2.2 0)).length).map fun f => + if q.1.2.2.any (fun e => decide (e.1 = f)) then + (q.2.2.map fun o => o.getD (List.replicate q.1.1.2.2 0)).getD f [] + else List.replicate q.1.1.2.2 0) + eIn (encList (encList encNat)) := by + refine ComputableTidilyInPolyTime.mapWithInput + (ComputableTidilyInPolyTime.range.comp + ((ComputableTidilyInPolyTime.length (encList encNat)).comp hraw2)) ?_ + have hany : ComputableTidilyInPolyTime + (fun r : OuterAcc × ℕ => r.1.1.2.2.any fun e => decide (e.1 = r.2)) + (encPair eIn encUnary) encBool := + ComputableTidilyInPolyTime.anyWithInput (by fun_prop) + (ComputableTidilyInPolyTime.decide_eq' (by fun_prop) + (ComputableTidilyInPolyTime.unary_to_binary.comp (by fun_prop))) + have hthen : ComputableTidilyInPolyTime + (fun r : OuterAcc × ℕ => + (r.1.2.2.map fun o => o.getD (List.replicate r.1.1.1.2.2 0)).getD r.2 []) + (encPair eIn encUnary) (encList encNat) := + (ComputableTidilyInPolyTime.listGetD []).comp + ((hraw2.comp (ComputableTidilyInPolyTime.fst _ _)).prod + (ComputableTidilyInPolyTime.snd _ _)) + exact hany.cond hthen (by fun_prop) + exact hvar.prod hfac + +private noncomputable def mkOuterAccCert + (cCnt : NativeCertificate outerCount encScheduleParams encNat) + (cInit : NativeCertificate outerInit encScheduleParams encOuterAcc) + (cStep : NativeCertificate greedySlotStepBody encOuterSt encOuterAcc) : + NativeCertificate + (fun p : ScheduleParams => (IndexFold.run greedySlotStepBody (outerCount p) (outerInit p)).2) + encScheduleParams encOuterAcc := + NativeCertificate.snd (IndexFold.certificate cCnt cInit cStep) + +private noncomputable def mkConstructCert + (cAcc : NativeCertificate + (fun p : ScheduleParams => (IndexFold.run greedySlotStepBody (outerCount p) (outerInit p)).2) + encScheduleParams encOuterAcc) + (cFinal : NativeCertificate finalizeBalancedSchedules encOuterAcc encOutWords) : + 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 (encPair (encList (encList encNat)) (encList (encList encNat))) := + (cFinal.comp cAcc).congr fun ⟨⟨n, m, Q⟩, ⟨r, C⟩, edges⟩ => by + have hp := run_greedySlotStepBody_params ((n, m, Q), (r, C), edges) + (List.replicate n none, List.replicate m none) (n + m) + dsimp only [Function.comp_apply, outerCount, outerInit, finalizeBalancedSchedules, + constructBalancedSchedules, greedySchedulePass] + rw [hp] + +/-- Uniform native machine certificate for `greedySchedulePass`. -/ +noncomputable def greedySchedulePassCertificate : + 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 := + NativeCertificate.snd (mkOuterAccCert + (NativeCertificate.ofPolyTime computableInPolyTime_outerCount) + (NativeCertificate.ofPolyTime computableInPolyTime_outerInit) + greedySlotStepBodyCertificate) + +/-- Uniform native machine certificate for `constructBalancedSchedules` ([OpenAI2026ETH], +Lemma 4.5, p. 31). -/ +noncomputable def constructBalancedSchedulesCertificate : + 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 (encPair (encList (encList encNat)) (encList (encList encNat))) := + mkConstructCert + (mkOuterAccCert + (NativeCertificate.ofPolyTime computableInPolyTime_outerCount) + (NativeCertificate.ofPolyTime computableInPolyTime_outerInit) + greedySlotStepBodyCertificate) + (NativeCertificate.ofPolyTime computableInPolyTime_finalizeBalancedSchedules) + +private theorem ofPolyTime_exists_bound {α β : Type} {f : α → β} {ea : α ↪ List Bool} + {eb : β ↪ List Bool} (hf : ComputableInPolyTime f ea eb) : + ∃ (c d : ℕ), ∀ (x : α), (NativeCertificate.ofPolyTime hf).time x + + (NativeCertificate.ofPolyTime hf).space x ≤ c * ((ea x).length + 1) ^ d := + ((NativeCertificate.ofPolyTime_isPolynomial hf).1.add + (NativeCertificate.ofPolyTime_isPolynomial hf).2).exists_le + +private theorem pendingSlotOfState_snd_le {st : OuterSt} {slot : Bool × ℕ} + (h : pendingSlotOfState st = some slot) : slot.2 ≤ st.2.1.1.1 + st.2.1.1.2.1 := by + unfold pendingSlotOfState slotOfIndex at h + by_cases h1 : st.1 < st.2.1.1.1 + · simp only [h1, ↓reduceIte, Option.elim_some] at h; split_ifs at h + injection h with h'; subst h'; exact min_le_left _ _ + · by_cases h2 : st.1 < st.2.1.1.1 + st.2.1.1.2.1 + · simp only [h1, h2, ↓reduceIte, Option.elim_some] at h; split_ifs at h + injection h with h'; subst h'; exact (Nat.sub_le _ _).trans (min_le_left _ _) + · simp only [h1, h2, ↓reduceIte, Option.elim_none] at h; cases h + +private theorem mkGreedyStepCert_bounds + (cPend : NativeCertificate pendingSlotOfState encOuterSt encSlotOpt) + (cIn : NativeCertificate streamSlotInOfOuter encOuterSlot encStreamSlotIn) + (cSlot : 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 (encList encNat)) + (cFin : NativeCertificate finishGreedySlotStep encFinIn encOuterAcc) + {cP dP cS dS cF dF : ℕ} {pSlot : ℕ → ℕ} + (hPend : ∀ st, cPend.time st + cPend.space st ≤ cP * ((encOuterSt st).length + 1) ^ dP) + (hIn : ∀ q, cIn.time q + cIn.space q ≤ cS * ((encOuterSlot q).length + 1) ^ dS) + (hpSlot : Cslib.PolynomiallyBounded pSlot) (hmSlot : Monotone pSlot) + (hSlot : ∀ a : StreamSlotIn, + cSlot.time a ≤ (a.1.2.1.1 ^ a.1.1.2 + 1) * pSlot (encStreamSlotIn a).length ∧ + cSlot.space a ≤ pSlot (encStreamSlotIn a).length) + (hFin : ∀ qc, cFin.time qc + cFin.space qc ≤ cF * ((encFinIn qc).length + 1) ^ dF) : + ∃ pStep : ℕ → ℕ, Cslib.PolynomiallyBounded pStep ∧ + ∀ p : ScheduleParams, ∀ s ≤ outerCount p, + let st := IndexFold.run greedySlotStepBody s (outerInit p) + (mkGreedyStepCert cPend cIn cSlot cFin).time st ≤ + (p.2.1.1 ^ p.1.2.2 + 1) * pStep (encScheduleParams p).length ∧ + (mkGreedyStepCert cPend cIn cSlot cFin).space st ≤ + pStep (encScheduleParams p).length := by + let pPend (n : ℕ) := cP * (n + 1) ^ dP; let pIn (n : ℕ) := cS * (n + 1) ^ dS + let pFin (n : ℕ) := cF * (n + 1) ^ dF + let bOuter (L : ℕ) := 8 * L ^ 3 + 4 * L ^ 2 + 10 * L + 3 + let bPair (L : ℕ) := 2 * bOuter L + L + 4; let bSlotIn (L : ℕ) := bOuter L + 28 * L + 20 + let bFinIn (L : ℕ) := 2 * bPair L + 4 * L ^ 2 + 2 * L + 2 + let pOver (L : ℕ) := 2 * pPend (bOuter L) + 2 * bOuter L + bPair L + pIn (bPair L) + + pFin (bFinIn L) + let pStep (L : ℕ) := pOver L + pSlot (bSlotIn L) + have hpStep : Cslib.PolynomiallyBounded pStep := by + dsimp only [pStep, pOver, bFinIn, bSlotIn, bPair, bOuter, pPend, pIn, pFin]; fun_prop + refine ⟨pStep, hpStep, fun p s hs => ?_⟩ + dsimp only; set L := (encScheduleParams p).length; set rq := p.2.1.1 ^ p.1.2.2 + set runAt := IndexFold.run greedySlotStepBody s (outerInit p) + have hparts := scheduleParams_parts_le p + have hstL : (encOuterSt runAt).length ≤ bOuter L := length_encOuterState_run_le p hs + have hpend : cPend.time runAt + cPend.space runAt ≤ pPend (bOuter L) := + (hPend runAt).trans + (Nat.mul_le_mul_left cP (Nat.pow_le_pow_left (Nat.add_le_add_right hstL 1) dP)) + simp only [mkGreedyStepCert, NativeCertificate.option_time, NativeCertificate.option_space, + NativeCertificate.linear_time, NativeCertificate.linear_space] + cases hps : pendingSlotOfState runAt with + | none => + simp only [Option.elim_none] + have hnT : 2 * cPend.time runAt + (encOuterSt runAt).length + (encOuterSt runAt).length ≤ + pStep L := by dsimp only [pStep, pOver]; omega + exact ⟨hnT.trans (Nat.le_mul_of_pos_left _ (by omega : 1 ≤ rq + 1)), + by dsimp only [pStep, pOver]; omega⟩ + | some slot => + simp only [Option.elim_some] + have hp_eq : runAt.2.1 = p := + run_greedySlotStepBody_params p (List.replicate p.1.1 none, List.replicate p.1.2.1 none) s + have hsl_le : slot.2 ≤ L := by + have := pendingSlotOfState_snd_le hps; rw [hp_eq] at this; exact this.trans hparts.1 + have hslotL : (encPair encBool encUnary slot).length = slot.2 + 3 := by + simp only [length_encPair, encBool_apply, List.length_singleton, encUnary_apply, + List.length_replicate]; omega + let q := (runAt, slot) + have hqL : (encOuterSlot q).length ≤ bPair L := by + unfold encOuterSlot; rw [length_encPair, hslotL]; dsimp only [q, bPair]; omega + have hIn_q : cIn.time q + cIn.space q ≤ pIn (bPair L) := + (hIn q).trans (Nat.mul_le_mul_left cS (Nat.pow_le_pow_left (Nat.add_le_add_right hqL 1) dS)) + let a := streamSlotInOfOuter q + have hSlotInL : (encStreamSlotIn a).length ≤ bSlotIn L := by + obtain ⟨h1, h2, hw1, hw2⟩ := + run_greedySlotStepBody_wf p.1.1 p.1.2.1 p.1.2.2 p.2.1.1 p.2.1.2 p.2.2 s + have hsch : (encPartialSchedules runAt.2.2).length ≤ bOuter L := by + have hsch0 := length_encPartialSchedules_le h1 h2 hw1 hw2 + have hp3 : 2 * (p.1.1 + p.1.2.1) * (2 * p.1.2.2 * (2 * (encNat p.2.1.1).length + 1) + 3) ≤ + 2 * L * (2 * L * (2 * L + 1) + 3) := + Nat.mul_le_mul (Nat.mul_le_mul_left 2 hparts.1) + (Nat.add_le_add_right (Nat.mul_le_mul (Nat.mul_le_mul_left 2 hparts.2.1) + (Nat.add_le_add_right (Nat.mul_le_mul_left 2 hparts.2.2.1) 1)) 3) + dsimp only [runAt, outerInit, bOuter] + linarith [hsch0, hp3, + show 2 * L * (2 * L * (2 * L + 1) + 3) = 8 * L ^ 3 + 4 * L ^ 2 + 6 * L by ring] + simp only [a, streamSlotInOfOuter, q, hp_eq, encStreamSlotIn, encScoreParams, length_encPair, + encUnary_apply, List.length_replicate, encBool_apply, List.length_singleton] + dsimp only [bSlotIn]; omega + have hSlot_a := hSlot a + have hrq_eq : a.1.2.1.1 ^ a.1.1.2 = rq := by simp only [a, streamSlotInOfOuter, q, hp_eq, rq] + have hSlotT : cSlot.time a ≤ (rq + 1) * pSlot (bSlotIn L) := by + rw [← hrq_eq]; exact hSlot_a.1.trans (Nat.mul_le_mul_left _ (hmSlot hSlotInL)) + have hSlotS : cSlot.space a ≤ pSlot (bSlotIn L) := hSlot_a.2.trans (hmSlot hSlotInL) + let chosen := 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 + have hchL : (encList encNat chosen).length ≤ 4 * L ^ 2 + 2 * L + 1 := by + have hw := length_encList_word_le (Q := a.1.1.2) (r := a.1.2.1.1) (w := chosen) + (length_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) + (fun _ hx => mem_streamBestSlotLabel_lt_max 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 hx) + have hq1 : a.1.1.2 = p.1.2.2 := by simp only [a, streamSlotInOfOuter, q, hp_eq] + have hq2 : a.1.2.1.1 = p.2.1.1 := by simp only [a, streamSlotInOfOuter, q, hp_eq] + have hp2 : 2 * p.1.2.2 * (2 * (encNat p.2.1.1).length + 1) ≤ 2 * L * (2 * L + 1) := + Nat.mul_le_mul (Nat.mul_le_mul_left 2 hparts.2.1) + (Nat.add_le_add_right (Nat.mul_le_mul_left 2 hparts.2.2.1) 1) + rw [hq1, hq2] at hw + linarith [hw, hp2, show 2 * L * (2 * L + 1) = 4 * L ^ 2 + 2 * L by ring] + have hFinL : (encFinIn (q, chosen)).length ≤ bFinIn L := by + unfold encFinIn; rw [length_encPair]; dsimp only [bFinIn]; omega + have hFin_qc : cFin.time (q, chosen) + cFin.space (q, chosen) ≤ pFin (bFinIn L) := + (hFin (q, chosen)).trans + (Nat.mul_le_mul_left cF (Nat.pow_le_pow_left (Nat.add_le_add_right hFinL 1) dF)) + refine ⟨?_, ?_⟩ + · simp only [NativeCertificate.congr_time, NativeCertificate.comp_time, + NativeCertificate.prod_time, NativeCertificate.linear_time, id_eq] + change 2 * cPend.time runAt + (encOuterSt runAt).length + + (((encOuterSlot q).length + (cIn.time q + cSlot.time a)) + cFin.time (q, chosen)) ≤ + (rq + 1) * pStep L + have hover : 2 * cPend.time runAt + (encOuterSt runAt).length + + (encOuterSlot q).length + cIn.time q + cFin.time (q, chosen) ≤ pOver L := by + dsimp only [pOver]; omega + calc 2 * cPend.time runAt + (encOuterSt runAt).length + + (((encOuterSlot q).length + (cIn.time q + cSlot.time a)) + cFin.time (q, chosen)) + ≤ pOver L + (rq + 1) * pSlot (bSlotIn L) := by omega + _ ≤ (rq + 1) * pOver L + (rq + 1) * pSlot (bSlotIn L) := + Nat.add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos rq)) _ + _ = (rq + 1) * pStep L := by dsimp only [pStep]; ring + · simp only [NativeCertificate.congr_space, NativeCertificate.comp_space, + NativeCertificate.prod_space, NativeCertificate.linear_space, id_eq] + change 2 * cPend.space runAt + (encOuterSt runAt).length + + (((encOuterSlot q).length + (cIn.space q + cSlot.space a)) + cFin.space (q, chosen)) ≤ + pStep L + dsimp only [pStep, pOver]; omega + +private theorem mkOuterAccCert_bounds + (cCnt : NativeCertificate outerCount encScheduleParams encNat) + (cInit : NativeCertificate outerInit encScheduleParams encOuterAcc) + (cStep : NativeCertificate greedySlotStepBody encOuterSt encOuterAcc) + {cC dC cI dI : ℕ} {pStep : ℕ → ℕ} + (hCnt : ∀ p, cCnt.time p + cCnt.space p ≤ cC * ((encScheduleParams p).length + 1) ^ dC) + (hInit : ∀ p, cInit.time p + cInit.space p ≤ cI * ((encScheduleParams p).length + 1) ^ dI) + (hpStep : Cslib.PolynomiallyBounded pStep) + (hStep : ∀ p : ScheduleParams, ∀ s ≤ outerCount p, + let st := IndexFold.run greedySlotStepBody s (outerInit p) + cStep.time st ≤ (p.2.1.1 ^ p.1.2.2 + 1) * pStep (encScheduleParams p).length ∧ + cStep.space st ≤ pStep (encScheduleParams p).length) : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ Monotone poly ∧ + ∀ p : ScheduleParams, + (mkOuterAccCert cCnt cInit cStep).time p ≤ + (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length ∧ + (mkOuterAccCert cCnt cInit cStep).space p ≤ poly (encScheduleParams p).length := by + let pCnt (n : ℕ) := cC * (n + 1) ^ dC; let pInit (n : ℕ) := cI * (n + 1) ^ dI + let bOuter (L : ℕ) := 8 * L ^ 3 + 4 * L ^ 2 + 10 * L + 3 + let rawPoly (L : ℕ) := pCnt L + L + pInit L + (L + 1) * (2 * bOuter L + 2 * (L + 1) ^ 2 + pStep L) + have hraw : Cslib.PolynomiallyBounded rawPoly := by + dsimp only [rawPoly, bOuter, pCnt, pInit]; fun_prop + obtain ⟨cP, dP, hleP⟩ := (PolyBounded.of_polynomiallyBounded id hraw).exists_le + let poly (n : ℕ) := cP * (n + 1) ^ dP + refine ⟨poly, by dsimp only [poly]; fun_prop, + fun _ _ hxy => Nat.mul_le_mul_left cP (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) dP), + fun p => ?_⟩ + let L := (encScheduleParams p).length; let K := outerCount p; let rq := p.2.1.1 ^ p.1.2.2 + have hpolyL : rawPoly L ≤ poly L := hleP L + have hKL : K ≤ L := (scheduleParams_parts_le p).1 + have hlIdx : (encNat K).length ≤ L := (length_encNat_le_self K).trans hKL + let runAt (s : ℕ) := IndexFold.run greedySlotStepBody s (outerInit p) + have hbOuter (s : ℕ) (hs : s ≤ K) : (encOuterSt (runAt s)).length ≤ bOuter L := + length_encOuterState_run_le p hs + let rstep := IndexFold.roundCertificate cStep; let initPair := (0, outerInit p) + let M := NativeCertificate.maxStateLength encOuterSt (IndexFold.step greedySlotStepBody) K + initPair + let RT := NativeCertificate.maxRoundTime rstep K initPair + let RS := NativeCertificate.maxRoundSpace rstep K initPair + have hmaxS : M ≤ bOuter L := NativeCertificate.maxStateLength_le _ _ _ _ hbOuter + have hcnt_p : cCnt.time p + cCnt.space p ≤ pCnt L := hCnt p + have hinit_p : cInit.time p + cInit.space p ≤ pInit L := hInit p + have hsqK : ((encNat K).length + 1) ^ 2 ≤ (L + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + refine ⟨?_, ?_⟩ + · have hmaxRT : RT ≤ bOuter L + (L + 1) ^ 2 + (rq + 1) * pStep L := by + refine NativeCertificate.maxRoundTime_le _ _ _ fun s hs => ?_ + have hs_len : (encNat (runAt s).1).length ≤ L := by + rw [IndexFold.run_index]; exact (ComputableTidilyInO.length_encNat_mono hs).trans hlIdx + have hsq := Nat.pow_le_pow_left (Nat.add_le_add_right hs_len 1) 2 + have hstL := hbOuter s hs + have hcbT : cStep.time (runAt s) ≤ (rq + 1) * pStep L := (hStep p s hs).1 + change (encOuterSt (runAt s)).length + ((encNat (runAt s).1).length + 1) ^ 2 + + cStep.time (runAt s) ≤ _ + omega + have hround : RT + M + ((encNat K).length + 1) ^ 2 ≤ + (rq + 1) * (2 * bOuter L + 2 * (L + 1) ^ 2 + pStep L) := + calc RT + M + ((encNat K).length + 1) ^ 2 + ≤ (2 * bOuter L + 2 * (L + 1) ^ 2) + (rq + 1) * pStep L := by omega + _ ≤ (rq + 1) * (2 * bOuter L + 2 * (L + 1) ^ 2) + (rq + 1) * pStep L := + Nat.add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos rq)) _ + _ = (rq + 1) * (2 * bOuter L + 2 * (L + 1) ^ 2 + pStep L) := by ring + have hmul := Nat.mul_le_mul (Nat.add_le_add_right hKL 1) hround + calc (mkOuterAccCert cCnt cInit cStep).time p + = cCnt.time p + (L + cInit.time p) + + (K + 1) * (RT + M + ((encNat K).length + 1) ^ 2) := rfl + _ ≤ (pCnt L + L + pInit L) + + (L + 1) * ((rq + 1) * (2 * bOuter L + 2 * (L + 1) ^ 2 + pStep L)) := by omega + _ ≤ (rq + 1) * (pCnt L + L + pInit L) + + (L + 1) * ((rq + 1) * (2 * bOuter L + 2 * (L + 1) ^ 2 + pStep L)) := + Nat.add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos rq)) _ + _ = (rq + 1) * rawPoly L := by dsimp only [rawPoly]; ring + _ ≤ (rq + 1) * poly L := Nat.mul_le_mul_left _ hpolyL + · have hmaxRS : RS ≤ bOuter L + (L + 1) + pStep L := by + refine NativeCertificate.maxRoundSpace_le _ _ _ fun s hs => ?_ + have hs_len : (encNat (runAt s).1).length ≤ L := by + rw [IndexFold.run_index]; exact (ComputableTidilyInO.length_encNat_mono hs).trans hlIdx + have hstL := hbOuter s hs + have hcbS : cStep.space (runAt s) ≤ pStep L := (hStep p s hs).2 + change (encOuterSt (runAt s)).length + ((encNat (runAt s).1).length + 1) + + cStep.space (runAt s) ≤ _ + omega + have hlin_sq : L + 1 ≤ (L + 1) ^ 2 := by rw [sq]; exact Nat.le_mul_self _ + have h1 := Nat.mul_le_mul_right (2 * bOuter L + 2 * (L + 1) ^ 2 + pStep L) + (by omega : 1 ≤ L + 1) + calc (mkOuterAccCert cCnt cInit cStep).space p + = cCnt.space p + (L + cInit.space p) + RS + M + (encNat K).length := rfl + _ ≤ rawPoly L := by dsimp only [rawPoly]; omega + _ ≤ poly L := hpolyL + +/-- Trajectory-maximum time and polynomial-workspace bounds for `greedySchedulePassCertificate`: +`O((r ^ Q + 1) * poly(|input|))` native time and polynomial workspace. -/ +theorem greedySchedulePassCertificate_bounds : + ∃ poly : ℕ → ℕ, Cslib.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 := by + obtain ⟨cC, dC, hCnt⟩ := ofPolyTime_exists_bound computableInPolyTime_outerCount + obtain ⟨cI, dI, hInit⟩ := ofPolyTime_exists_bound computableInPolyTime_outerInit + obtain ⟨cP, dP, hPend⟩ := ofPolyTime_exists_bound computableInPolyTime_pendingSlotOfState + obtain ⟨cS, dS, hIn⟩ := ofPolyTime_exists_bound computableInPolyTime_streamSlotInOfOuter + obtain ⟨cF, dF, hFin⟩ := ofPolyTime_exists_bound computableInPolyTime_finishGreedySlotStep + obtain ⟨pSlot, hpSlot, hmSlot, hSlot⟩ := streamBestSlotCertificate_bounds + obtain ⟨pStep, hpStep, hStep⟩ := + mkGreedyStepCert_bounds _ _ _ _ hPend hIn hpSlot hmSlot hSlot hFin + exact mkOuterAccCert_bounds _ _ _ hCnt hInit hpStep hStep + +/-- `greedySchedulePass` runs in `O((r ^ Q + 1) * poly(|input|))` native time and polynomial +workspace. -/ +theorem computableInO_greedySchedulePass : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + 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 => (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length) + (fun p => poly (encScheduleParams p).length) := by + obtain ⟨poly, hpoly, _, hB⟩ := greedySchedulePassCertificate_bounds + exact ⟨poly, hpoly, greedySchedulePassCertificate.computes.mono_le + (fun p => (hB p).1) (fun p => (hB p).2)⟩ + +/-- `greedySchedulePass` runs in polynomial workspace (`ComputableInPolySpace`). -/ +theorem computableInPolySpace_greedySchedulePass : + 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 := by + obtain ⟨poly, hpoly, c, hc, hl⟩ := computableInO_greedySchedulePass + exact ⟨_, fun n => c * (poly n + 1), by fun_prop, hc, hl⟩ + +private theorem mkConstructCert_bounds + (cAcc : NativeCertificate + (fun p : ScheduleParams => (IndexFold.run greedySlotStepBody (outerCount p) (outerInit p)).2) + encScheduleParams encOuterAcc) + (cFinal : NativeCertificate finalizeBalancedSchedules encOuterAcc encOutWords) + {pPass : ℕ → ℕ} {cFinalC dFinal : ℕ} + (hpPass : Cslib.PolynomiallyBounded pPass) (hmPass : Monotone pPass) + (hPass : ∀ p : ScheduleParams, + cAcc.time p ≤ (p.2.1.1 ^ p.1.2.2 + 1) * pPass (encScheduleParams p).length ∧ + cAcc.space p ≤ pPass (encScheduleParams p).length) + (hFinal : ∀ q, cFinal.time q + cFinal.space q ≤ + cFinalC * ((encOuterAcc q).length + 1) ^ dFinal) : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ Monotone poly ∧ + ∀ p : ScheduleParams, (mkConstructCert cAcc cFinal).time p ≤ + (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length ∧ + (mkConstructCert cAcc cFinal).space p ≤ poly (encScheduleParams p).length := by + let bOuter (L : ℕ) := 8 * L ^ 3 + 4 * L ^ 2 + 10 * L + 3 + let pFinal (n : ℕ) := cFinalC * (n + 1) ^ dFinal; let poly (L : ℕ) := pPass L + pFinal (bOuter L) + have hpoly : Cslib.PolynomiallyBounded poly := by dsimp only [poly, pFinal, bOuter]; fun_prop + have hmono : Monotone poly := fun x y hxy => by + have hbo : bOuter x ≤ bOuter y := by + dsimp only [bOuter]; have := Nat.pow_le_pow_left hxy 2 + have := Nat.pow_le_pow_left hxy 3; omega + exact Nat.add_le_add (hmPass hxy) + (Nat.mul_le_mul_left cFinalC (Nat.pow_le_pow_left (Nat.add_le_add_right hbo 1) dFinal)) + refine ⟨poly, hpoly, hmono, fun p => ?_⟩ + let L := (encScheduleParams p).length; let rq := p.2.1.1 ^ p.1.2.2 + let outSt := (IndexFold.run greedySlotStepBody (outerCount p) (outerInit p)).2 + have houtL : (encOuterAcc outSt).length ≤ bOuter L := by + have hrunL := length_encOuterState_run_le p (le_rfl : outerCount p ≤ p.1.1 + p.1.2.1) + rw [IndexFold.length_run] at hrunL + change 2 * (encNat (outerCount p)).length + 1 + (encOuterAcc outSt).length ≤ bOuter L at hrunL + omega + have hfin : cFinal.time outSt + cFinal.space outSt ≤ pFinal (bOuter L) := + (hFinal outSt).trans + (Nat.mul_le_mul_left cFinalC (Nat.pow_le_pow_left (Nat.add_le_add_right houtL 1) dFinal)) + have hp : cAcc.time p ≤ (rq + 1) * pPass L ∧ cAcc.space p ≤ pPass L := hPass p + refine ⟨?_, by change cAcc.space p + cFinal.space outSt ≤ poly L; dsimp only [poly]; omega⟩ + calc (mkConstructCert cAcc cFinal).time p + = cAcc.time p + cFinal.time outSt := rfl + _ ≤ (rq + 1) * pPass L + pFinal (bOuter L) := by omega + _ ≤ (rq + 1) * pPass L + (rq + 1) * pFinal (bOuter L) := + Nat.add_le_add_left (Nat.le_mul_of_pos_left _ (Nat.succ_pos rq)) _ + _ = (rq + 1) * poly L := by dsimp only [poly]; ring + +/-- Trajectory-maximum time and polynomial-workspace bounds for +`constructBalancedSchedulesCertificate` ([OpenAI2026ETH], Lemma 4.5, pp. 30–31). -/ +theorem constructBalancedSchedulesCertificate_bounds : + ∃ poly : ℕ → ℕ, Cslib.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 := by + obtain ⟨pPass, hpPass, hmPass, hPass⟩ := greedySchedulePassCertificate_bounds + obtain ⟨cFinal, dFinal, hFinal⟩ := + ofPolyTime_exists_bound computableInPolyTime_finalizeBalancedSchedules + exact mkConstructCert_bounds _ _ hpPass hmPass hPass hFinal + +/-- `constructBalancedSchedules` runs in `O((r ^ Q + 1) * poly(|input|))` native time (hence +`poly(n, m, |E|, D, Q, r, C)` bit operations where `D = r ^ (2 * Q)`) and polynomial workspace. -/ +theorem computableInO_constructBalancedSchedules : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + 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 (encPair (encList (encList encNat)) (encList (encList encNat))) + (fun p => (p.2.1.1 ^ p.1.2.2 + 1) * poly (encScheduleParams p).length) + (fun p => poly (encScheduleParams p).length) := by + obtain ⟨poly, hpoly, _, hB⟩ := constructBalancedSchedulesCertificate_bounds + exact ⟨poly, hpoly, constructBalancedSchedulesCertificate.computes.mono_le + (fun p => (hB p).1) (fun p => (hB p).2)⟩ + +/-- `constructBalancedSchedules` runs in polynomial workspace (`ComputableInPolySpace`) without +materializing `r ^ Q` candidate words. -/ +theorem computableInPolySpace_constructBalancedSchedules : + 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 (encPair (encList (encList encNat)) (encList (encList encNat))) := by + obtain ⟨poly, hpoly, c, hc, hl⟩ := computableInO_constructBalancedSchedules + exact ⟨_, fun n => c * (poly n + 1), by fun_prop, hc, hl⟩ + +end Cslib.BalancedSchedules + +end diff --git a/ComplexityTests/GreedyLabelSchedule.lean b/ComplexityTests/GreedyLabelSchedule.lean new file mode 100644 index 0000000000..463137a419 --- /dev/null +++ b/ComplexityTests/GreedyLabelSchedule.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +import Complexity.Computability.PolyTime.GreedyLabelSchedule +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Concrete tests for runtime balanced label schedules +-/ + +namespace ComplexityTests.GreedyLabelSchedule + +open Finset Cslib.BalancedSchedules Cslib.GenericRAM Turing.MultiTapeTM + +-- Outer index decoding, capping, no-op on assigned/out-of-range slots, and Q=0/r=0/r=1/E=0 regimes. +example : slotOfIndex 3 2 1 = some (false, 1) ∧ slotOfIndex 3 2 4 = some (true, 1) ∧ + slotOfIndex 3 2 5 = none ∧ slotOfIndex 3 2 99 = none ∧ + pendingSlotOfState (0, (((2, 1, 2), (2, 4), [(0, 0)]), ([some [1, 0], none], [none]))) = + none := by decide +kernel +example : greedySlotStepBody (0, (((2, 1, 2), (2, 4), [(0, 0)]), ([some [1, 0], none], [none]))) = + (((2, 1, 2), (2, 4), [(0, 0)]), ([some [1, 0], none], [none])) := rfl +example : greedySlotStepBody (7, (((2, 1, 2), (2, 4), [(0, 0)]), ([some [1, 0], none], [none]))) = + (((2, 1, 2), (2, 4), [(0, 0)]), ([some [1, 0], none], [none])) := rfl +example : constructBalancedSchedules 2 3 0 2 4 [(0, 1)] = ([[], []], [[], [], []]) ∧ + constructBalancedSchedules 2 2 2 0 4 [(0, 1)] = ([[0, 0], [0, 0]], [[0, 0], [0, 0]]) ∧ + constructBalancedSchedules 2 2 3 1 2 [(0, 0)] = + ([[0, 0, 0], [0, 0, 0]], [[0, 0, 0], [0, 0, 0]]) ∧ + constructBalancedSchedules 2 3 2 3 4 [] = + ([[0, 0], [1, 1]], [[0, 0], [0, 0], [0, 0]]) := by decide +kernel + +-- Nontrivial 2-variable, 4-factor hypergraph with non-empty factors 0, 2 and empty factors 1, 3. +private def testEdges : List (ℕ × ℕ) := [(0, 0), (0, 1), (2, 0), (2, 1)] +private def testEdge : Fin 4 → Fin 4 × Fin 2 + | ⟨0, _⟩ => (0, 0) | ⟨1, _⟩ => (0, 1) | ⟨2, _⟩ => (2, 0) | ⟨3, _⟩ => (2, 1) + +example : edgesOfFin testEdge = testEdges ∧ + normalizeEmptyFactorSchedules 2 testEdges [[1, 1], [1, 0], [0, 1], [1, 1]] = + [[1, 1], [0, 0], [0, 1], [0, 0]] ∧ + greedySchedulePass 2 4 2 2 4 testEdges = + ([some [0, 0], some [1, 1]], [some [0, 0], some [0, 0], some [1, 0], some [0, 0]]) ∧ + constructBalancedSchedules 2 4 2 2 4 testEdges = + ([[0, 0], [1, 1]], [[0, 0], [0, 0], [1, 0], [0, 0]]) := by decide +kernel +-- Exact evaluation of greedyLabelPass and concrete occupancy bounds on testEdge. +example : (let slots : List (Fin 2 ⊕ Fin 4) := + (List.ofFn fun v : Fin 2 => Sum.inl v) ++ (List.ofFn fun f : Fin 4 => Sum.inr f) + let res := greedyLabelPass testEdge 4 (candidateScheduleList (by decide : 1 ≤ 2) 2) slots + (fun _ => none, fun _ => none) + (partialScheduleListOfFin res.1, partialScheduleListOfFin res.2)) = + ([some [0, 0], some [1, 1]], [some [0, 0], some [0, 0], some [1, 0], some [0, 0]]) := by + rw [← greedySchedulePass_eq_greedyLabelPass (by decide : 1 ≤ 2) testEdge 4] + change greedySchedulePass 2 4 2 2 4 testEdges = _; decide +kernel +example : let a := constructedVarSchedule (by decide : 1 ≤ 2) 2 4 2 4 (edgesOfFin testEdge) + let d := constructedFactorSchedule (by decide : 1 ≤ 2) 2 4 2 4 (edgesOfFin testEdge) + (∀ u : (Fin 2 → Fin 2) × (Fin 2 → Fin 2), + occupancy (fun e => (a (testEdge e).2, d (testEdge e).1)) u ≤ 1) ∧ + (∀ t : Fin 2, ∀ g : Fin 2, occupancy (fun v => a v t) g ≤ 1) := by decide +kernel +-- Nonvacuous Lemma 4.5 instance (r=2, Q=1, n=96, m=50, E=96, b=1, w=2; empty factors 48, 49). +private def balancedEdge (e : Fin 96) : Fin 50 × Fin 96 := (⟨e.val / 2, by omega⟩, e) +private abbrev balA := constructedVarSchedule (by decide : 1 ≤ 2) 96 50 1 (1 + 2) + (edgesOfFin balancedEdge) +private abbrev balD := constructedFactorSchedule (by decide : 1 ≤ 2) 96 50 1 (1 + 2) + (edgesOfFin balancedEdge) +example : balD ⟨48, by decide⟩ 0 = 0 ∧ balD ⟨49, by decide⟩ 0 = 0 ∧ + (∀ u, occupancy (fun e => (balA (balancedEdge e).2, balD (balancedEdge e).1)) u ≤ 48) ∧ + (∀ g, occupancy (fun v => balA v 0) g ≤ 96) := by + have hb : ∀ e : Fin 96, #{e' : Fin 96 | (balancedEdge e').2 = (balancedEdge e).2} ≤ 1 := fun e => + (Finset.card_le_card fun _ he' => Finset.mem_singleton.mpr (Finset.mem_filter.mp he').2).trans + (by simp only [Finset.card_singleton, le_rfl]) + have hw : ∀ e : Fin 96, #{e' : Fin 96 | (balancedEdge e').1 = (balancedEdge e).1} ≤ 2 := fun e => + (Finset.card_le_card (t := {⟨2 * (e.val / 2), by omega⟩, ⟨2 * (e.val / 2) + 1, by omega⟩}) + fun _ he' => by + simp only [Finset.mem_filter, Finset.mem_univ, true_and, balancedEdge, Fin.ext_iff] at he' + simp only [Finset.mem_insert, Finset.mem_singleton, Fin.ext_iff]; omega).trans + Finset.card_le_two + obtain ⟨hemp, hinc, hgrp⟩ := constructBalancedSchedules_balanced + (by decide : 1 ≤ 2) (by decide : 1 ≤ 1) (by decide : 1 ≤ 96) balancedEdge hb hw + (by decide : 0 < 1 + 2) (by decide : 2 * (1 + 2) * ((2 ^ 1) ^ 2) ^ 2 ≤ 96) + (by decide : 2 * 1 * 2 ^ 2 ≤ 96) + have h48 := congrFun (hemp ⟨48, by decide⟩ fun ⟨_, he⟩ => by + simp only [balancedEdge, Fin.ext_iff] at he; omega) 0 + have h49 := congrFun (hemp ⟨49, by decide⟩ fun ⟨_, he⟩ => by + simp only [balancedEdge, Fin.ext_iff] at he; omega) 0 + exact ⟨h48, h49, fun u => by have := hinc u; dsimp only [balA, balD]; omega, + fun g => by have := hgrp 0 g; dsimp only [balA]; omega⟩ +-- All-prefix outer state bit-length bound, fun_prop, and concrete certificate bounds at testParams. +example : ∀ s ≤ 2 + 4, (encPair encNat encOuterAcc + (IndexFold.run greedySlotStepBody s + (((2, 4, 2), (2, 4), testEdges), (List.replicate 2 none, List.replicate 4 none)))).length ≤ + 2100 := + fun _ hs => (length_encOuterState_run_valid_le (n := 2) (m := 4) (Q := 2) (r := 2) (C := 4) + (edges := testEdges) hs (by decide +kernel)).trans (by decide +kernel) +example : ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ => (slotOfIndex p.1.1 p.1.2 p.2).isSome) + (encPair (encPair encUnary encUnary) encNat) encBool := by fun_prop +private def testParams : ScheduleParams := ((2, 4, 2), (2, 4), testEdges) +/-- info: constructBalancedSchedulesCertificate.time testParams : ℕ -/ +#guard_msgs in +#check constructBalancedSchedulesCertificate.time testParams +example : ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + greedySchedulePassCertificate.time testParams ≤ 5 * poly (encScheduleParams testParams).length ∧ + greedySchedulePassCertificate.space testParams ≤ poly (encScheduleParams testParams).length ∧ + constructBalancedSchedulesCertificate.time testParams ≤ + 5 * poly (encScheduleParams testParams).length ∧ + constructBalancedSchedulesCertificate.space testParams ≤ + poly (encScheduleParams testParams).length := by + obtain ⟨p1, hp1, _, hb1⟩ := greedySchedulePassCertificate_bounds + obtain ⟨p2, hp2, _, hb2⟩ := constructBalancedSchedulesCertificate_bounds + set L := (encScheduleParams testParams).length + have h1t : greedySchedulePassCertificate.time testParams ≤ 5 * p1 L := (hb1 testParams).1 + have h2t : constructBalancedSchedulesCertificate.time testParams ≤ 5 * p2 L := (hb2 testParams).1 + refine ⟨fun n => p1 n + p2 n, by fun_prop, ?_, (hb1 testParams).2.trans (Nat.le_add_right _ _), + ?_, (hb2 testParams).2.trans (Nat.le_add_left _ _)⟩ <;> dsimp only <;> omega + +end ComplexityTests.GreedyLabelSchedule From 58a3472febd10ea9dad31bd7b51b20782cb4930d Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Tue, 27 Oct 2026 09:08:45 +0000 Subject: [PATCH 3/4] docs(PolyTime): clarify GreedyLabelSchedule certified vs subroutine scope --- .../Computability/PolyTime/GreedyLabelSchedule.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean index 6610a4c2da..ff5cc9df51 100644 --- a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean +++ b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean @@ -38,11 +38,12 @@ Completes the `(n + m)`-slot greedy pass and empty-scope factor normalization of `constructBalancedSchedulesCertificate` certify `O((r ^ Q + 1) * poly(|input|))` native time and polynomial workspace (`ComputableInPolySpace`). -Encoded `ComputableInPolyTime`, `NativeCertificate`, `ComputableInO`, and `ComputableInPolySpace` -theorems govern the concrete list/integer operations (`slotOfIndex`, `pendingSlotOfState`, -`greedySlotStepBody`, `greedySchedulePass`, `normalizeEmptyFactorSchedules`, -`constructBalancedSchedules`, and their certificates) under `encScheduleParams` and `encOuterAcc`, -whereas `constructedVarSchedule` and `constructedFactorSchedule` are unencoded typed specification +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` From 87ea717d5ef01f91b857409a1cd34d1ead30c25b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 05:32:11 -0400 Subject: [PATCH 4/4] doc(PolyTime): qualify numeric schedule runtime by valid incidences --- Complexity/Computability/PolyTime/GreedyLabelSchedule.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean index ff5cc9df51..2d9691aa3d 100644 --- a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean +++ b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean @@ -1291,8 +1291,9 @@ theorem constructBalancedSchedulesCertificate_bounds : ofPolyTime_exists_bound computableInPolyTime_finalizeBalancedSchedules exact mkConstructCert_bounds _ _ hpPass hmPass hPass hFinal -/-- `constructBalancedSchedules` runs in `O((r ^ Q + 1) * poly(|input|))` native time (hence -`poly(n, m, |E|, D, Q, r, C)` bit operations where `D = r ^ (2 * Q)`) and polynomial workspace. -/ +/-- `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 computableInO_constructBalancedSchedules : ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ ComputableInO