OAI/Computability/MaxCut/Estimates/Put.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OptimalMaxCut.CounterMachine.Command.put line 11
  2. theorem OAI.OptimalMaxCut.CounterMachine.Command.put_evaluates line 15
  3. def OAI.OptimalMaxCut.CounterMachine.Command.subFrom line 26
  4. theorem OAI.OptimalMaxCut.CounterMachine.Command.subFrom_evaluates line 28
  5. theorem OAI.OptimalMaxCut.CounterMachine.Command.rewind_evaluates line 44
  6. def OAI.OptimalMaxCut.CounterMachine.Command.skipInput line 64

    Source documentation

    Skip exactly the prescribed number of attempted reads, recording only real bits on the backup. EOF is handled by a genuine branch.

    def skipInput (r : R) : Command R := .loop r (.read .skip .skip .skip)

    Mentions: OAI.OptimalMaxCut.CounterMachine.Command

  7. theorem OAI.OptimalMaxCut.CounterMachine.Command.skipInput_evaluates line 66
  8. def OAI.OptimalMaxCut.CounterMachine.Command.inputBit line 98

    Source documentation

    Read one bit at a unary index; a missing bit is false. Input is restored.

    def inputBit (index result : R) : Command R :=
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Command

  9. theorem OAI.OptimalMaxCut.CounterMachine.Command.inputBit_evaluates line 101
  10. def OAI.OptimalMaxCut.CounterMachine.Command.lengthLoop line 156
  11. theorem OAI.OptimalMaxCut.CounterMachine.Command.lengthLoop_evaluates line 159
  12. def OAI.OptimalMaxCut.CounterMachine.Command.inputLength line 207
  13. theorem OAI.OptimalMaxCut.CounterMachine.Command.inputLength_evaluates line 209
  14. inductive OAI.OptimalMaxCut.CounterMachine.Expr line 242

    Source documentation

    Polynomially bounded arithmetic expressions with finite bounded summation. The only inspection of the input is by actual bit-read or length macros above. Bounded sums suffice for divisions, remainder, bounded minimization and every finite loop in the rounded long-code graph printer.

    inductive Expr where
…
  15. def OAI.OptimalMaxCut.CounterMachine.Expr.bind line 255
  16. def OAI.OptimalMaxCut.CounterMachine.Expr.eval line 259
  17. def OAI.OptimalMaxCut.CounterMachine.Expr.valueBudget line 270
  18. theorem OAI.OptimalMaxCut.CounterMachine.Expr.eval_le line 281
  19. def OAI.OptimalMaxCut.CounterMachine.Expr.timeBudget line 307
  20. def OAI.OptimalMaxCut.CounterMachine.Expr.compile line 320
  21. def OAI.OptimalMaxCut.CounterMachine.Data.Clean line 339
  22. theorem OAI.OptimalMaxCut.CounterMachine.Data.Clean.mono line 341
  23. theorem OAI.OptimalMaxCut.CounterMachine.Data.Clean.set_succ line 344
  24. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_args line 350
  25. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_clean_zero line 355
  26. def OAI.OptimalMaxCut.CounterMachine.Expr.Correct line 367

    Source documentation

    Exact operational contract: all scratch counters are returned to zero, original arguments and input are preserved, and a fixed explicit clock holds.

    def Correct (e : Expr) : Prop := ∀ (vars : ℕ → ℕ) (k : ℕ) (d : Data ℕ) (M : ℕ),
…

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

  27. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_const line 372
  28. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_arg line 376
  29. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_length line 383
  30. theorem OAI.OptimalMaxCut.CounterMachine.Expr.binary_start line 388
  31. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_add line 405
  32. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_sub line 429
  33. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_zero line 453
  34. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_bit line 467
  35. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.assoc line 497
  36. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_mul line 509