OAI/Computability/UniqueGames/Machines/MachineBinaryRenameLoop.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

The actual cursor loop for sparse-name renaming. A finite three-position slot counts completed clauses. Each nonempty cursor test calls the checked literal machine, then pushes one variable-count bit. Every third literal also pushes one clause-count bit. No instruction counts an unbounded list in finite control.

All nine literal-machine tapes retain their meanings. Tapes 9 and 10 are the variable and clause counters. The original token stream is preserved; the cursor is exhausted, the six work tapes are restored, and the output contains the reversed concatenation of exactly the emitted literal words.

  1. abbrev OAI.UniqueGamesTheorem.BinaryRenameLoop.Token line 23
  2. def OAI.UniqueGamesTheorem.BinaryRenameLoop.nextSlot line 25
  3. def OAI.UniqueGamesTheorem.BinaryRenameLoop.clauseIncrement line 27
  4. def OAI.UniqueGamesTheorem.BinaryRenameLoop.finalSlot line 29
  5. def OAI.UniqueGamesTheorem.BinaryRenameLoop.completedClauses line 33
  6. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.finalSlot_three line 37
  7. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.completedClauses_three line 40
  8. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.finalSlot_triples line 44
  9. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.completedClauses_triples line 49
  10. def OAI.UniqueGamesTheorem.BinaryRenameLoop.outputBody line 54
  11. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.outputBody_nil line 57
  12. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.outputBody_cons line 59
  13. def OAI.UniqueGamesTheorem.BinaryRenameLoop.steps line 63
  14. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.payload_length_le_stream line 67
  15. def OAI.UniqueGamesTheorem.BinaryRenameLoop.perLiteralBound line 82
  16. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.literal_steps_le line 85
  17. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.steps_le line 97
  18. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.steps_le_cubic line 110
  19. abbrev OAI.UniqueGamesTheorem.BinaryRenameLoop.Alphabet line 128
  20. abbrev OAI.UniqueGamesTheorem.BinaryRenameLoop.State line 129
  21. abbrev OAI.UniqueGamesTheorem.BinaryRenameLoop.clean line 130
  22. inductive OAI.UniqueGamesTheorem.BinaryRenameLoop.Label line 133
  23. def OAI.UniqueGamesTheorem.BinaryRenameLoop.literalTapes line 139
  24. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.literalTapes_injective line 142
  25. def OAI.UniqueGamesTheorem.BinaryRenameLoop.finish line 148
  26. def OAI.UniqueGamesTheorem.BinaryRenameLoop.next line 154
  27. def OAI.UniqueGamesTheorem.BinaryRenameLoop.instruction line 158
  28. def OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes line 175

    Source documentation

    These are the only four stacks changed by the complete loop.

    def loopTapes (tape : Fin 11 → K) (base : K → List Bool)
    (cursor output variableCounter clauses : List Bool) : K → List Bool :=
…
  29. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes_cursor line 180
  30. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes_output line 186
  31. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes_variables line 192
  32. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes_clauses line 198
  33. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.update_cursor line 203
  34. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.update_output line 213
  35. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.update_variables line 223
  36. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.update_clauses line 233
  37. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes_other line 239
  38. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.stepAux_finish line 245
  39. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.joinTrace line 250
  40. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.peekStep line 262
  41. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.emptyStep line 274
  42. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.tallyStep line 285
  43. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.bodyTrace line 301

    Source documentation

    Peek, execute the checked literal program, then update the two counters.

    theorem bodyTrace (tokens : List Token) (token : Token) (slot : Fin 3)
    (suffix output variableCounter clauses : List Bool)
    (canonical : BinaryNameMachine.canonical token.2 = true)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (present : token.2 ∈ BinaryNameSearch.payloads tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    (advance (TM2.step program))^[BinaryLiteralMachine.steps tokens token.2 + 2]
      (some ⟨some (labels .entry), clean ambient slot,
        loopTapes tape base (BinaryNameSearch.tokenBits token ++ suffix) output variableCounter clauses⟩) =
      some ⟨some (labels .entry), clean ambient (nextSlot slot),
        loopTapes tape base suffix
…

    Mentions: OAI.UniqueGamesTheorem.BinaryRenameLoop.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameSearch.payloads, OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryLiteralMachine.steps, OAI.UniqueGamesTheorem.BinaryRenameLoop.clean, OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes, OAI.UniqueGamesTheorem.BinaryNameSearch.tokenBits, OAI.UniqueGamesTheorem.BinaryRenameLoop.nextSlot

  44. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTrace line 374

    Source documentation

    Full loop execution, including the final empty-cursor test.

    theorem loopTrace (tokens input : List Token) (slot : Fin 3)
    (output variableCounter clauses : List Bool)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (included : ∀ t ∈ input, t ∈ tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    (advance (TM2.step program))^[steps tokens input]
      (some ⟨some (labels .entry), clean ambient slot,
        loopTapes tape base (BinaryNameSearch.stream input) output variableCounter clauses⟩) =
      some ⟨done, clean ambient (finalSlot input.length slot),
        loopTapes tape base [] ((outputBody tokens input).reverse ++ output)
          (List.replicate input.length true ++ variableCounter)
…

    Mentions: OAI.UniqueGamesTheorem.BinaryRenameLoop.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryRenameLoop.steps, OAI.UniqueGamesTheorem.BinaryRenameLoop.clean, OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes, OAI.UniqueGamesTheorem.BinaryRenameLoop.finalSlot, OAI.UniqueGamesTheorem.BinaryRenameLoop.outputBody

  45. theorem OAI.UniqueGamesTheorem.BinaryRenameLoop.triplesTrace line 419

    Source documentation

    On complete triples the finite slot is reset and the two counters are exact.

    theorem triplesTrace (tokens input : List Token) (count : Nat)
    (length_eq : input.length = 3 * count) (output variableCounter clauses : List Bool)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (included : ∀ t ∈ input, t ∈ tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    (advance (TM2.step program))^[steps tokens input]
      (some ⟨some (labels .entry), clean ambient 0,
        loopTapes tape base (BinaryNameSearch.stream input) output variableCounter clauses⟩) =
      some ⟨done, clean ambient 0,
        loopTapes tape base [] ((outputBody tokens input).reverse ++ output)
          (List.replicate (3 * count) true ++ variableCounter)
…

    Mentions: OAI.UniqueGamesTheorem.BinaryRenameLoop.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryRenameLoop.steps, OAI.UniqueGamesTheorem.BinaryRenameLoop.clean, OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes, OAI.UniqueGamesTheorem.BinaryRenameLoop.outputBody

  46. def OAI.UniqueGamesTheorem.BinaryRenameLoop.triplesInTime line 437

    Source documentation

    The machine's bit-length bound includes every peek, literal run, and tally.

    def triplesInTime (tokens input : List Token) (count : Nat)
    (length_eq : input.length = 3 * count) (output variableCounter clauses : List Bool)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (included : ∀ t ∈ input, t ∈ tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .entry), clean ambient 0,
        loopTapes tape base (BinaryNameSearch.stream input) output variableCounter clauses⟩
      (some ⟨done, clean ambient 0,
        loopTapes tape base [] ((outputBody tokens input).reverse ++ output)
          (List.replicate (3 * count) true ++ variableCounter)
…

    Mentions: OAI.UniqueGamesTheorem.BinaryRenameLoop.Token, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameSearch.stream, OAI.UniqueGamesTheorem.BinaryRenameLoop.clean, OAI.UniqueGamesTheorem.BinaryRenameLoop.loopTapes, OAI.UniqueGamesTheorem.BinaryRenameLoop.outputBody