OAI/Computability/UniqueGames/Machines/MachineBinaryNameSearch.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

First-occurrence search over signed, framed binary names. The stream has no clause markers. Every iteration discards one sign, scans and compares the actual candidate payload, and increments a Boolean unary counter only after a mismatch. The preserved key is a reversed payload, never a unary name.

The six explicitly distinct tapes are: stream, preserved key, candidate, copied key, copy scratch, and unary occurrence counter. Successful search consumes precisely the prefix through the first matching name, preserves the unread suffix and all ambient tapes, and returns the three work tapes empty. The time theorem follows from literal instruction equations and checked comparison executions, with no supplied loop-body trace premise.

  1. abbrev OAI.UniqueGamesTheorem.BinaryNameSearch.Token line 29
  2. def OAI.UniqueGamesTheorem.BinaryNameSearch.tokenBits line 31
  3. def OAI.UniqueGamesTheorem.BinaryNameSearch.stream line 34
  4. def OAI.UniqueGamesTheorem.BinaryNameSearch.payloads line 38
  5. def OAI.UniqueGamesTheorem.BinaryNameSearch.afterMatch line 40
  6. def OAI.UniqueGamesTheorem.BinaryNameSearch.steps line 44
  7. def OAI.UniqueGamesTheorem.BinaryNameSearch.payloadSize line 50
  8. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.stream_nil line 52
  9. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.stream_cons line 54
  10. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.payloads_nil line 57
  11. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.payloads_cons line 59
  12. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.payloadSize_nil line 62
  13. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.payloadSize_cons line 64
  14. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.stream_length line 67
  15. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.steps_le line 77

    Source documentation

    Work is linear in the scanned payloads plus one key-copy cost per token.

    theorem steps_le (tokens : List Token) (key : List Bool) :
    steps tokens key ≤ 2 * payloadSize tokens + (3 * key.length + 6) * tokens.length := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameSearch.Token, OAI.UniqueGamesTheorem.BinaryNameSearch.steps, OAI.UniqueGamesTheorem.BinaryNameSearch.payloadSize

  16. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.steps_le_stream line 87

    Source documentation

    This bound uses lengths of actual encoded words, not decoded name values.

    theorem steps_le_stream (tokens : List Token) (key : List Bool) :
    steps tokens key ≤ (3 * key.length + 7) * (stream tokens).length := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameSearch.Token, OAI.UniqueGamesTheorem.BinaryNameSearch.steps, OAI.UniqueGamesTheorem.BinaryNameSearch.stream

  17. abbrev OAI.UniqueGamesTheorem.BinaryNameSearch.Alphabet line 97
  18. abbrev OAI.UniqueGamesTheorem.BinaryNameSearch.State line 98
  19. abbrev OAI.UniqueGamesTheorem.BinaryNameSearch.clean line 100
  20. inductive OAI.UniqueGamesTheorem.BinaryNameSearch.Label line 102
  21. def OAI.UniqueGamesTheorem.BinaryNameSearch.compareTapes line 108
  22. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.compareTapes_injective line 111
  23. def OAI.UniqueGamesTheorem.BinaryNameSearch.exitAt line 117
  24. def OAI.UniqueGamesTheorem.BinaryNameSearch.finish line 122
  25. def OAI.UniqueGamesTheorem.BinaryNameSearch.instruction line 125
  26. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.stepAux_finish line 136
  27. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.update_source line 140
  28. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.update_counter line 151
  29. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.joinTrace line 157
  30. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.signStep line 170
  31. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.emptyStep line 181
  32. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.incrementStep line 192
  33. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.tokenTrace line 203

    Source documentation

    One sign is consumed, then the actual shared scan/copy/compare routine runs.

    theorem tokenTrace (token : Token) (key suffix counter : List Bool)
    (canonical : BinaryNameMachine.canonical token.2 = true)
    (keyWord : base (tape 1) = key.reverse)
    (candidateEmpty : base (tape 2) = []) (copyEmpty : base (tape 3) = [])
    (scratchEmpty : base (tape 4) = []) :
    (advance (TM2.step program))^[1 + BinaryNameCompare.steps token.2.length key.length]
      (some ⟨some (labels .sign), clean ambient,
        tapesAt (tape 0) (tape 5) base (tokenBits token ++ suffix) counter⟩) =
      some ⟨if token.2 = key then foundExit else some (labels .increment), clean ambient,
        tapesAt (tape 0) (tape 5) base suffix counter⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameSearch.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameCompare.steps, OAI.UniqueGamesTheorem.BinaryNameSearch.clean, OAI.UniqueGamesTheorem.BinaryNameSearch.tokenBits

  34. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.searchTrace line 251

    Source documentation

    Successful search returns exactly the first occurrence index. All labels are literal instruction equations, so this theorem supplies its own body runs.

    theorem searchTrace (tokens : List Token) (key suffix counter : List Bool)
    (canonical : ∀ token ∈ tokens, BinaryNameMachine.canonical token.2 = true)
    (present : key ∈ payloads tokens)
    (keyWord : base (tape 1) = key.reverse)
    (candidateEmpty : base (tape 2) = []) (copyEmpty : base (tape 3) = [])
    (scratchEmpty : base (tape 4) = []) :
    (advance (TM2.step program))^[steps tokens key]
      (some ⟨some (labels .sign), clean ambient,
        tapesAt (tape 0) (tape 5) base (stream tokens ++ suffix) counter⟩) =
      some ⟨foundExit, clean ambient,
        tapesAt (tape 0) (tape 5) base (stream (afterMatch tokens key) ++ suffix)
          (List.replicate ((payloads tokens).idxOf key) true ++ counter)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameSearch.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameSearch.payloads, OAI.UniqueGamesTheorem.BinaryNameSearch.steps, OAI.UniqueGamesTheorem.BinaryNameSearch.clean, OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryNameSearch.afterMatch

  35. def OAI.UniqueGamesTheorem.BinaryNameSearch.searchInTime line 303

    Source documentation

    Explicit polynomial bound for the actual successful run.

    def searchInTime (tokens : List Token) (key suffix counter : List Bool)
    (canonical : ∀ token ∈ tokens, BinaryNameMachine.canonical token.2 = true)
    (present : key ∈ payloads tokens)
    (keyWord : base (tape 1) = key.reverse)
    (candidateEmpty : base (tape 2) = []) (copyEmpty : base (tape 3) = [])
    (scratchEmpty : base (tape 4) = []) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .sign), clean ambient,
        tapesAt (tape 0) (tape 5) base (stream tokens ++ suffix) counter⟩
      (some ⟨foundExit, clean ambient,
        tapesAt (tape 0) (tape 5) base (stream (afterMatch tokens key) ++ suffix)
          (List.replicate ((payloads tokens).idxOf key) true ++ counter)⟩)
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameSearch.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameSearch.payloads, OAI.UniqueGamesTheorem.BinaryNameSearch.clean, OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryNameSearch.afterMatch

  36. def OAI.UniqueGamesTheorem.BinaryNameSearch.machine line 325

    Source documentation

    Concrete finite-control instantiation; the counter is its designated output.

    def machine : FinTM2 where
…
  37. theorem OAI.UniqueGamesTheorem.BinaryNameSearch.machine_finiteAlphabet line 338