OAI/Computability/UniqueGames/Machines/MachineLookupLemmas.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Actual traces for the fixed unary lookup machine. Successful lookup preserves an arbitrary unread table suffix. Rejection relative to a list's end is stated only for its complete, unframed encoding, so no hidden endpoint is assumed.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.guard_step_succ line 24
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.guard_step_zero line 37
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.select_step_nonempty line 50
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.select_step_empty line 66
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.copyTrace line 77
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.selectTrace line 92
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.skipCycleTrace line 107
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.emptyCycleTrace line 125
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.successPrefixTrace line 143

    Source documentation

    A successful positional lookup scans precisely its prior and selected field. The suffix is arbitrary and is retained byte for byte.

    theorem successPrefixTrace (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (prior : List Nat) (value : Nat)
    (indexSuffix suffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[
        (encodeWords prior).length + prior.length + value + 3]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord prior.length ++ indexSuffix)
        (encodeWords prior ++ (encodeWord value ++ suffix)) output⟩) =
      some ⟨some .accepted, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) suffix (encodeWord value ++ output)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.lookupTrace_some line 171

    Source documentation

    Successful array access, with explicit selected value and preserved framing.

    theorem lookupTrace_some (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i value : Nat)
    (selected : values[i]? = some value)
    (indexSuffix suffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values ++ suffix) output⟩) =
      some ⟨some .accepted, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)) ++ suffix)
        (encodeWord value ++ output)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.emptyTrace line 200
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.lookupTrace_invalid line 223

    Source documentation

    Invalid indices reject on a complete encoded table, after consuming that table and all positive index bits. The output and other tapes are unchanged.

    theorem lookupTrace_invalid (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat) (invalid : values.length ≤ i)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩) =
      some ⟨some .rejected, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) [] output⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultLabel line 246

    Source documentation

    The two explicit control outcomes on a complete encoded table.

    def resultLabel (values : List Nat) (i : Nat) : Label :=
…

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

  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultOutput line 252

    Source documentation

    Successful lookup prefixes a complete unary word; failure writes nothing.

    def resultOutput (values : List Nat) (i : Nat) (output : List Bool) : List Bool :=
…
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.lookupTrace line 259

    Source documentation

    A total execution statement for every natural index and complete table. No bound or validity assumption on the index is needed.

    theorem lookupTrace (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩) =
      some ⟨some (resultLabel values i), (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)))
        (resultOutput values i output)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultOutput

  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.lookupInTime line 283

    Source documentation

    A proved linear transition budget in the lengths of the encoded table and index, including invalid indices. The witness is the actual trace above.

    def lookupInTime (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program index source destination))
      ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩
      (some ⟨some (resultLabel values i), (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)))
        (resultOutput values i output)⟩)
      ((encodeWords values).length + 2 * (encodeWord i).length) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultOutput

  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.lookupHaltTrace line 300

    Source documentation

    The final control label executes a genuine halt in one more transition.

    theorem lookupHaltTrace (index source destination : K)
    (his : index ≠ source) (hid : index ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program index source destination)))^[MachineLookupSpec.steps values i + 1]
      (some ⟨some .guard, (ambient, register), tapes index source destination base
        (encodeWord i ++ indexSuffix) (encodeWords values) output⟩) =
      some ⟨none, (ambient, none), tapes index source destination base
        (encodeWord 0 ++ indexSuffix) (encodeWords (values.drop (i + 1)))
        (resultOutput values i output)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookupSpec.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.resultOutput

  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.timePolynomial line 315

    Source documentation

    A single polynomial in the combined two input lengths.

    noncomputable def timePolynomial : Polynomial Nat := Polynomial.C 2 * Polynomial.X + 1
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.timePolynomial_bounds line 317
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.machineInTime line 328

    Source documentation

    The same exact computation as a certificate for the concrete finite three-stack machine. Both valid and invalid indices terminate with reset local state, retaining the zero index delimiter and all other stated tape contents.

    def machineInTime (base : Fin 3 → List Bool) (values : List Nat) (i : Nat)
    (indexSuffix output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      ⟨some .guard, ((), register), tapes (K := Fin 3) 0 1 2 base
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes

  21. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.Alphabet line 355
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.initialTapes line 358

    Source documentation

    Tape roles: original table, unary query, scan work, output, copy scratch.

    def initialTapes (tape : Fin 5 → K) (base : K → List Bool)
    (index : Nat) (indexSuffix workSuffix output : List Bool) : K → List Bool :=
…
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.finalTapes line 363
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.lookupFramedHaltTrace_some line 370
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.preservingLookupTrace line 390

    Source documentation

    Code-level interfaces specify the actual two copy loops and six lookup instructions in the caller's program. No execution premise is supplied.

    theorem preservingLookupTrace (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (firstLabel secondLabel : Λ) (lookupLabels : MachineLookup.Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.Alphabet

  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.preservingLookup_steps_le line 440
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.preservingLookupInTime line 448
  28. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.Label line 470
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.program line 474
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.machine line 481
  31. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.Alphabet line 501
  32. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.Label line 503
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.instruction line 508
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.steps line 523
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.finalTapes line 528
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.initialTapes_eq_update line 533
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.affineLookupTrace line 555

    Source documentation

    An exact trace for the actual composite instructions. atLabels specifies the caller's finite program; there is no execution or runtime premise.

    theorem affineLookupTrace (source : K) (tape : Fin 5 → K)
    (distinct : Function.Injective tape) (outside : ∀ i, source ≠ tape i)
    (coefficient offset : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.Alphabet

  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.steps_le line 583
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.steps_le_table line 591
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.finalTapes_other line 598
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.finalTapes_output line 604
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.machine line 609
  43. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductGather.Tape line 640

    Source documentation

    Shared original table, query, scan and copy scratch, then input coordinate fields and the corresponding gathered output fields.

    abbrev Tape (width : Nat) := Fin 4 ⊕ (Fin width ⊕ Fin width)
  44. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.shift line 642
  45. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.shift_injective line 645
  46. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.lookupRole line 649
  47. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.lookupRole_injective line 656
  48. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.Label line 660
  49. instance OAI.UniqueGamesTheorem.Explicit.MachineProductGather.labelFintype line 664
  50. instance OAI.UniqueGamesTheorem.Explicit.MachineProductGather.labelDecidableEq line 671
  51. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.entry line 678
  52. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.instruction line 682
  53. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.steps line 696
  54. def OAI.UniqueGamesTheorem.Explicit.MachineProductGather.finalTapes line 703
  55. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.finalTapes_other line 713
  56. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.gatherTrace line 728
  57. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.finalTapes_field line 790

    Source documentation

    Every output is the physically gathered unary field, with its old suffix preserved. This identifies the operands consumed by the Horner phase.

    theorem finalTapes_field (values : List Nat) (coefficient width : Nat)
    (placement : Tape width → K) (distinct : Function.Injective placement)
    (indices offsets fields : Fin width → Nat) (base : K → List Bool) (i : Fin width) :
    finalTapes values coefficient width placement indices offsets fields base
      (placement (.inr (.inr i))) =
      encodeWord (fields i) ++ base (placement (.inr (.inr i))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductGather.Tape, OAI.UniqueGamesTheorem.Explicit.MachineProductGather.finalTapes

  58. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.steps_le line 825

    Source documentation

    For fixed width, gather time is linear in the encoded table size plus coordinate magnitudes. Query and scan debris is never rescanned.

    theorem steps_le (values : List Nat) (coefficient width magnitude : Nat)
    (indices offsets fields : Fin width → Nat)
    (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
    (bounded : ∀ i, indices i ≤ magnitude) :
    steps values coefficient width indices offsets ≤
      width * (2 * magnitude + 5 * (encodeWords values).length + 6) + 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductGather.steps