OAI/Computability/UniqueGames/Machines/MachineCompositionLemmas.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

Execution transport and polynomial budget arithmetic for genuine TM2 sequential composition. These lemmas preserve actual transition witnesses. The four-phase lemma requires all phases to be executions of the same combined program; it is not a replacement for constructing that program and proving its tape handoffs.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance line 17
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance_none line 20
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance_some line 23
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance_iterate_none line 26
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 32
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.liftExecutionInTime line 56
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 70
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.embeddedExecution line 79

    Source documentation

    The checked disjoint-stack embedding transports a complete successful run with no additional transitions, including its final jump to a bridge label.

    def embeddedExecution {K E Λ Λextra σ τ : Type} {Γ : K → Type} {Δ : E → Type}
    [DecidableEq K] [DecidableEq E]
    (haltTarget : Option (Λ ⊕ Λextra)) (extraState : τ)
    (extraTapes : ∀ e, List (Δ e))
    (source : Λ → Turing.TM2.Stmt Γ Λ σ)
    (extra : Λextra → Turing.TM2.Stmt (MachineEmbedding.Alphabet Γ Δ)
      (Λ ⊕ Λextra) (σ × τ))
    {start finish : Turing.TM2.Cfg Γ Λ σ} {budget : Nat}
    (execution : StateTransition.EvalsToInTime (Turing.TM2.step source)
      start (some finish) budget) :
    StateTransition.EvalsToInTime (Turing.TM2.step (MachineEmbedding.program haltTarget source extra))
      (MachineEmbedding.configuration haltTarget extraState extraTapes start)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.configuration

  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 97
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.compositionPolynomial line 107

    Source documentation

    Two reversal transfers each consume intermediateLength + 1 transitions.

    noncomputable def compositionPolynomial (first second intermediate : Polynomial Nat) : Polynomial Nat :=
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.compositionBudget_le line 110
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.fourPhaseExecution line 121
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.tapes line 160
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.statement line 162
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration line 164
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.program line 166
  17. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.castStatement line 169
  18. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.castConfiguration line 170
  19. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.castProgram line 171
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.tapes_rfl line 173
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.statement_rfl line 174
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_rfl line 175
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.program_rfl line 176
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.program_apply line 178
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.statement_roundtrip line 181
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.statement_symm_roundtrip line 184
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_roundtrip line 187
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_symm_roundtrip line 190
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.program_roundtrip line 193
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.program_symm_roundtrip line 196
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.tapes_roundtrip line 199
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.tapes_symm_roundtrip line 202
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_label line 205
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_state line 208
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_tapes line 211
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration_mk line 214
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.map_configuration_rfl line 218
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.stepAux_simulation line 223
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.step_simulation line 228
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.trace_transport line 235

    Source documentation

    Exact conjugacy of every finite trace, including a none endpoint.

    theorem trace_transport (h : Γ = Δ) (source : Λ → Stmt Γ Λ σ)
    (n : Nat) (start : Option (Cfg Γ Λ σ)) :
    (MachineComposition.advance (step (program h source)))^[n]
      (start.map (configuration h)) =
      ((MachineComposition.advance (step source))^[n] start).map (configuration h) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration

  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.successfulTrace line 243
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.executionInTime line 251
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.executionInTime_steps line 263
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime line 268
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime_steps line 274
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.Label line 296
  47. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.labelFintype line 300
  48. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.labelDecidableEq line 308
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.entry line 319
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.instruction line 326
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.resultOf line 337
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.steps line 341
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.trace line 349

    Source documentation

    This generic composition lemma retains the local execution obligations. Concrete callers discharge them with the rotor, comparison and row programs.

    theorem trace (program : Λ → TM2.Stmt Γ Λ σ)
    (invariant : Data → Prop) (state : Data → σ) (tapes : Data → ∀ k, List (Γ k))
    (commands : List Command)
    (localInvariant : ∀ command ∈ commands, ∀ data, invariant data →
      invariant (result command data))
    (localTrace : ∀ command ∈ commands, ∀ (labels : LocalLabel command → Λ) (exit : Option Λ),
      (∀ l, program (labels l) = localInstruction command labels exit l) →
      ∀ data, invariant data →
      (advance (TM2.step program))^[cost command data]
        (some ⟨some (labels (main command)), state data, tapes data⟩) =
      some ⟨exit, state (result command data), tapes (result command data)⟩)
    (labels : Label LocalLabel commands → Λ) (exit : Option Λ)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteSequence.Label

  54. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer line 410
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer line 412
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.readSlots line 418
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.fill line 428

    Source documentation

    Proof-level description of the finite register updates.

    def fill (slots : List (Fin N)) (bits buffer : Buffer N) : Buffer N :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer

  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.fill_apply line 431
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.fill_all line 442
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.stepAux_readSlots line 450

    Source documentation

    The input symbols are physically popped; the remaining suffix is exact.

    theorem stepAux_readSlots (src : 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 (readSlots src slots next) (ambient, buffer)
        (Function.update tapes src (slots.map bits ++ suffix)) =
      TM2.stepAux next (ambient, fill slots bits buffer)
        (Function.update tapes src suffix) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.readSlots, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.fill

  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.stepAux_readAll line 466
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_readSlots line 480
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.writeSlots line 490

    Source documentation

    The slot list is a fixed part of the syntax; each instruction reads only the finite internal state. Push order is reversed on the stack.

    def writeSlots {M : Nat} (dst : K) (emit : σ → Buffer M) : List (Fin M) →
    TM2.Stmt (fun _ : K => Bool) Λ σ → TM2.Stmt (fun _ : K => Bool) Λ σ
  | [], next => next
  | i :: slots, next => .push dst (fun state => emit state i) (writeSlots dst emit slots next)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer

  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.stepAux_writeSlots line 495
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_writeSlots line 510
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.blockStmt line 528

    Source documentation

    Read a fixed block, write its fixed finite transformation, reset the local register, and execute the next finite statement.

    def blockStmt (src dst : K) (F : Buffer N → Buffer M)
    (next : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N)) :
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer

  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.finishAt line 535
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.blockMapAt line 540
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockStmt line 544
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockMapAt line 551
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockStmt line 559
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockMapAt line 575

    Source documentation

    The suffix and all unmentioned tapes are preserved, and the local register is reset, in the actual transition semantics.

    theorem stepAux_blockMapAt (src dst : K) (F : Buffer N → Buffer M)
    (exit : Option Λ) (hne : src ≠ dst) (bits : Buffer N) (suffix : List Bool)
    (state : σ × Buffer N) (tapes : K → List Bool)
    (hinput : tapes src = List.ofFn bits ++ suffix) :
    TM2.stepAux (blockMapAt src dst F exit) state tapes =
      { l := exit, var := (state.1, emptyBuffer N),
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.blockMapAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer

  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.step_blockMapAt line 587

    Source documentation

    Placement in an arbitrary program gives one actual TM2 transition.

    theorem step_blockMapAt (src dst : K) (F : Buffer N → Buffer M)
    (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N))
    (label : Λ) (hprogram : program label = blockMapAt src dst F exit)
    (hne : src ≠ dst) (bits : Buffer N) (suffix : List Bool)
    (state : σ × Buffer N) (tapes : K → List Bool)
    (hinput : tapes src = List.ofFn bits ++ suffix) :
    TM2.step program { l := some label, var := state, stk := tapes } =
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.blockMapAt

  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.machine line 606

    Source documentation

    The fixed block map is also a concrete machine with two Boolean tapes and a finite register, independently of any ambient placement.

    def machine {N M : Nat} (F : Buffer N → Buffer M) : FinTM2 where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.Buffer

  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.machine_statementPushBound line 617
  76. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement line 645

    Source documentation

    Translate instructions using the checked recursive translator, keeping every tape and destination label unchanged.

    abbrev statement (e : σ ≃ τ) : Stmt Γ Λ σ → Stmt Γ Λ τ :=
…
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement_symm_statement line 650

    Source documentation

    Translating every instruction back restores the original statement, including its state-dependent instruction functions.

    @[simp] theorem statement_symm_statement (e : σ ≃ τ) (q : Stmt Γ Λ σ) :
    statement e.symm (statement e q) = q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement

  78. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration line 656
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration_label line 659
  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration_state line 662
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration_tapes line 665
  82. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration_symm_configuration line 668
  83. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration_configuration_symm line 673
  84. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configurationEquiv line 679

    Source documentation

    This is a bijection on actual machine configurations, not just on states.

    def configurationEquiv (e : σ ≃ τ) : Cfg Γ Λ σ ≃ Cfg Γ Λ τ where
…
  85. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configurationEquiv_apply line 685
  86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.control_configuration line 688
  87. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.program line 693
  88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.program_symm_program line 696
  89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statementPushBound line 702

    Source documentation

    The register change does not alter the finite statement's push bound.

    theorem statementPushBound (e : σ ≃ τ) (q : Stmt Γ Λ σ) :
    Runtime.statementPushBound (statement e q) = Runtime.statementPushBound q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.statementPushBound, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement

  90. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.supportsStmt_iff line 708

    Source documentation

    Exactly the same finite label set supports the translated statement.

    theorem supportsStmt_iff (e : σ ≃ τ) (S : Finset Λ) (q : Stmt Γ Λ σ) :
    SupportsStmt S (statement e q) ↔ SupportsStmt S q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement

  91. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.supports_iff line 730
  92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.stepAux_transport line 738

    Source documentation

    The actual recursively interpreted statement commutes with the register equivalence, with exactly the same tape updates.

    theorem stepAux_transport (e : σ ≃ τ) (q : Stmt Γ Λ σ) (state : σ)
    (tapes : ∀ k, List (Γ k)) :
    stepAux (statement e q) (e state) tapes =
      configuration e (stepAux q state tapes) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration

  93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.stepAux_transport_symm line 745
  94. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.step_transport line 753

    Source documentation

    Exact conjugacy also covers the halted configuration and the none step.

    theorem step_transport (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ) (c : Cfg Γ Λ σ) :
    step (program e source) (configuration e c) =
      (step source c).map (configuration e) := by
…

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

  95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.step_iff line 765
  96. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.advance_transport line 777
  97. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.iterate_transport line 787

    Source documentation

    Every intermediate configuration is transported at its original time index. This includes traces whose option-valued result is none.

    theorem iterate_transport (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ) (n : Nat)
    (c : Option (Cfg Γ Λ σ)) :
    (MachineComposition.advance (step (program e source)))^[n]
        (c.map (configuration e)) =
      ((MachineComposition.advance (step source))^[n] c).map (configuration e) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration

  98. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.trace_iff line 800

    Source documentation

    A successful running trace exists for exactly the same number of steps in the translated and original program.

    theorem trace_iff (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ) (n : Nat)
    (a b : Cfg Γ Λ σ) :
    (MachineComposition.advance (step (program e source)))^[n]
        (some (configuration e a)) = some (configuration e b) ↔
      (MachineComposition.advance (step source))^[n] (some a) = some b := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration

  99. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.trace line 816
  100. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.execution line 825

    Source documentation

    Transport an actual runtime witness without changing its step count or budget; the final option may be either a configuration or none.

    def execution (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ)
    {start : Cfg Γ Λ σ} {finish : Option (Cfg Γ Λ σ)} {budget : Nat}
    (run : StateTransition.EvalsToInTime (step source) start finish budget) :
    StateTransition.EvalsToInTime (step (program e source))
      (configuration e start) (finish.map (configuration e)) budget where
…

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

  101. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.execution_steps line 839
  102. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.execution_reflect line 846

    Source documentation

    Conversely, a translated runtime witness determines the original witness at exactly the same number of transitions.

    def execution_reflect (e : σ ≃ τ) (source : Λ → Stmt Γ Λ σ)
    {start : Cfg Γ Λ σ} {finish : Option (Cfg Γ Λ σ)} {budget : Nat}
    (run : StateTransition.EvalsToInTime (step (program e source))
      (configuration e start) (finish.map (configuration e)) budget) :
    StateTransition.EvalsToInTime (step source) start finish budget where
…

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

  103. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.execution_reflect_steps line 861