FiniteWordMachine.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A single physical machine for a computed finite-word algorithm

def OAI.ContingencyTables.FiniteWordExecution.machine line 14
def OAI.ContingencyTables.FiniteWordExecution.machineTime line 17
lemma OAI.ContingencyTables.FiniteWordExecution.output_alphabet line 20

theorem OAI.ContingencyTables.FiniteWordExecution.machine_law line 29

Source documentation

Every run halts within the physical execution bound. Its output law is exactly the law obtained by feeding an independent uniform word to f.

theorem machine_law (N : TreeTyped.Realizer n) (F : TreeTyped.Realizer f)
    (as : List Symbol) (ha : ∀ a∈as,a≠0)
    (hout : ∀ bs,∀ b∈f (as,bs),b≠6 ∧ b≠7)
    (t : ℕ) (ht : machineTime N F as≤t) :
    (∀ bits : Bits t,(run (machine N F) as bits).state=none) ∧
    ∀ g : Tape Symbol → ℚ,
      average (fun bits : Bits t => g (run (machine N F) as bits).tape)=
        average (fun bits : Bits (n as) => g (Tape.mk₁ (f (as,List.ofFn bits)))) := by
…

Mentions: OAI.ContingencyTables.FiniteWordExecution.machineTime, OAI.ContingencyTables.FiniteWordExecution.machine

theorem OAI.ContingencyTables.FiniteWordExecution.machineTime_polynomial line 48
Source documentation
Packing, coin reads, deterministic execution and public output all have a polynomial bound in encoded input size plus the declared word.
```
theorem machineTime_polynomial {N : TreeTyped.Realizer n} {F : TreeTyped.Realizer f}
    (hN : TreeTyped.PolynomialTime N) (hF : TreeTyped.PolynomialTime F) :
    ∃ q : Polynomial ℕ,∀ as,machineTime N F as≤q.eval (wordMeasure n as) := by
…
```
Mentions: OAI.ContingencyTables.FiniteWordExecution.machineTime, OAI.ContingencyTables.FiniteWordExecution.wordMeasure