OAI/Computability/MaxCut/Machines/RawInitialMachineCleanup.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Actual cleanup of all six clause-field tapes followed by the global unary index increment. The output accumulator, unread input, and other caller tapes are preserved, and no additional finish instruction is assumed.

  1. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineCleanup.trace_trans_inline_RawInitialMachineCleanup line 19
  2. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineCleanup.incrementIndexTrace line 24

    Source documentation

    The index increment is exactly the one push in the actual global program.

    theorem incrementIndexTrace (base : Tape → List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[1]
      (some ⟨some .incrementIndex, state, base⟩) =
      some ⟨some .guard, state, Function.update base .index (true :: base .index)⟩ := by
…
  3. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineCleanup.cleanupTrace line 31

    Source documentation

    Clear six actual field tapes, increment the index, and return to the guard.

    theorem cleanupTrace {n : ℕ} (base : Tape → List Bool) (c : Target.Clause n)
    (suffix : List Bool) (i : ℕ)
    (hempty : ∀ j, base (.field j) = []) (hindex : base .index = encodeWord i)
    (incoming : State) :
    (MachineComposition.advance (TM2.step program))^[
        (encodeWords (Complexity.clauseWords c)).length + 7]
      (some ⟨some (.cleanupField 0), incoming, recordTapes base c suffix⟩) =
      some ⟨some .guard, (incoming.1, none),
        Function.update (Function.update base .input suffix) .index (encodeWord (i + 1))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Complexity.clauseWords

  4. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineCleanup.cleanupInTime line 114
  5. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineBody.trace_trans_inline_RawInitialMachineBody line 136
  6. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineBody.guardTrace_succ line 140
  7. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineBody.guardTrace_zero line 155
  8. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineBody.bodyTrace line 169
  9. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.tapes_inline_RawInitialMachineFinish line 224
  10. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.finishTapes line 232
  11. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.trace_trans_inline_RawInitialMachineFinish line 235
  12. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.trueRelationWords line 239
  13. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.dummyBits_length line 246
  14. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.update_reversed_inline_RawInitialMachineFinish line 254
  15. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.cleanupTrace_inline_RawInitialMachineFinish line 260
  16. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.resetReverseTrace_inline_RawInitialMachineFinish line 309
  17. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.update_finish_inline_RawInitialMachineFinish line 340
  18. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.copyFinishTrace_inline_RawInitialMachineFinish line 344
  19. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.closeDummyTailTrace_inline_RawInitialMachineFinish line 360
  20. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.closeDummyReverseTrace_inline_RawInitialMachineFinish line 369
  21. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.dummyRelationTrace_inline_RawInitialMachineFinish line 378
  22. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.dummyTrace line 390

    Source documentation

    The three actual prefix scans and three emitting transitions append the complete dummy row.

    theorem dummyTrace (n m : Nat) (rev : List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[2 * n + 4 * m + 9]
      (some ⟨some (.scan .dummyVariables), state, finishTapes n m rev⟩) =
      some ⟨some (.cleanupFinal 0), (state.1, none),
        finishTapes n m ((encodeWords (RawInitialRows.dummyWords n m)).reverse ++ rev)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.finishTapes, OAI.MaxCutGames.Foundations.PCP.RawInitialRows.dummyWords

  23. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.finishTrace line 428

    Source documentation

    Exact final execution, including all tape cleanup and the canonical halt state.

    theorem finishTrace (n m : Nat) (rev : List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[
        3 * n + 5 * m + 17 + (encodeWords (RawInitialRows.dummyWords n m)).length + rev.length]
      (some ⟨some (.scan .dummyVariables), state, finishTapes n m rev⟩) =
      some (haltList machine (rev.reverse ++ encodeWords (RawInitialRows.dummyWords n m))) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialRows.dummyWords, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.finishTapes

  24. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineFinish.finishInTime line 446
  25. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoop.finalSigns line 469
  26. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoop.trace_trans_inline_RawInitialMachineLoop line 474
  27. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoop.empty_loopTapes line 478
  28. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoop.loopTrace line 485

    Source documentation

    The complete actual loop: every clause is read once, emits six rows, and leaves clean field tapes before the next guard. The final zero guard is included.

    theorem loopTrace {n : Nat} (i : Nat) (cs : List (Clause n))
    (rev : List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[loopTime i cs]
      (some ⟨some .guard, state, loopTapes n i cs.length (clauseInput cs) rev⟩) =
      some ⟨some (.scan .dummyVariables), (finalSigns state.1 cs, none),
        finishTapes n (i + cs.length) ((encodeWords (clauseOutput n i cs)).reverse ++ rev)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoop.finalSigns

  29. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoop.loopInTime line 509
  30. theorem OAI.MaxCutGames.Foundations.PCP.MachineRawInitialTable.trace_trans_inline_MachineRawInitialTable line 530
  31. def OAI.MaxCutGames.Foundations.PCP.MachineRawInitialTable.prefixBits line 534
  32. theorem OAI.MaxCutGames.Foundations.PCP.MachineRawInitialTable.outputBits line 538
  33. theorem OAI.MaxCutGames.Foundations.PCP.MachineRawInitialTable.machineTrace line 545
  34. def OAI.MaxCutGames.Foundations.PCP.MachineRawInitialTable.outputsInTime line 571
  35. def OAI.MaxCutGames.Foundations.PCP.MachineRawInitialTable.computableInPolyTime line 579
  36. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Buffer line 611
  37. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.readUnarySlots line 619

    Source documentation

    Read fixed register slots from the actual unary 0/1 word encoding. Each slot consumes one symbol for false and two symbols for true.

    def readUnarySlots (source : K) : List (Fin N) →
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) →
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N)
  | [], next => next
  | i :: slots, next =>
      .pop source (fun state head =>
        (state.1, Function.update state.2 i (head.getD false)))
        (.branch (fun state => state.2 i)
          (.pop source (fun state _ => state) (readUnarySlots source slots next))
          (readUnarySlots source slots next))

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Buffer

  38. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBits line 630
  39. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBits_eq_encodeWords line 633
  40. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBits_length_le line 640
  41. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.statementPushBound_readUnarySlots line 650
  42. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnarySlots line 662

    Source documentation

    Exact stack and register semantics, retaining every unread suffix bit.

    theorem stepAux_readUnarySlots (source : K) (slots : List (Fin N))
    (next : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N))
    (ambient : σ) (bits buffer : Buffer N) (tapes : K → List Bool)
    (suffix : List Bool) :
    TM2.stepAux (readUnarySlots source slots next) (ambient, buffer)
        (Function.update tapes source (unaryBits slots bits ++ suffix)) =
      TM2.stepAux next (ambient, MachineFixedBlockMap.fill slots bits buffer)
        (Function.update tapes source suffix) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Buffer, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.readUnarySlots, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBits, OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.fill

  43. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnaryAll line 686
  44. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBlockMapAt line 701

    Source documentation

    A fixed table lookup or fixed pattern permutation can follow immediately after the physical unary decoding, with one genuine finite TM2 transition.

    def unaryBlockMapAt {M : Nat} (source destination : K) (F : Buffer N → Buffer M)
    (exit : Option Λ) : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Buffer

  45. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.stepAux_unaryBlockMapAt line 709
  46. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.step_unaryBlockMapAt line 724
  47. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBlockInTime line 737
  48. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.unaryBits_relation line 754
  49. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.readerStateEquiv line 767

    Source documentation

    Merely rearranges finite registers to match the affine-emitter state. No tape content or unbounded integer is moved into the internal state.

    def readerStateEquiv (σ : Type) (N : Nat) :
    (((σ × Unit) × Option Bool) × Buffer N) ≃ (((σ × Buffer N) × Unit) × Option Bool) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Buffer

  50. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.State line 778
  51. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.readRelationAt line 780
  52. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.stepAux_readRelationAt line 785
  53. inductive OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape line 806
  54. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList line 811
  55. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_getElem?_ctorIdx_eq line 814
  56. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_nodup line 818
  57. instance OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.(instance at line 820) line 820
  58. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient line 824
  59. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan line 825
  60. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.values line 827
  61. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan line 831

    Source documentation

    Output variable count and output clause count, in the checked CNF codec.

    def headerPlan : Plan :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan

  62. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_length line 835
  63. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_bits line 838
  64. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.source line 846
  65. inductive OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Label line 849
  66. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guard line 861
  67. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program line 870

    Source documentation

    The actual finite program. All graph-dependent naturals remain on unary stacks. The only buffered graph data is one fixed 4096-bit relation table.

    def program (headerPlan rowPlan : Plan) :
    Label headerPlan.length rowPlan.length →
      TM2.Stmt (fun _ : Tape => Bool) (Label headerPlan.length rowPlan.length) (State Unit)
  | .copyFirst => Reduction.MachineTransfer.loopAt .input .scratch id false .copyFirst
      (some .copySecond)
  | .copySecond => MachineCopy.forkLoop .scratch .input .archive false .copySecond
      (some .startVertices)
  | .startVertices => Hastad.SourceMachine.fieldStart .vertices .readVertices
  | .readVertices => Hastad.SourceMachine.fieldLoop .input .vertices .readVertices (some .startDarts)
  | .startDarts => Hastad.SourceMachine.fieldStart .darts .readDarts
  | .readDarts => Hastad.SourceMachine.fieldLoop .input .darts .readDarts (some .seedIndex)
  | .seedIndex => .push .rowIndex (fun _ => false)
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Label, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.State, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop, OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStart, OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldLoop

  68. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.machine line 917
  69. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles line 928
  70. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_injective line 932
  71. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime line 937

    Source documentation

    The head-access call is part of this concrete program, with its actual finite labels and framed tape effects. Its data are read from the table.

    def headPhaseInTime (headerPlan rowPlan : Plan) (base : Tape → List Bool)
    (table : GenericGraphTables.Table 64) (e : Fin table.darts)
    (hTable : base .archive = GenericGraphTables.tableBits table)
    (hReverse : base .reverseIndex = encodeWord (Lookup.headIndex table e).val)
    (hHead : base .head = []) (hScratch : base .scratch = []) (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan rowPlan))
      ⟨some .headTableFirst, ((ambient, ()), none), base⟩
      (some ⟨some .readRelation, ((ambient, ()), none),
        Lookup.headLookupTapes headRoles base table e⟩)
      (Lookup.headTimePolynomial.eval (GenericGraphTables.tableBits table).length) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles

  72. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes line 953
  73. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes_operands line 966
  74. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_input line 973
  75. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_tail line 980
  76. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_head line 987
  77. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_accumulator line 994
  78. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_rowIndex line 1001
  79. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_scratch line 1009
  80. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_accumulator line 1012