OAI/Computability/UniqueGames/Machines/MachineExpanderFamilyTransferLemmas.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Actual family-table installation and counter cleanup

Checked physical drain and transfer loops are placed in the family program through its finite register equivalence. Alphabet equality transports their actual traces back to the dependent alphabet of the full family machine.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.controlStatementInverse line 24
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.controlTrace line 32

    Source documentation

    Static state-coordinate transport preserves every actual transition.

    theorem controlTrace {K Λ σ τ : Type} {Γ : K → Type} [DecidableEq K]
    (states : σ ≃ τ) (target : Λ → TM2.Stmt Γ Λ τ)
    (n : Nat) (start finish : TM2.Cfg Γ Λ σ)
    (run : (advance (TM2.step (MachineControl.program (Equiv.refl Λ) states.symm target)))^[n]
      (some start) = some finish) :
    (advance (TM2.step target))^[n]
      (some (MachineControl.configuration id states start)) =
      some (MachineControl.configuration id states finish) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.configuration

  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.controlDrainTrace line 56
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.controlTransferTrace line 75
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister line 102
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.registerStates_reset line 105
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister_idempotent line 109
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller_clearRegister line 112
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister_position line 115
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister_register line 118
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolTraceActual line 124

    Source documentation

    The Boolean view is the same actual program under alphabet equality.

    theorem boolTraceActual (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (n : Nat)
    (start finish : TM2.Cfg BoolAlphabet (Label d) (State ρ d))
    (run : (advance (TM2.step (boolView positive H growth)))^[n] (some start) = some finish) :
    (advance (TM2.step (program positive H growth)))^[n]
      (some (MachineAlphabetTransport.configuration alphabet_eq.symm start)) =
      some (MachineAlphabetTransport.configuration alphabet_eq.symm finish) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration

  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.drainBoolTrace line 135
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.transferBoolTrace line 152
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installedTapes line 176

    Source documentation

    Only these four tape words change during installation.

    def installedTapes (base : Tape → List Bool) (newWord : List Bool) : Tape → List Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape

  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes line 183
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installTableBoolTrace line 186
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cleanupCountersBoolTrace line 245
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installTableTrace line 265

    Source documentation

    Actual dependent-alphabet trace for draining the old table, installing the new forward table by two physical reversals, and clearing the old size word.

    theorem installTableTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : (tape : Tape) → List (Alphabet tape))
    (newWord : List Bool) (resultWord : toBoolTapes base resultTape = newWord)
    (reverseEmpty : toBoolTapes base (.inr .tableReverse) = []) (state : State ρ d) :
    (advance (TM2.step (program positive H growth)))^[
        (toBoolTapes base tableTape).length + 2 * newWord.length +
          (toBoolTapes base (.inr .currentSize)).length + 4]
      (some ⟨some (.inr .clearOldTable), state, base⟩) =
      some ⟨some (.inr (.affine .multiplySize .seed)), clearRegister state,
        fromBoolTapes (installedTapes (toBoolTapes base) newWord)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.resultTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installedTapes

  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cleanupCountersTrace line 280

    Source documentation

    After the checked affine phase, both table-loop counters are physically drained and the actual family level guard is reached.

    theorem cleanupCountersTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : (tape : Tape) → List (Alphabet tape))
    (state : State ρ d) :
    (advance (TM2.step (program positive H growth)))^[
        (toBoolTapes base inputVertexTape).length + (toBoolTapes base vertexCountTape).length + 2]
      (some ⟨some (.inr .drainInputVertex), state, base⟩) =
      some ⟨some (.inr .levelGuard), clearRegister state,
        fromBoolTapes (cleanedCounterTapes (toBoolTapes base))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.inputVertexTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.vertexCountTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes

  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installTableInTime line 291
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cleanupCountersInTime line 306
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_scratch line 320
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_destination line 323
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affine_scratch_ne_destination line 326
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes line 330

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet

  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_other line 337
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_source line 343
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_scratch line 348
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_destination line 353
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affinePhaseBoolTrace line 363

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineSource, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineExit, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineDestination, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineCoefficient

  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affinePhaseTrace line 410

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineSource, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineExit, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineResultTapes

  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affinePhaseInTime line 425
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.copyCountInTime line 438
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.multiplySizeInTime line 455
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller_initialState line 476
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller_normalizeState line 479
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister_initialState line 482
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_update_level line 487

    Source documentation

    The guard changes only the physical remaining-level word.

    theorem boundaryTapes_update_level (remaining current next : Nat)
    (word suffix : List Bool) :
    Function.update (boundaryTapes remaining current word suffix)
      (.inr .remainingLevel) (encodeWord next ++ suffix) =
      boundaryTapes next current word suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boundaryTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes_initialize line 500

    Source documentation

    The two literal prefixes install the actual level-zero table and unary one.

    theorem initialTapes_initialize (level : Nat) (suffix : List Bool) :
    Function.update
      (Function.update (initialTapes level suffix) tableTape (initialEncoding d))
      (.inr .currentSize) (encodeWord 1) =
      boundaryTapes level 1 (initialEncoding d) suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boundaryTapes

  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.actualStep_of_boolStep line 518

    Source documentation

    Static alphabet transport preserves this actual single transition.

    theorem actualStep_of_boolStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d)
    (start finish : TM2.Cfg BoolAlphabet (Label d) (State ρ d))
    (run : TM2.step (boolView positive H growth) start = some finish) :
    TM2.step (program positive H growth)
      (MachineAlphabetTransport.configuration alphabet_eq.symm start) =
      some (MachineAlphabetTransport.configuration alphabet_eq.symm finish) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration

  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.bool_initializeStep line 531
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_succStep line 544
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_zeroStep line 557
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.bool_doneStep line 569
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initializeStep line 578

    Source documentation

    The literal initialization executes in one transition of the actual program.

    theorem initializeStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : ∀ tape, List (Alphabet tape)) (state : State ρ d) :
    TM2.step (program positive H growth) ⟨some (.inr .initialize), state, base⟩ =
      some ⟨some (.inr .levelGuard), normalizeState positive H state,
        Function.update
          (Function.update base tableTape (initialEncoding d ++ base (.inl (.inl .table))))
          (.inr .currentSize) (encodeWord 1 ++ base (.inr .currentSize))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.normalizeState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelGuard_succStep line 591

    Source documentation

    A positive level physically loses one true bit, retaining its delimiter and suffix.

    theorem levelGuard_succStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (remaining : Nat) (suffix : List Bool)
    (counter : base (.inr .remainingLevel) = encodeWord (remaining + 1) ++ suffix) :
    TM2.step (program positive H growth) ⟨some (.inr .levelGuard), state, base⟩ =
      some ⟨some (.inr (.affine .copyCount .seed)), clearRegister state,
        Function.update base (.inr .remainingLevel) (encodeWord remaining ++ suffix)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister

  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelGuard_zeroStep line 605

    Source documentation

    The zero delimiter is retained when the family loop enters its final halt.

    theorem levelGuard_zeroStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (suffix : List Bool)
    (counter : base (.inr .remainingLevel) = encodeWord 0 ++ suffix) :
    TM2.step (program positive H growth) ⟨some (.inr .levelGuard), state, base⟩ =
      some ⟨some (.inr .done), clearRegister state, base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.clearRegister

  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.doneStep line 615
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialize_boundaryStep line 623
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_succStep line 639
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_zeroStep line 650
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_boundaryState line 678
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.prepareState_boundaryState line 682
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister_boundaryState line 687
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_prepareState line 692
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_resetState line 695
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_clearRegister line 698
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_advancePositionState line 701
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_resetPositionState line 704
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.nextPosition_val_of_lt line 707
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes_update_count line 712

    Source documentation

    Replacing the count word leaves the entire row frame and result unchanged.

    theorem boundaryTapes_update_count (vertex remaining next : Nat)
    (oldTable output countSuffix result : List Bool) :
    Function.update (boundaryTapes vertex remaining oldTable output countSuffix result)
      (.inr .vertexCount) (encodeWord next ++ countSuffix) =
      boundaryTapes vertex next oldTable output countSuffix result := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes_increment_vertex line 723

    Source documentation

    The last row's one actual push increments the unary vertex word.

    theorem boundaryTapes_increment_vertex (vertex remaining : Nat)
    (oldTable output countSuffix result : List Bool) :
    Function.update (boundaryTapes vertex remaining oldTable output countSuffix result)
      (.inl .inputVertex) (true :: encodeWord vertex) =
      boundaryTapes (vertex + 1) remaining oldTable output countSuffix result := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initialTapes_initialize line 736
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initializeStep line 750
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initialize_boundaryStep line 759
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexGuard_succStep line 775

    Source documentation

    A positive vertex counter is physically decremented; its suffix remains.

    theorem vertexGuard_succStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (remaining : Nat) (suffix : List Bool)
    (counter : base (.inr .vertexCount) = encodeWord (remaining + 1) ++ suffix) :
    TM2.step (program positive H) ⟨some (.inr .vertexGuard), state, base⟩ =
      some ⟨some (.inr .prepareRow), clearRegister state,
        Function.update base (.inr .vertexCount) (encodeWord remaining ++ suffix)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister

  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexGuard_zeroStep line 788

    Source documentation

    The zero delimiter is retained when the loop enters output reversal.

    theorem vertexGuard_zeroStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (suffix : List Bool)
    (counter : base (.inr .vertexCount) = encodeWord 0 ++ suffix) :
    TM2.step (program positive H) ⟨some (.inr .vertexGuard), state, base⟩ =
      some ⟨some (.inr .reverseOutput), clearRegister state, base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister

  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_succStep line 799
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_zeroStep line 812
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.prepareRowStep line 823

    Source documentation

    Preparing a row modifies finite control only, preserving every tape.

    theorem prepareRowStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d) :
    TM2.step (program positive H) ⟨some (.inr .prepareRow), state, base⟩ =
      some ⟨some (.inl .initialize), prepareState positive H state, base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.prepareState

  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.afterRow_moreStep line 832

    Source documentation

    A nonfinal row advances the finite position without changing tapes.

    theorem afterRow_moreStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (more : state.2.val + 1 < rowFactor d) :
    TM2.step (program positive H) ⟨some (.inr .afterRow), state, base⟩ =
      some ⟨some (.inr .prepareRow), advancePositionState positive state, base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.advancePositionState

  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.afterRow_lastStep line 842

    Source documentation

    The final row increments the tape vertex and resets the finite position.

    theorem afterRow_lastStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (last : ¬ state.2.val + 1 < rowFactor d) :
    TM2.step (program positive H) ⟨some (.inr .afterRow), state, base⟩ =
      some ⟨some (.inr .vertexGuard), resetPositionState positive state,
        Function.update base (.inl .inputVertex) (true :: base (.inl .inputVertex))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.resetPositionState

  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.afterRow_last_boundaryStep line 852
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.reverseOutput_consStep line 872

    Source documentation

    One reversal step moves an actual symbol and preserves the finite position.

    theorem reverseOutput_consStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (symbol : Bool) (word : List Bool) (source : base (.inl .output) = symbol :: word) :
    TM2.step (program positive H) ⟨some (.inr .reverseOutput), state, base⟩ =
      some ⟨some (.inr .reverseOutput), ((state.1.1, some symbol), state.2),
        Function.update (Function.update base (.inl .output) word)
          (.inr .result) (symbol :: base (.inr .result))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program

  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.reverseOutput_nilStep line 884
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.doneStep line 896