OAI/Computability/MaxCut/Machines/MachineExpanderFamilyAffine.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Actual lookup and reversal phases of the expander row program

The Boolean phase selector chooses the first or second occurrence of the same preserving lookup. The selected word is proved to be the actual stored reverse index of the supplied graph row. All execution facts follow from the concrete program statements; no phase execution is assumed.

  1. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_scratch line 11
  2. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_destination line 14
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affine_scratch_ne_destination line 17
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes line 21

    Source documentation

    Exact final dependent tape family, with all other tape contents retained.

    def affineResultTapes (d : Nat) (phase : AffinePhase)
    (base : (tape : Tape) → List (Alphabet tape)) (n : Nat) :
    (tape : Tape) → List (Alphabet tape) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet

  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_other line 28
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_source line 34
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_scratch line 39
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_destination line 44
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseBoolTrace line 54

    Source documentation

    The concrete Boolean view is pulled into unary-affine state coordinates, executed from its actual statements, and transported back without extra steps.

    theorem affinePhaseBoolTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (phase : AffinePhase) (base : Tape → List Bool)
    (n : Nat) (suffix : List Bool)
    (sourceWord : base (affineSource phase) = encodeWord n ++ suffix)
    (scratchEmpty : base (.inr .unaryScratch) = []) (state : State ρ d) :
    (advance (TM2.step (boolView positive H growth)))^[2 * (n + 1) + 1]
      (some ⟨some (.inr (.affine phase .seed)), state, base⟩) =
      some ⟨some (affineExit d phase), clearRegister state,
        Function.update base (affineDestination phase)
          (encodeWord (affineCoefficient d phase * n) ++ base (affineDestination phase))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineSource, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolView, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineExit, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineDestination, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineCoefficient

  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseTrace line 101

    Source documentation

    Actual family-program execution. Alphabet conversion is static equality transport; the transition count is exactly the checked unary-affine count.

    theorem affinePhaseTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (phase : AffinePhase)
    (base : (tape : Tape) → List (Alphabet tape)) (n : Nat) (suffix : List Bool)
    (sourceWord : toBoolTapes base (affineSource phase) = encodeWord n ++ suffix)
    (scratchEmpty : base (.inr .unaryScratch) = []) (state : State ρ d) :
    (advance (TM2.step (program positive H growth)))^[2 * (n + 1) + 1]
      (some ⟨some (.inr (.affine phase .seed)), state, base⟩) =
      some ⟨some (affineExit d phase), clearRegister state,
        affineResultTapes d phase base n⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineSource, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineExit, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes

  11. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseInTime line 116
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.copyCountInTime line 129
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.multiplySizeInTime line 146
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emitSteps line 171

    Source documentation

    One scaled scan/restore, one bounded offset, the delimiter, and final jump.

    def emitSteps (n : Nat) : Nat := 3 * (n + 1) + 6
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.affinePlan_bits line 173
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.affinePlan_steps line 184
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord line 192

    Source documentation

    Every tape except the accumulator is literally retained.

    def emittedWord {K : Type} [DecidableEq K]
    (target : K) (base : K → List Bool) (value : Nat) : K → List Bool :=
…
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord_target line 196
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord_other line 201
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.program_firstEmit line 209
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.program_secondEmit line 215
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.program_outputEmit line 221
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstEmitTraceAt line 233

    Source documentation

    The code premise identifies concrete statements in a caller's program; it does not assume any phase execution.

    theorem firstEmitTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (portsInjective : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (atLabels : ∀ l, target (labels l) = statement positive H ports labels exit l)
    (n : Nat) (base : K → List Bool)
    (source : base (ports .inputVertex) = encodeWord n)
    (scratch : base (ports .emitScratch) = [])
    (ambient : Ambient ρ d × Fin (degree d)) :
    (MachineComposition.advance (TM2.step target))^[emitSteps n]
      (some ⟨some (labels (.firstEmit (Emitter.labelAt 3 _ 0 .entry))),
        ((ambient, ()), none), base⟩) =
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Ambient, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emitSteps

  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondEmitTraceAt line 264
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.outputEmitTraceAt line 295
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTimeAt line 326
  27. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTimeAt line 344
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTimeAt line 362
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstEmitTrace line 382
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondEmitTrace line 394
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.outputEmitTrace line 406
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTime line 418
  33. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTime line 430
  34. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTime line 442
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel line 471
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel line 475
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel line 478
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhasePort line 481
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress line 484
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress_eq_rowIndex line 487
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupTape_injective line 495
  42. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes line 500

    Source documentation

    The exact cleaned tape state produced by either lookup.

    def lookupResultTapes (ports : Tape → K) (base : K → List Bool)
    (value : Nat) (indexSuffix : List Bool) : K → List Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape

  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_index line 505
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_work line 513
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_output line 519
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_other line 526

    Source documentation

    Every tape outside the query, work, and lookup-output roles is retained.

    theorem lookupResultTapes_other (ports : Tape → K) (base : K → List Bool)
    (value : Nat) (indexSuffix : List Bool) (p : K)
    (hi : p ≠ ports .queryIndex) (hw : p ≠ ports .lookupWork)
    (ho : p ≠ ports .lookupOutput) :
    lookupResultTapes ports base value indexSuffix p = base p := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes

  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_table line 533
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_restore line 539
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseTrace line 566

    Source documentation

    Actual first/second lookup execution on a stored graph row. The selected reverse index is obtained from rotationWords_getElem?, not a caller premise.

    theorem lookupPhaseTrace :
    (advance (TM2.step target))^[MachinePreservingLookupClean.steps
        (rotationWords G) (rowIndex v (degree d) x).val]
      (some ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))),
        (ambient, register), base⟩) =
      some ⟨some (labels (scanPhaseLabel second)), (ambient, none),
        lookupResultTapes ports base (reverseIndex G (rowIndex v (degree d) x)).val
          indexSuffix⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.steps, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes

  50. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime line 590

    Source documentation

    A linear bound in the original encoded table length for the same actual phase. This includes the copy, restore, lookup, and residual cleanup.

    def lookupPhaseInTime :
    StateTransition.EvalsToInTime (TM2.step target)
      ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))),
        (ambient, register), base⟩
      (some ⟨some (labels (scanPhaseLabel second)), (ambient, none),
        lookupResultTapes ports base (reverseIndex G (rowIndex v (degree d) x)).val
          indexSuffix⟩)
      (6 * (encodeWords (rotationWords G)).length + 4) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace line 618

    Source documentation

    The reversal consumes the reverse query word and prepends its forward encoding to the index tape, retaining every other tape and finite state.

    theorem reversePhaseTrace :
    (advance (TM2.step target))^[(base (ports .queryReverse)).length + 1]
      (some ⟨some (labels (reversePhaseLabel second)), (ambient, register), base⟩) =
      some ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))), (ambient, none),
        Reduction.MachineTransfer.tapesAt (ports .queryReverse) (ports .queryIndex) base []
          ((base (ports .queryReverse)).reverse ++ base (ports .queryIndex))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt

  52. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseInTime line 634
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace_unary line 648

    Source documentation

    Reversing an actual emitted unary field takes exactly index + 2 steps. This includes consuming the field's delimiter and leaving the reversal loop.

    theorem reversePhaseTrace_unary (index : Nat) (suffix : List Bool)
    (queryWord : base (ports .queryReverse) = (encodeWord index).reverse)
    (indexWord : base (ports .queryIndex) = suffix) :
    (advance (TM2.step target))^[index + 2]
      (some ⟨some (labels (reversePhaseLabel second)), (ambient, register), base⟩) =
      some ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))), (ambient, none),
        Reduction.MachineTransfer.tapesAt (ports .queryReverse) (ports .queryIndex) base []
          (encodeWord index ++ suffix)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.MaxCutGames.Reduction.MachineTransfer.tapesAt

  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_zero line 668
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_one line 669
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_two line 670
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_three line 671
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_four line 672
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_five line 673
  60. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes line 677
  61. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps line 690
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_eq_sum line 699
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_dirty line 703
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_other line 710

    Source documentation

    Every tape outside the six named work roles keeps its exact contents.

    theorem cleanupTapes_other (ports : Tape → K) (base : K → List Bool) (k : K)
    (outside : ∀ i : Fin 6, k ≠ ports (dirtyTape i)) :
    cleanupTapes ports base k = base k := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes

  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_table line 727
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_inputVertex line 732
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_output line 737
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.join_trace_inline_MachineExpanderRowCleanup line 742
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupOneTraceAt line 749

    Source documentation

    One cleanup phase follows the actual drain instruction at its placed label.

    theorem cleanupOneTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (i : Fin 6) (base : K → List Bool) (state : State ρ d) :
    (advance (TM2.step target))^[((base (ports (dirtyTape i))).length + 1)]
      (some ⟨some (labels (.cleanup i)), state, base⟩) =
      some ⟨some (if hi : i.val + 1 < 6 then labels (.cleanup ⟨i.val + 1, hi⟩)
          else labels .done),
        (state.1, none), Function.update base (ports (dirtyTape i)) []⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape

  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTraceAt line 768

    Source documentation

    All six phases execute in the common program, with exactly the sum of the six initial word lengths plus one empty-branch transition per tape.

    theorem cleanupTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (distinct : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (state : State ρ d) :
    (advance (TM2.step target))^[cleanupSteps ports base]
      (some ⟨some (labels (.cleanup 0)), state, base⟩) =
      some ⟨some (labels .done), (state.1, none), cleanupTapes ports base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes

  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.doneStepAt line 794

    Source documentation

    The done label transfers control without inspecting or modifying any tape.

    theorem doneStepAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (state : State ρ d) :
    TM2.step target ⟨some (labels .done), state, base⟩ = some ⟨exit, state, base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement

  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupExitTraceAt line 805

    Source documentation

    Cleanup followed by the actual done-to-caller transition.

    theorem cleanupExitTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (distinct : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (state : State ρ d) :
    (advance (TM2.step target))^[cleanupSteps ports base + 1]
      (some ⟨some (labels (.cleanup 0)), state, base⟩) =
      some ⟨exit, (state.1, none), cleanupTapes ports base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes

  73. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.initializedTapes line 822
  74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.initializeStepAt line 832

    Source documentation

    Initialization physically pushes four delimiters and resets the bit register.

    theorem initializeStepAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (distinct : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (state : State ρ d) :
    TM2.step target ⟨some (labels .initialize), state, base⟩ =
      some ⟨some (labels (.firstEmit (PCP.AlphabetTable.Emitter.labelAt 3 _ 0 .entry))),
        (state.1, none), initializedTapes ports base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.initializedTapes

  75. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes line 845
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.clearQueryStepAt line 852

    Source documentation

    The query-clear phase removes one symbol from each of its two tapes and preserves the complete finite state and every other tape.

    theorem clearQueryStepAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (distinct : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (code : ∀ label, target (labels label) = statement positive H ports labels exit label)
    (base : K → List Bool) (state : State ρ d) :
    TM2.step target ⟨some (labels .clearQuery), state, base⟩ =
      some ⟨some (labels (.secondEmit (PCP.AlphabetTable.Emitter.labelAt 3 _ 0 .entry))),
        state, clearedQueryTapes ports base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes