OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedScheduleWatchdog.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.BudgetedSchedule.allowance_le_watchdog line 12
2. theorem OAI.LowSpaceSubsetSum.BudgetedSchedule.accepts_of_core line 35

   Source documentation

   The watchdog runs the actual prepared-array checker and parent emitter; the successful semantic event is used only to prove its output.

   theorem accepts_of_core (D : RepresentationScheduleData n g) (F : IndexedMask n)
       (hF : F.semantic = D.signs) (B : ℕ) (hn : 10000 ≤ n) (hg : g ≤ n)
       (rows : Fin 4 → Vector (Fin n) g)
       (hrows : ∀ i j, (rows i)[j] = D.coordinates.index (i, j))
       (families : Fin 4 → Array (Fin (2 ^ g)))
       (hsize : ∀ i, (families i).size ≤ 11 * 2 ^ g)
       (hcore : (D.coreUnits B (fun i => (families i).map SeparatorStoredMasks.decode) : ℝ) ≤
         (inputScale D.input : ℝ) ^ 410 * (2 : ℝ) ^ ((n + 1) / 2))
       (hyes : D.run B (fun i => (families i).map SeparatorStoredMasks.decode) = true) :
       ∃ left, (run D F hF B (PreparedSeparatorContext.prepare rows families hsize).1
         D.target (trialWatchdog D.input)).1 = some (true, left) := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RepresentationScheduleData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.SeparatorStoredMasks.decode, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.BudgetedSchedule.run, OAI.LowSpaceSubsetSum.PreparedSeparatorContext.prepare, OAI.LowSpaceSubsetSum.trialWatchdog