OAI/Computability/MaxCut/Machines/Printer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OptimalMaxCut.CounterMachine.printer line 11
2. def OAI.OptimalMaxCut.CounterMachine.printerTime line 13
3. theorem OAI.OptimalMaxCut.CounterMachine.printer_evaluates line 18
4. theorem OAI.OptimalMaxCut.CounterMachine.halted_eq line 32
5. def OAI.OptimalMaxCut.CounterMachine.tableComputer line 44

   Source documentation

   A genuine polynomial-time finite Boolean-tape Turing machine for any closed bounded-arithmetic bit table. This is an operational theorem, not a closure axiom or a unit-cost machine convention.

   noncomputable def tableComputer (len bit : Expr) :
       TM2ComputableInPolyTime (id : List Bool → List Bool) id (table len bit) where
   …

   Mentions: OAI.OptimalMaxCut.CounterMachine.Expr, OAI.OptimalMaxCut.CounterMachine.table

6. theorem OAI.OptimalMaxCut.CounterMachine.tableComputer_finiteAlphabet line 84