ClockSchedule.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniformKServer.BitTape.cells line 10
def OAI.UniformKServer.ClockSchedule.capped line 14
def OAI.UniformKServer.ClockSchedule.budget line 17
def OAI.UniformKServer.ClockSchedule.scheduled line 19
theorem OAI.UniformKServer.ClockSchedule.shift_cells line 22
theorem OAI.UniformKServer.ClockSchedule.ofWord_cells line 30
theorem OAI.UniformKServer.ClockSchedule.step_bounds line 33
theorem OAI.UniformKServer.ClockSchedule.run_cons line 48
theorem OAI.UniformKServer.ClockSchedule.run_bounds line 51
theorem OAI.UniformKServer.ClockSchedule.run_append line 69
theorem OAI.UniformKServer.ClockSchedule.run_halted line 72
theorem OAI.UniformKServer.ClockSchedule.capped_eq_after line 78
theorem OAI.UniformKServer.ClockSchedule.capped_bounds line 87
Source documentation
A literal capped bit-machine simulation cannot write a compressed output claiming more bits or touch more than linearly many cells.
```
theorem capped_bounds (P : BitMachine) (input : List Bool) (B : ℕ) :
    (capped P input B).outputRev.length ≤ B ∧
    (capped P input B).input.cells ≤ input.length + 1 + B ∧
    ∀ i, ((capped P input B).work i).cells ≤ 1+B := by
…
```
Mentions: OAI.UniformKServer.BitMachine, OAI.UniformKServer.ClockSchedule.capped

theorem OAI.UniformKServer.ClockSchedule.deterministic_activation line 99

Source documentation

The exact activation threshold and output/space bounds for the source restart-from-scratch schedule. The premise is only termination of the supplied literal constructor, not a complexity or competitive assumption.

theorem deterministic_activation (P : BitMachine) (input : List Bool)
    (halts : ∃ B, (capped P input B).yielded = true) :
    ∃ T : ℕ, 1 ≤ T ∧ ∀ t : ℕ, 1 ≤ t →
      ((scheduled P input t).yielded = true ↔ 2^T-1 ≤ t) ∧
      (scheduled P input t).outputRev.length ≤ Nat.clog 2 (t+1) ∧
      (scheduled P input t).input.cells ≤ input.length+1+Nat.clog 2 (t+1) ∧
      (∀ i, ((scheduled P input t).work i).cells ≤ 1+Nat.clog 2 (t+1)) := by
…

Mentions: OAI.UniformKServer.BitMachine, OAI.UniformKServer.ClockSchedule.capped, OAI.UniformKServer.ClockSchedule.scheduled