OAI/Computability/MaxCut/Machines/RuntimeSpace.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

Intermediate tape-space bounds derived from actual successful machine prefixes, and their use in the separately checked physical finalizer.

  1. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.configurationLength line 20

    Source documentation

    All stacks are counted, even when their symbol types differ.

    def configurationLength (tm : FinTM2) (cfg : tm.Cfg) : Nat :=
…
  2. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.initial_configurationLength line 23
  3. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.step_configurationLength line 33
  4. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.execution_configurationLength line 43

    Source documentation

    Every successfully executed prefix bounds the space in its actual endpoint.

    theorem execution_configurationLength (tm : FinTM2) {start finish : tm.Cfg}
    {budget : Nat}
    (run : StateTransition.EvalsToInTime tm.step start (some finish) budget) :
    configurationLength tm finish ≤ configurationLength tm start +
      budget * (Fintype.card tm.K * Runtime.programPushBound tm) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.configurationLength

  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.prefix_configurationLength line 51
  6. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial line 58
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial_eval line 61
  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.prefix_length_polynomial line 66
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.totalLength_eq_configurationLength line 76

    Source documentation

    This equality only identifies the actual endpoint stacks with a Boolean finalizer's stacks. It makes no execution or time assumption.

    theorem totalLength_eq_configurationLength (tm : FinTM2) (finish : tm.Cfg)
    (base : tm.K → List Bool)
    (sameLengths : ∀ k, (base k).length = (finish.stk k).length) :
    SourceRuntimeFinish.totalLength base = configurationLength tm finish := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.totalLength, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.configurationLength

  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.finishCost_le_of_prefix line 84

    Source documentation

    The actual physical finalizer's cost is bounded by the space reached by the actual prefix. Repeated cleanup keys remain permitted.

    theorem finishCost_le_of_prefix (tm : FinTM2) (input : List (tm.Γ tm.k₀))
    {finish : tm.Cfg} {budget : Nat}
    (run : StateTransition.EvalsToInTime tm.step (initList tm input) (some finish) budget)
    (clearKeys : List tm.K) (accumulator output : tm.K)
    (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
    (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
    (base : tm.K → List Bool) (outputEmpty : base output = [])
    (sameLengths : ∀ k, (base k).length = (finish.stk k).length) :
    SourceRuntimeFinish.finishCost clearKeys accumulator base ≤ input.length +
      budget * (Fintype.card tm.K * Runtime.programPushBound tm) + clearKeys.length + 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishCost

  11. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.completedTime line 100
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.completedTime_eval line 104
  13. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeSpace.prefixAndFinishInTime line 113

    Source documentation

    Composition retains both actual execution witnesses. The cleanup witness is supplied by SourceRuntimeFinish.finishInTime in the caller's real program.

    def prefixAndFinishInTime (tm : FinTM2) (input : List (tm.Γ tm.k₀))
    (time : Polynomial Nat) {middle finish : tm.Cfg}
    (prefixRun : StateTransition.EvalsToInTime tm.step (initList tm input)
      (some middle) (time.eval input.length))
    (clearKeys : List tm.K) (accumulator output : tm.K)
    (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
    (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
    (base : tm.K → List Bool) (outputEmpty : base output = [])
    (sameLengths : ∀ k, (base k).length = (middle.stk k).length)
    (finishRun : StateTransition.EvalsToInTime tm.step middle (some finish)
      (SourceRuntimeFinish.finishCost clearKeys accumulator base)) :
    StateTransition.EvalsToInTime tm.step (initList tm input) (some finish)
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeFinish.finishCost

  14. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.ExtraTape line 144
  15. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList line 147
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_getElem?_ctorIdx_eq line 149
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_nodup line 153
  18. instance OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.(instance at line 155) line 155
  19. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Phase line 158
  20. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Phase.enumList line 161
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Phase.enumList_getElem?_ctorIdx_eq line 164
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Phase.enumList_nodup line 168
  23. instance OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.(instance at line 170) line 170
  24. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Tape line 174
  25. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Symbols line 175
  26. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.Label line 176
  27. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.State line 177
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.extraTapes line 179
  29. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.auxProgram line 185
  30. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.program line 206
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.machine line 210
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputTapes line 228
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputTapes_input line 231
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputTapes_counter line 235
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputConfig line 238
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.embedded line 242
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.temporaryTapes line 247
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.temporaryConfig line 250
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputTapes_update_input_inline_MachineRepeat line 254
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputTapes_update_counter_inline_MachineRepeat line 266
  41. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.oneStep_inline_MachineRepeat line 275
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.parseStep_true line 283
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.parseStep_false line 292
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.parseTrace line 301
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.guardStep_some line 327
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.guardStep_none line 336
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.bodyExecution line 345

    Source documentation

    Lift the actual certified body run while preserving the remaining counter.

    def bodyExecution (counter : List (M.Γ M.k₀))
    (word : List (M.Γ M.k₀)) (result : List (M.Γ M.k₁)) (budget : Nat)
    (run : TM2OutputsInTime M word (some result) budget) :
    StateTransition.EvalsToInTime (machine M input output).step
      (embedded M counter (initList M word))
      (some (embedded M counter (haltList M result))) budget :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.machine, OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.embedded

  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.bodyToTemp_tapes_inline_MachineRepeat line 355
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.tempToBody_tapes_inline_MachineRepeat line 371
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.finalToTemp_tapes_inline_MachineRepeat line 383
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.tempToOutput_tapes_inline_MachineRepeat line 395
  52. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.bodyToTemp line 406
  53. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.tempToBody line 422
  54. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.finalToTemp line 437
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.tempToOutput line 449
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.bodyReturn line 463

    Source documentation

    Transfer the literal body output back to the input, preserving its order.

    def bodyReturn (result : List (M.Γ M.k₁)) (counter : List (M.Γ M.k₀)) :
    StateTransition.EvalsToInTime (machine M input output).step
      (embedded M counter (haltList M result))
      (some (inputConfig M .guard (result.map (fun b => input.symm (output b))) counter))
      (2*(result.length+1)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.machine, OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.embedded, OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputConfig

  57. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.finish line 476

    Source documentation

    Zero remaining iterations still run the actual final transfers and halt with every tape other than the designated output empty.

    def finish (word : List (M.Γ M.k₀)) :
    StateTransition.EvalsToInTime (machine M input output).step
      (inputConfig M .guard word []) (some (haltList (machine M input output) word))
      (2*word.length+3) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.machine, OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputConfig

  58. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopBudget line 490

    Source documentation

    Running time after the parser: actual body budgets, two transfers per body result, one guard per iteration, and the final transfer and empty guard.

    def loopBudget : Nat → (Nat → List Bool) → (Nat → Nat) → Nat
  | 0, words, _ => 2*(words 0).length+3
  | count+1, words, budgets => budgets 0 + 2*(words 1).length+3 +
      loopBudget count (fun i => words (i+1)) (fun i => budgets (i+1))
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopExecution line 495
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.inputConfig_init_inline_MachineRepeat line 533
  61. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.executeSequence line 545
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopBudget_eq_sum line 574

    Source documentation

    Explicit sum form of the actual repeat budget.

    theorem loopBudget_eq_sum (count : Nat) (words : Nat → List Bool) (budgets : Nat → Nat) :
    loopBudget count words budgets =
      (∑ i ∈ Finset.range count, (budgets i + 2*(words (i+1)).length+3)) +
      2*(words count).length+3 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopBudget

  63. def OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.executeSequenceSum line 586

    Source documentation

    The sum of supplied body budgets and explicit linear transfer overheads.

    def executeSequenceSum (count : Nat) (words : Nat → List Bool) (budgets : Nat → Nat)
    (runs : ∀ i, i < count → TM2OutputsInTime M ((words i).map input.symm)
      (some ((words (i+1)).map output.symm)) (budgets i)) :
    TM2OutputsInTime (machine M input output)
      ((encodeWord count ++ words 0).map input.symm)
      (some ((words count).map input.symm))
      (count+1 + ((∑ i ∈ Finset.range count, (budgets i+2*(words (i+1)).length+3)) +
        2*(words count).length+3)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.machine, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopBudget_le line 600

    Source documentation

    A uniform bound along the executed sequence is enough to bound the actual repeat runtime. No polynomial growth of an arbitrary iteration is asserted.

    theorem loopBudget_le (count : Nat) (words : Nat → List Bool) (budgets : Nat → Nat)
    (bodyBound lengthBound : Nat)
    (hb : ∀i, i<count → budgets i ≤ bodyBound)
    (hl : ∀i, i≤count → (words i).length ≤ lengthBound) :
    loopBudget count words budgets ≤ count*(bodyBound+2*lengthBound+3)+2*lengthBound+3 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.loopBudget

  65. def OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet line 636

    Source documentation

    Every physical tape has a finite alphabet. Together with M.kFin, this also makes the disjoint union of all physical tape alphabets finite.

    def FiniteAlphabet (M : FinTM2) : Prop := ∀ k, Finite (M.Γ k)
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.input_finite line 639

    Source documentation

    This one alphabet is already finite in the underlying machine record.

    theorem input_finite (M : FinTM2) : Finite (M.Γ M.k₀) := by
…
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.of_homogeneous line 643
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.of_bool line 650

    Source documentation

    All concrete Boolean-stack machines satisfy the stronger alphabet condition.

    theorem of_bool (M : FinTM2) (alphabet : ∀ k, M.Γ k = Bool) : FiniteAlphabet M :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet

  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.of_equiv line 653
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.symbols_finite line 658
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.sequential_machine line 666

    Source documentation

    The first two tape groups retain their original alphabets. The sole new bridge tape uses the second machine's already finite input alphabet.

    theorem sequential_machine (first second : FinTM2)
    (relabel : first.Γ first.k₁ → second.Γ second.k₀)
    (fallback : second.Γ second.k₀)
    (hfirst : FiniteAlphabet first) (hsecond : FiniteAlphabet second) :
    FiniteAlphabet (MachineSequential.machine first second relabel fallback) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineSequential.machine

  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.compose line 679

    Source documentation

    Preservation for the machine actually stored in the polynomial-time composition certificate, with its actual relabeling bridge.

    theorem compose {α β γ αΓ βΓ γΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {ec : γ → List γΓ}
    {f : α → β} {g : β → γ}
    (first : TM2ComputableInPolyTime ea eb f)
    (second : TM2ComputableInPolyTime eb ec g) (fallback : βΓ)
    (hfirst : FiniteAlphabet first.tm) (hsecond : FiniteAlphabet second.tm) :
    FiniteAlphabet (MachineSequential.compose first second fallback).tm := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineSequential.compose

  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.composeBits line 690
  74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.repeat_machine line 701

    Source documentation

    Counter, temporary, and output tapes of the actual repeat machine all use the body's finite input alphabet; body tapes retain their original alphabets.

    theorem repeat_machine (body : FinTM2)
    (input : body.Γ body.k₀ ≃ Bool) (output : body.Γ body.k₁ ≃ Bool)
    (hbody : FiniteAlphabet body) :
    FiniteAlphabet (MachineRepeat.machine body input output) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRepeat.machine

  75. def OAI.MaxCutGames.Explicit.MachineUniformRun.outputBits line 722
  76. def OAI.MaxCutGames.Explicit.MachineUniformRun.afterScale line 725
  77. def OAI.MaxCutGames.Explicit.MachineUniformRun.afterEmit line 729
  78. def OAI.MaxCutGames.Explicit.MachineUniformRun.scaleInTime line 733
  79. theorem OAI.MaxCutGames.Explicit.MachineUniformRun.repeated_template line 755
  80. theorem OAI.MaxCutGames.Explicit.MachineUniformRun.template_output line 766
  81. theorem OAI.MaxCutGames.Explicit.MachineUniformRun.template_copiedLength line 778
  82. def OAI.MaxCutGames.Explicit.MachineUniformRun.emitInTime line 785
  83. def OAI.MaxCutGames.Explicit.MachineUniformRun.prefixPolynomial line 802
  84. theorem OAI.MaxCutGames.Explicit.MachineUniformRun.input_length line 805
  85. def OAI.MaxCutGames.Explicit.MachineUniformRun.prefixInTime line 809
  86. def OAI.MaxCutGames.Explicit.MachineUniformRun.timePolynomial line 826
  87. theorem OAI.MaxCutGames.Explicit.MachineUniformRun.haltList_eq line 829
  88. def OAI.MaxCutGames.Explicit.MachineUniformRun.finishStartInTime line 837
  89. def OAI.MaxCutGames.Explicit.MachineUniformRun.outputInTime line 849

    Source documentation

    The complete actual run, including the physical cleanup and output reversal.

    noncomputable def outputInTime (C n q Q : Nat) (body : List Bool) :
    TM2OutputsInTime (machine C) (encodeWords [n, q, Q] ++ body)
      (some (outputBits C n q Q body))
      ((timePolynomial C).eval (encodeWords [n, q, Q] ++ body).length) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineUniformRun.outputBits, OAI.MaxCutGames.Explicit.MachineUniformRun.timePolynomial

  90. def OAI.MaxCutGames.Explicit.MachineUniformRun.computation line 884

    Source documentation

    A fixed actual program works for every game and every alphabet size.

    noncomputable def computation {q : Nat} (C : Nat) (hC : 0 < C) :
    TM2ComputableInPolyTime gameBits gameBits (UniformTarget.construct (q := q) C hC) where
…

    Mentions: OAI.MaxCutGames.Explicit.UniformTarget.construct

  91. theorem OAI.MaxCutGames.Explicit.MachineUniformRun.finiteAlphabet line 905