PolynomialTime.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Superstring.BitCode.RunsInPolyTime line 11
Source documentation
Actual code and a clock, not an oracle or a premise of the main theorem. Ambient register types may be infinite names; certificate_any restricts them exactly to finite support. All executions start and end with the single encoded input/output stack.
```
def RunsInPolyTime {α β : Type} (ea : α → List Bool) (eb : β → List Bool)
    (f : α → β) : Prop :=
…
```
theorem OAI.Superstring.BitCode.RunsInPolyTime.certificate line 22
theorem OAI.Superstring.BitCode.RunsInPolyTime.output_length line 27
theorem OAI.Superstring.BitCode.RunsInPolyTime.id line 37
theorem OAI.Superstring.BitCode.single_left line 50
theorem OAI.Superstring.BitCode.single_right line 57
theorem OAI.Superstring.BitCode.Block.transfer_single line 66
def OAI.Superstring.BitCode.Block.move line 83
Source documentation
Relocate a single encoded value without reversing its bit order.
```
def move (i j scratch : K) : Block K := .seq (transfer i scratch) (transfer scratch j)
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Block.transfer
theorem OAI.Superstring.BitCode.Block.move_single line 85
theorem OAI.Superstring.BitCode.eval_mono_nat line 95
theorem OAI.Superstring.BitCode.RunsInPolyTime.comp line 107
Source documentation
Composition of finite bit programs preserves polynomial-time computability.
```
theorem comp (hg : RunsInPolyTime eb ec g) (hf : RunsInPolyTime ea eb f) :
    RunsInPolyTime ea ec (g ∘ f) := by
…
```
Mentions: OAI.Superstring.BitCode.RunsInPolyTime
theorem OAI.Superstring.BitCode.RunsInPolyTime.of_observed line 146
Source documentation
Turn an observed-output proof into clean composable code. No garbage is silently ignored, and every extra clearing step is paid for.
```
theorem of_observed {K : Type} [DecidableEq K] (b : Block K) (i o : K)
    (P : Polynomial ℕ)
    (correct : ∀ a, ∃ n t, n ≤ P.eval (ea a).length ∧
      b.Exec (single i (ea a)) t n ∧ t o = eb (f a)) : RunsInPolyTime ea eb f := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.single, OAI.Superstring.BitCode.RunsInPolyTime
theorem OAI.Superstring.BitCode.RunsInPolyTime.of_program line 182
theorem OAI.Superstring.BitCode.Block.Exec.embed line 229
Source documentation
Embed a program into any injectively named register bank. Its entire complement is framed. This also permits distinct routines to share designated input/output registers while having disjoint private work registers.
```
theorem Exec.embed {b : Block K} {s t : Store K} {n : ℕ} (h : b.Exec s t n)
    (f : K → L) (hf : Function.Injective f) (S : Store L)
    (hs : ∀ k, S (f k) = s k) :
    ∃ T, (b.rename f).Exec S T n ∧ (∀ k, T (f k) = t k) ∧
      ∀ j, (∀ k, f k ≠ j) → T j = S j := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.Exec

theorem OAI.Superstring.BitCode.Block.Exec.transport line 275

Source documentation

The convenient exact-final-state form of framed register embedding.

theorem Exec.transport {b : Block K} {s t : Store K} {n : ℕ} (h : b.Exec s t n)
    (f : K → L) (hf : Function.Injective f) (S T : Store L)
    (hs : ∀ k, S (f k) = s k) (ht : ∀ k, T (f k) = t k)
    (hframe : ∀ j, (∀ k, f k ≠ j) → T j = S j) :
    (b.rename f).Exec S T n := by
…

Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.Exec