OAI/Computability/MaxCut/Estimates/Sample.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OptimalMaxCut.LongCode.Game.Sample line 13
  2. def OAI.OptimalMaxCut.LongCode.Game.gridSize line 17

    Source documentation

    One input-size polynomial denominator, rather than a product of all vertex degrees. Both grid and unweighting error are uniform over all cuts.

    def gridSize (Y E : Type) [Fintype Y] [Fintype E] (q K : ℕ) :=
…
  3. theorem OAI.OptimalMaxCut.LongCode.Game.gridSize_pos line 20
  4. def OAI.OptimalMaxCut.LongCode.Game.gridWeights line 23
  5. theorem OAI.OptimalMaxCut.LongCode.Game.gridWeights_error line 28
  6. def OAI.OptimalMaxCut.LongCode.Game.gridOutput line 45
  7. theorem OAI.OptimalMaxCut.LongCode.Game.gridOutput_error line 49
  8. theorem OAI.OptimalMaxCut.LongCode.Game.gridOutput_complete line 57
  9. theorem OAI.OptimalMaxCut.LongCode.Game.gridOutput_vertex_bound line 67
  10. theorem OAI.OptimalMaxCut.LongCode.Game.exists_grid_gap_parameters line 74

    Source documentation

    All game-independent constants for the rounded, executable-integer target. This is the mathematical gap; the polynomial TM printer is still separate.

     theorem exists_grid_gap_parameters (α : ℝ) (hα : alphaGW < α) (hα1 : α ≤ 1) :
    ∃ (t ε y n : ℚ) (δ : ℝ) (K : ℕ) (ht : t ∈ Set.Icc (-1 : ℚ) 1),
      0 < t ∧ t < 1 ∧ 0 < ε ∧ (ε:ℝ) < 1/2 ∧ 0 < δ ∧ δ < 1/2 ∧
      0 < y ∧ 0 ≤ n ∧ (n:ℝ) < α*(y:ℝ) ∧
      (∀ {X Y E : Type} [Fintype X] [Fintype Y] [Fintype E] {q N : ℕ}
        (G : Game X Y E q) (enum : X × Cube (Fin q) ≃ Fin N) (anchor : Fin N),
        (∃ lx ly, 1-(ε:ℝ) ≤ G.satisfied lx ly) →
        (y:ℝ) ≤ ((G.gridOutput t ht enum anchor K).graph.maxCut : ℝ) /
          (G.gridOutput t ht enum anchor K).scale) ∧
      (∀ {X Y E : Type} [Fintype X] [Fintype Y] [Fintype E] {q N : ℕ}
        (_hq : 0 < q) (G : Game X Y E q) (enum : X × Cube (Fin q) ≃ Fin N) (anchor : Fin N),
        G.Sound δ → ((G.gridOutput t ht enum anchor K).graph.maxCut : ℝ) /
…

    Mentions: OAI.OptimalMaxCut.alphaGW, OAI.OptimalMaxCut.LongCode.Game

  11. inductive OAI.OptimalMaxCut.CounterMachine.Tape line 125
  12. inductive OAI.OptimalMaxCut.CounterMachine.Instruction line 129
  13. structure OAI.OptimalMaxCut.CounterMachine.Data line 140
  14. structure OAI.OptimalMaxCut.CounterMachine.Configuration line 146
  15. def OAI.OptimalMaxCut.CounterMachine.Instruction.execute line 151
  16. def OAI.OptimalMaxCut.CounterMachine.step line 169
  17. def OAI.OptimalMaxCut.CounterMachine.tapes line 172
  18. def OAI.OptimalMaxCut.CounterMachine.embed line 178
  19. def OAI.OptimalMaxCut.CounterMachine.goto line 181
  20. def OAI.OptimalMaxCut.CounterMachine.Instruction.code line 184
  21. theorem OAI.OptimalMaxCut.CounterMachine.tapes_inc line 202
  22. theorem OAI.OptimalMaxCut.CounterMachine.tapes_dec line 212
  23. theorem OAI.OptimalMaxCut.CounterMachine.tapes_read line 222
  24. theorem OAI.OptimalMaxCut.CounterMachine.tapes_back line 228
  25. theorem OAI.OptimalMaxCut.CounterMachine.tapes_write line 234
  26. theorem OAI.OptimalMaxCut.CounterMachine.instruction_simulation line 239
  27. theorem OAI.OptimalMaxCut.CounterMachine.step_simulation line 281
  28. def OAI.OptimalMaxCut.CounterMachine.machine line 291

    Source documentation

    No semantic atomic arithmetic operation is being charged unit time: only unary increment/decrement, one input/output bit, and finite jumps are atomic.

    def machine [Fintype R] [Fintype L] (p : L → Instruction R L) (main : L) : FinTM2 where
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Instruction

  29. theorem OAI.OptimalMaxCut.CounterMachine.finite_tape_alphabet line 302
  30. inductive OAI.OptimalMaxCut.CounterMachine.Command line 314

    Source documentation

    A structured program still has only finitely many syntactic labels. loop r c tests/decrements its own unary counter, then runs c. It is a genuine while loop: no claim of termination is built into the syntax.

    inductive Command (R : Type) where
…
  31. def OAI.OptimalMaxCut.CounterMachine.Command.Label line 328
  32. instance OAI.OptimalMaxCut.CounterMachine.Command.labelFintype line 335
  33. def OAI.OptimalMaxCut.CounterMachine.Command.entry line 343
  34. def OAI.OptimalMaxCut.CounterMachine.Command.code line 348
  35. def OAI.OptimalMaxCut.CounterMachine.Command.incData line 376
  36. def OAI.OptimalMaxCut.CounterMachine.Command.decData line 378
  37. def OAI.OptimalMaxCut.CounterMachine.Command.readData line 380
  38. def OAI.OptimalMaxCut.CounterMachine.Command.backData line 382
  39. def OAI.OptimalMaxCut.CounterMachine.Command.discardData line 384
  40. def OAI.OptimalMaxCut.CounterMachine.Command.writeData line 385
  41. inductive OAI.OptimalMaxCut.CounterMachine.Command.Evaluates line 389

    Source documentation

    Timed operational semantics. Loop termination and the number of iterations must be proved by the caller; there is no hidden bounded-search oracle.

    inductive Evaluates : Command R → Data R → Data R → ℕ → Prop
  | skip (d) : Evaluates .skip d d 1
  | inc (d r) : Evaluates (.inc r) d (incData d r) 1
  | dec (d r) : Evaluates (.dec r) d (decData d r) 1
  | write (d b) : Evaluates (.write b) d (writeData d b) 1
  | discard (d) : Evaluates .discard d (discardData d) 1
  | rewind_empty {d} : d.backup = [] → Evaluates .rewind d d 1
  | rewind_cons {d e n b rest} : d.backup = b :: rest →
      Evaluates .rewind (backData d) e n → Evaluates .rewind d e (1 + n)
  | seq {a b d e f n m} : Evaluates a d e n → Evaluates b e f m →
      Evaluates (.seq a b) d f (n + m)
  | test_zero {r a b d e n} : d.reg r = 0 → Evaluates a d e n →
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Command, OAI.OptimalMaxCut.CounterMachine.Data, OAI.OptimalMaxCut.CounterMachine.Command.incData, OAI.OptimalMaxCut.CounterMachine.Command.decData, OAI.OptimalMaxCut.CounterMachine.Command.writeData, OAI.OptimalMaxCut.CounterMachine.Command.discardData, OAI.OptimalMaxCut.CounterMachine.Command.backData

  42. def OAI.OptimalMaxCut.CounterMachine.advance line 418

    Source documentation

    Propagation through halt is explicit, as in the supplied TM2 support.

    def advance (p : L → Instruction R L) : Option (Configuration R L) → Option (Configuration R L) :=
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Instruction, OAI.OptimalMaxCut.CounterMachine.Configuration

  43. def OAI.OptimalMaxCut.CounterMachine.atCfg line 421
  44. def OAI.OptimalMaxCut.CounterMachine.Runs line 423
  45. theorem OAI.OptimalMaxCut.CounterMachine.runs_one line 426
  46. theorem OAI.OptimalMaxCut.CounterMachine.Runs.trans line 430
  47. theorem OAI.OptimalMaxCut.CounterMachine.Command.trace line 436
  48. theorem OAI.OptimalMaxCut.CounterMachine.advance_simulation line 508
  49. theorem OAI.OptimalMaxCut.CounterMachine.iterate_simulation line 514
  50. abbrev OAI.OptimalMaxCut.CounterMachine.Command.FinalLabel line 525
  51. def OAI.OptimalMaxCut.CounterMachine.Command.finalCode line 527
  52. def OAI.OptimalMaxCut.CounterMachine.Command.initial line 531
  53. def OAI.OptimalMaxCut.CounterMachine.Command.finiteMachine line 534
  54. theorem OAI.OptimalMaxCut.CounterMachine.Command.finiteMachine_initial line 537
  55. def OAI.OptimalMaxCut.CounterMachine.Command.machine_run line 547

    Source documentation

    Every derived structured evaluation is an actual finite-alphabet execution, including the final halt transition. No arithmetic oracle is added.

     noncomputable def machine_run [Fintype R] {c : Command R} {input : List Bool} {out : Data R} {n : ℕ}
    (h : Evaluates c (initial input) out n) :
    StateTransition.EvalsToInTime c.finiteMachine.step (initList c.finiteMachine input)
      (some (embed ⟨out, none⟩)) (n + 1) := by
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Command, OAI.OptimalMaxCut.CounterMachine.Data, OAI.OptimalMaxCut.CounterMachine.Command.Evaluates, OAI.OptimalMaxCut.CounterMachine.Command.initial, OAI.OptimalMaxCut.CounterMachine.embed

  56. theorem OAI.OptimalMaxCut.CounterMachine.Command.finiteMachine_finite_alphabet line 564
  57. def OAI.OptimalMaxCut.CounterMachine.Data.set line 576
  58. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_self line 579
  59. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_set line 582
  60. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_reg_same line 585
  61. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_reg_ne line 588
  62. theorem OAI.OptimalMaxCut.CounterMachine.Data.set_comm line 591
  63. def OAI.OptimalMaxCut.CounterMachine.Command.clear line 601
  64. def OAI.OptimalMaxCut.CounterMachine.Command.move line 603
  65. theorem OAI.OptimalMaxCut.CounterMachine.Command.clear_evaluates line 605
  66. theorem OAI.OptimalMaxCut.CounterMachine.Command.move_evaluates line 621
  67. def OAI.OptimalMaxCut.CounterMachine.Command.Within line 651

    Source documentation

    A definite cutoff clock for an actually terminating command, not an assumed machine-computability predicate.

    def Within (c : Command R) (d e : Data R) (B : ℕ) : Prop :=
…

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

  68. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.seq line 654
  69. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.mono line 660
  70. theorem OAI.OptimalMaxCut.CounterMachine.Data.ext line 673
  71. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.loop line 679
  72. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.inc line 691
  73. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.dec line 693
  74. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.skip line 695
  75. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.clear line 697
  76. theorem OAI.OptimalMaxCut.CounterMachine.Command.Within.move line 700
  77. def OAI.OptimalMaxCut.CounterMachine.Command.copy line 705

    Source documentation

    Copy without destruction using a disjoint zeroed backup register.

    def copy (r s t : R) : Command R :=
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Command

  78. theorem OAI.OptimalMaxCut.CounterMachine.Command.copy_evaluates line 708
  79. def OAI.OptimalMaxCut.CounterMachine.Command.mulAdd line 739
  80. theorem OAI.OptimalMaxCut.CounterMachine.Command.mulAdd_evaluates line 742