OAI/Computability/UniqueGames/Reduction/AddressTuplePolynomialLemmas.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

The actual address machine's final bridge, cleanup, reversal, and halt. The polynomial cleanup bound follows from space used by the supplied actual prefix execution. The complete reduction supplies that prefix in MachineAddressGame.

  1. def OAI.UniqueGamesTheorem.Integration.AddressTuplePolynomial.run_actual line 19
  2. theorem OAI.UniqueGamesTheorem.Integration.AddressTuplePolynomial.trace_actual line 48

    Source documentation

    The explicit iterated transition trace and its uniform bound, for callers that compose traces directly instead of runtime-witness structures.

    theorem trace_actual (T : NoiseTables.Table s d)
    (labels : AddressTupleBody.Label k s d noiseCount (AddressOutcomeSpecs.rows k T) → Λ)
    (exit : Option Λ)
    (P : Λ → TM2.Stmt (fun _ : AddressTupleBody.Arena k s d noiseCount => Bool) Λ (BodyState k))
    (atLabels : ∀ l, P (labels l) = instruction (AddressOutcomeSpecs.rows k T) labels exit l)
    (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (base : AddressTupleBody.Arena k s d noiseCount → List Bool) (ready : Ready F tuple base)
    (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base)
    (oldRhs : Fin k → Bool)
    (hB : base (headerTape k s d noiseCount .baseValue) =
      encodeWord (CanonicalAddress.base F.variables F.equations.length s d))
    (hC : base (headerTape k s d noiseCount .capacity) =
…

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Label, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.Arena

  3. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Tape line 82
  4. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.State line 84
  5. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.accumulator line 88
  6. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.output line 89
  7. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.accumulator_ne_output line 91
  8. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.clearKeys line 95

    Source documentation

    The finalizer visits every other tape in a fixed finite order.

    def clearKeys : List (Tape k T) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Tape

  9. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.mem_clearKeys line 100
  10. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.accumulator_not_mem_clearKeys line 105
  11. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.output_not_mem_clearKeys line 106
  12. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.clearKeys_covers line 108
  13. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.clearKeys_nodup line 111
  14. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.HeaderLabel line 115
  15. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.BodyLabel line 116
  16. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.FinishLabel line 118
  17. inductive OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Label line 120
  18. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.headerLabels line 130
  19. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.initializeLabels line 131
  20. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyLabels line 132
  21. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishLabels line 133
  22. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.start line 135
  23. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.initializeStart line 136
  24. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyStart line 137
  25. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.checkLabel line 138
  26. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.resetLabel line 139
  27. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStart line 140
  28. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.next line 142
  29. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.resetAt line 145
  30. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.next_lt line 148
  31. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.next_ge line 150
  32. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.resetAt_lt line 152
  33. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.program line 157

    Source documentation

    Header, digit initialization, physical tuple body, carry loops, and complete finalization are placed in a single actual finite transition program.

    def program : Label k T → TM2.Stmt (fun _ : Tape k T => Bool) (Label k T) (State k)
  | .header l => MachineAddressHeaders.statement
      (AddressMachineSpace.fullHeaderSlots k s d T.vectors.length)
      (headerLabels k T) (some (initializeStart k T)) l
  | .initialize l => MachineOdometerInit.statement
      (AddressMachineSpace.odometerSlots k s d T.vectors.length)
      (initializeLabels k T) (some (bodyStart k T)) l
  | .body l => Integration.AddressTupleBody.instruction (AddressOutcomeSpecs.rows k T)
      (bodyLabels k T) (some (next k T 0)) l
  | .check j => MachineTupleOdometer.increment
      (AddressMachineSpace.current k s d T.vectors.length j)
      (AddressMachineSpace.remaining k s d T.vectors.length j)
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Label, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Tape, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.State, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.statement, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.fullHeaderSlots, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.headerLabels, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.initializeStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.odometerSlots, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.initializeLabels, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyStart, OAI.UniqueGamesTheorem.Integration.AddressTupleBody.instruction, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.rows, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyLabels, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.next, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.current, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.remaining

  34. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.atHeader line 179
  35. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.atInitialize line 183
  36. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.atBody line 188
  37. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.atCheck line 192
  38. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.atReset line 197
  39. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.atFinish line 202
  40. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStartStep line 207

    Source documentation

    This bridge has no data-dependent action and costs exactly one transition.

    theorem finishStartStep (state : State k) (base : Tape k T → List Bool) :
    TM2.step (program k T) ⟨some (finishStart k T),state,base⟩ =
      some ⟨SourceRuntimeFinish.entry (clearKeys k T) (finishLabels k T),state,base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.State, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Tape, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.program, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.clearKeys, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishLabels

  41. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStartInTime line 214
  42. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine line 223

    Source documentation

    All alphabets and registers are finite. Counts live solely on Bool stacks.

    def machine : FinTM2 where
…
  43. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine_main line 234
  44. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine_program line 235
  45. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine_initialState line 236
  46. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine_input line 237
  47. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine_output line 238
  48. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.inputAlphabet line 241

    Source documentation

    Identity alphabet encodings at both ends of the concrete machine.

    def inputAlphabet : (machine k T).Γ (machine k T).k₀ ≃ Bool := Equiv.refl Bool

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine

  49. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.outputAlphabet line 242
  50. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.inputTapes line 244
  51. def OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.outputTapes line 247
  52. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.inputTapes_source line 250
  53. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.inputTapes_other line 253
  54. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.outputTapes_output line 256
  55. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.outputTapes_other line 259
  56. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.initList_eq line 262
  57. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.haltList_eq line 274
  58. def OAI.UniqueGamesTheorem.Reduction.AddressMachineFinish.timePolynomial line 306
  59. def OAI.UniqueGamesTheorem.Reduction.AddressMachineFinish.completePrefix line 313

    Source documentation

    Finish the concrete program, including its one-step finalizer entry bridge. The runtime bound uses all actual intermediate tapes, with no output-size or private-space assumption.

    def completePrefix (input : List Bool) (prefixTime : Polynomial Nat)
    (base : AddressMachineProgram.Tape k T → List Bool)
    (execution : StateTransition.EvalsToInTime (AddressMachineProgram.machine k T).step
      (initList (AddressMachineProgram.machine k T) input)
      (some ⟨some (AddressMachineProgram.finishStart k T),
        AddressMachineSpace.initialState k, base⟩) (prefixTime.eval input.length))
    (outputEmpty : base (AddressMachineProgram.output k T) = []) :
    TM2OutputsInTime (AddressMachineProgram.machine k T) input
      (some (base (AddressMachineProgram.accumulator k T)).reverse)
      ((timePolynomial k T prefixTime).eval input.length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.Tape, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.initialState, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.output, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.accumulator, OAI.UniqueGamesTheorem.Reduction.AddressMachineFinish.timePolynomial