PolynomialTimeSize.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A polynomial-time TM2 program has polynomial output bit length. The constant below counts the pushes in its finite program text, rather than assuming an output-size estimate as an additional complexity axiom.

def OAI.ContinuumCoulomb.TM2Size.pushes line 16

Source documentation

Maximum number of pushes along one finite statement branch.

def pushes {K : Type} {Γ : K → Type} {Λ σ : Type} : TM2.Stmt Γ Λ σ → ℕ
  | .push _ _ q => pushes q + 1
  | .peek _ _ q => pushes q
  | .pop _ _ q => pushes q
  | .load _ q => pushes q
  | .branch _ q r => max (pushes q) (pushes r)
  | .goto _ => 0
  | .halt => 0

theorem OAI.ContinuumCoulomb.TM2Size.stepAux_stack_length line 25
def OAI.ContinuumCoulomb.TM2Size.programPushes line 60
Source documentation
A finite program has a fixed bound on pushes in one machine step.
```
def programPushes (tm : FinTM2) : ℕ := by
…
```
theorem OAI.ContinuumCoulomb.TM2Size.step_stack_length line 64
theorem OAI.ContinuumCoulomb.TM2Size.iterate_stack_length line 79
theorem OAI.ContinuumCoulomb.TM2Size.init_stack_length line 98
theorem OAI.ContinuumCoulomb.TM2Size.output_length line 106
Source documentation
Bit output length is bounded directly from a genuine polynomial-time certificate; this is needed when composing the hardness reduction.
```
theorem output_length {α β : Type} {ea : α → List Bool} {eb : β → List Bool}
    {f : α → β} (h : TM2ComputableInPolyTime ea eb f) (a : α) :
    (eb (f a)).length ≤ (ea a).length + h.time.eval (ea a).length * programPushes h.tm := by
…
```
Mentions: OAI.ContinuumCoulomb.TM2Size.programPushes