OAI/Computability/MaxCut/Machines/CloneMachineModel.lean

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

Affine word emission in the actual clone-table machine

The shared machine keeps its context fixed while copying one saved word. Its finite transducer therefore acts by a fixed symbol substitution. The lemmas below identify that substitution with the established unary encoding of offset + scale * value, including all header and equation-field contexts. Scale, offset, and the triple-table length remain symbolic.

  1. inductive OAI.MaxCutGames.Reduction.CloneMachineModel.Tape line 12
  2. abbrev OAI.MaxCutGames.Reduction.CloneMachineModel.Context line 16
  3. abbrev OAI.MaxCutGames.Reduction.CloneMachineModel.State line 17
  4. abbrev OAI.MaxCutGames.Reduction.CloneMachineModel.Alphabet line 18
  5. inductive OAI.MaxCutGames.Reduction.CloneMachineModel.Label line 20
  6. def OAI.MaxCutGames.Reduction.CloneMachineModel.defaultControl line 36
  7. def OAI.MaxCutGames.Reduction.CloneMachineModel.initialState line 37
  8. def OAI.MaxCutGames.Reduction.CloneMachineModel.headerTape line 39
  9. def OAI.MaxCutGames.Reduction.CloneMachineModel.contextSource line 41
  10. def OAI.MaxCutGames.Reduction.CloneMachineModel.contextScale line 45
  11. def OAI.MaxCutGames.Reduction.CloneMachineModel.tripleField line 49
  12. def OAI.MaxCutGames.Reduction.CloneMachineModel.contextOffset line 56
  13. def OAI.MaxCutGames.Reduction.CloneMachineModel.affineEmit line 60
  14. def OAI.MaxCutGames.Reduction.CloneMachineModel.emission line 64
  15. def OAI.MaxCutGames.Reduction.CloneMachineModel.contextNext line 67
  16. def OAI.MaxCutGames.Reduction.CloneMachineModel.cleanupNext line 74
  17. def OAI.MaxCutGames.Reduction.CloneMachineModel.drain line 77
  18. def OAI.MaxCutGames.Reduction.CloneMachineModel.program line 84
  19. def OAI.MaxCutGames.Reduction.CloneMachineModel.machine line 107
  20. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_eq_flatMap line 136

    Source documentation

    Identity control transitions reduce exactly to fixed symbol substitution.

    theorem output_eq_flatMap {Q : Type} [Fintype Q]
    (emit : Q → Bool → List Bool) (q : Q) (input : List Bool) :
    MachineTransducer.output (fun state _ => state) emit q input =
      input.flatMap (emit q) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.output

  21. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_append line 145
  22. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.affineEmit_replicate_true line 152
  23. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.affineEmit_word line 160

    Source documentation

    This includes zero scale and zero offset, with no positivity assumptions.

    theorem affineEmit_word (scale offset v : Nat) :
    (encodeWord v).flatMap (affineEmit scale offset) =
      encodeWord (offset + scale * v) := by
…
  24. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.affineEmit_word_append line 167
  25. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.affineEmit_words line 172
  26. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_word line 181

    Source documentation

    Exact symbolic context transform used by the shared clone-table machine.

    theorem output_word (triples : List (Nat × Nat × Nat))
    (c : Context triples.length) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) c (encodeWord v) =
      encodeWord (contextOffset triples c + contextScale c * v) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.output

  27. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_word_append line 188
  28. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_words line 195
  29. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_header_variables line 202
  30. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_header_count line 208

    Source documentation

    The equation-count multiplier remains the arbitrary symbolic table length.

    theorem output_header_count (triples : List (Nat × Nat × Nat)) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) (.inl 1) (encodeWord v) =
      encodeWord (triples.length * v) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.output

  31. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_field line 213
  32. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_first_field line 219
  33. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_second_field line 225
  34. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_third_field line 231
  35. theorem OAI.MaxCutGames.Reduction.CloneMachineAffine.output_rhs_field line 238

    Source documentation

    RHS words are copied exactly, including both legal Boolean values.

    theorem output_rhs_field (triples : List (Nat × Nat × Nat))
    (i : Fin triples.length) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) (.inr (i, 3)) (encodeWord v) =
      encodeWord v := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.output

  36. inductive OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.Label line 255
  37. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.readStart line 259
  38. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.readLoop line 260
  39. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.destination line 264
  40. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.statement line 266
  41. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.atReadStart line 280
  42. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.atReadLoop line 287
  43. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.atReadDone line 295
  44. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.copied line 300
  45. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.readTapes line 303
  46. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes line 308
  47. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.clear_readTapes line 312
  48. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.readTapes_work line 332
  49. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_other line 337
  50. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_source line 341
  51. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_work line 345
  52. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_n line 348
  53. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_m line 352
  54. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.inTime line 357

    Source documentation

    Actual copying, two-field extraction, and complete disposal of the work copy.

    def inTime (slots : Fin 5 ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
    (base : K → List Bool) (n m : Nat) (suffix : List Bool)
    (hinput : base (slots 0) = encodeWords [n, m] ++ suffix)
    (hwork : base (slots 1) = []) (hscratch : base (slots 4) = [])
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .copyOut), ((ambient, ()), register), base⟩
      (some ⟨exit, ((ambient, ()), none), resultTapes slots base n m⟩)
      (3 * (base (slots 0)).length + 6) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.Label, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.statement, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes

  55. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.baseConstant line 407
  56. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.radix line 408
  57. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.capacity line 409
  58. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.edgeFactor line 410
  59. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.edgeCount line 412
  60. inductive OAI.MaxCutGames.Reduction.MachineAddressHeaders.Kind line 416
  61. abbrev OAI.MaxCutGames.Reduction.MachineAddressHeaders.Kind.enumList line 419
  62. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Kind.enumList_getElem?_ctorIdx_eq line 421
  63. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Kind.enumList_nodup line 425
  64. instance OAI.MaxCutGames.Reduction.MachineAddressHeaders.(instance at line 427) line 427
  65. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.polynomial line 431
  66. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.polynomial_capacity_eval line 435
  67. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.polynomial_edges_eval line 439
  68. inductive OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Control line 445
  69. abbrev OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Control.enumList line 450
  70. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Control.enumList_getElem?_ctorIdx_eq line 453
  71. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Control.enumList_nodup line 457
  72. instance OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.(instance at line 459) line 459
  73. abbrev OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Coefficients line 463
  74. abbrev OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Layout line 467
  75. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.inputControl line 469
  76. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.outputControl line 472
  77. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.controlSlots line 475
  78. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.coefficientBlock line 483
  79. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.localSlots line 490
  80. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control line 511
  81. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots line 513
  82. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control_eq_iff line 517
  83. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_radix line 520
  84. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_accA line 522
  85. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_accB line 524
  86. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_destination line 526
  87. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_counter line 528
  88. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_scratch line 530
  89. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_digit line 532
  90. inductive OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Label line 536
  91. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalStart line 542
  92. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.afterEval line 545
  93. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.statement line 551

    Source documentation

    The fixed arithmetic program never captures input counts in its code.

    def statement (slots : Layout k s d noiseCount ↪ K) (labels : Label k s d noiseCount → Λ)
    (exit : Option Λ) :
    Label k s d noiseCount → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ)
  | .copyNOut => MachineTransfer.loopAt (control slots .variableCount) (control slots .scratch)
      id false (labels .copyNOut) (some (labels .copyNBack))
  | .copyNBack => MachineCopy.forkLoop (control slots .scratch) (control slots .variableCount)
      (control slots .baseValue) false (labels .copyNBack) (some (labels .copyMOut))
  | .copyMOut => MachineTransfer.loopAt (control slots .occurrenceCount) (control slots .scratch)
      id false (labels .copyMOut) (some (labels .copyMBack))
  | .copyMBack => MachineCopy.forkLoop (control slots .scratch) (control slots .occurrenceCount)
      (control slots .temporary) false (labels .copyMBack) (some (labels .addM))
  | .addM => MachineUnaryAddAt.loop (control slots .temporary) (control slots .baseValue)
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control

  94. structure OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.WorkClean line 582
  95. structure OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Clean line 589
  96. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.WorkClean.update_control line 595
  97. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalPhaseTrace line 608

    Source documentation

    One placed invocation of the already checked preserving polynomial evaluator.

    theorem evalPhaseTrace (slots : Layout k s d noiseCount ↪ K)
    (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
    (kind : Kind) (base : K → List Bool) (value : Nat)
    (hinput : base (control slots (inputControl kind)) = encodeWord value)
    (hdest : base (control slots (outputControl kind)) = [])
    (clean : WorkClean slots base) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[SourceHeaderCounts.Eval.steps (polynomial k s d noiseCount kind) value]
      (some ⟨some (labels (evalStart kind)), ((ambient, ()), register), base⟩) =
      some ⟨some (labels (afterEval kind)), ((ambient, ()), none),
        Function.update base (control slots (outputControl kind))
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Kind, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.inputControl, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.outputControl, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.WorkClean, OAI.MaxCutGames.Reduction.MachineAddressHeaders.polynomial, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalStart, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.afterEval

  98. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.headerBits line 631
  99. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.resultTapes line 634
  100. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.steps line 641
  101. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.trace_trans_inline_MachineAddressHeaders line 647
  102. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.preparedBase line 651
  103. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.prepareBaseTrace line 656

    Source documentation

    Copies preserve both operands; addition consumes only the temporary copy.

    theorem prepareBaseTrace (slots : Layout k s d noiseCount ↪ K)
    (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
    (base : K → List Bool) (n m : Nat)
    (hn : base (control slots .variableCount) = encodeWord n)
    (hm : base (control slots .occurrenceCount) = encodeWord m)
    (clean : Clean slots base) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[2 * n + 3 * m + 10]
      (some ⟨some (labels .copyNOut), ((ambient, ()), register), base⟩) =
      some ⟨some (labels (evalStart .capacity)), ((ambient, ()), none),
        preparedBase slots base n m⟩ := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Clean, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.evalStart, OAI.MaxCutGames.Reduction.MachineAddressHeaders.capacity, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.preparedBase

  104. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.doubleTrace line 729

    Source documentation

    Physical doubling emits the vertex-count word and restores the capacity.

    theorem doubleTrace (slots : Layout k s d noiseCount ↪ K)
    (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
    (base : K → List Bool) (value : Nat)
    (hcap : base (control slots .capacity) = encodeWord value)
    (hscratch : base (control slots .scratch) = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[3 * value + 5]
      (some ⟨some (labels .doubleScan), ((ambient, ()), register), base⟩) =
      some ⟨some (labels .alphabet), ((ambient, ()), none),
        Function.update base (control slots .reversed)
          ((encodeWord (2 * value)).reverse ++ base (control slots .reversed))⟩ := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.capacity

  105. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.trace line 755

    Source documentation

    All arithmetic and header emission, with exact composed transition count.

    theorem trace (slots : Layout k s d noiseCount ↪ K)
    (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
    (base : K → List Bool) (n m : Nat)
    (hn : base (control slots .variableCount) = encodeWord n)
    (hm : base (control slots .occurrenceCount) = encodeWord m)
    (clean : Clean slots base) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps k s d noiseCount n m]
      (some ⟨some (labels .copyNOut), ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none), resultTapes slots base n m⟩ := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Clean, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.steps, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.resultTapes

  106. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.inTime line 837
  107. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.timePolynomial line 854

    Source documentation

    A fixed polynomial in the serialized input length bounds actual steps.

    def timePolynomial (k s d noiseCount : Nat) : Polynomial Nat :=
…
  108. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.steps_le_timePolynomial line 861
  109. abbrev OAI.MaxCutGames.Reduction.MachineAddressHeaders.Layout line 884
  110. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.arithmeticSlots line 888
  111. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.prefixLocal line 893
  112. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.prefixLocal_apply line 901
  113. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.prefixSlots line 910
  114. abbrev OAI.MaxCutGames.Reduction.MachineAddressHeaders.Label line 913
  115. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.statement line 915
  116. structure OAI.MaxCutGames.Reduction.MachineAddressHeaders.Clean line 922
  117. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.prefixResult_control line 929

    Source documentation

    Prefix writes only the read-copy and the two designated count tapes.

    theorem prefixResult_control (slots : Layout k s d noiseCount ↪ K) (base : K → List Bool)
    (n m : Nat) (c : Arithmetic.Control)
    (hn : c ≠ .variableCount) (hm : c ≠ .occurrenceCount) :
    Prefix.resultTapes (prefixSlots slots) base n m
      (Arithmetic.control (arithmeticSlots slots) c) =
    base (Arithmetic.control (arithmeticSlots slots) c) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.Control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Prefix.resultTapes, OAI.MaxCutGames.Reduction.MachineAddressHeaders.prefixSlots, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.arithmeticSlots

  118. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.prefixResult_coefficient line 939
  119. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.Clean.afterPrefix line 946
  120. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes line 960
  121. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.inTime line 965
  122. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.timePolynomial line 1011
  123. def OAI.MaxCutGames.Reduction.MachineAddressHeaders.inPolynomialTime line 1014
  124. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_source line 1035
  125. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_n line 1041
  126. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_m line 1048
  127. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_base line 1055
  128. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_capacity line 1060
  129. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_reversed line 1065
  130. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_other line 1074

    Source documentation

    No slot other than the read-copy, saved counts, B, cap, and output is changed.

    theorem resultTapes_other (slots : Layout k s d noiseCount ↪ K)
    (base : K → List Bool) (n m : Nat) (tape : K)
    (hread : tape ≠ slots (.inl 1))
    (hn : tape ≠ Arithmetic.control (arithmeticSlots slots) .variableCount)
    (hm : tape ≠ Arithmetic.control (arithmeticSlots slots) .occurrenceCount)
    (hB : tape ≠ Arithmetic.control (arithmeticSlots slots) .baseValue)
    (hcap : tape ≠ Arithmetic.control (arithmeticSlots slots) .capacity)
    (hout : tape ≠ Arithmetic.control (arithmeticSlots slots) .reversed) :
    resultTapes slots base n m tape = base tape := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineAddressHeaders.Layout, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.MaxCutGames.Reduction.MachineAddressHeaders.arithmeticSlots, OAI.MaxCutGames.Reduction.MachineAddressHeaders.capacity, OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes

  131. theorem OAI.MaxCutGames.Reduction.MachineAddressHeaders.resultTapes_readCopy line 1087