MachineBinaryTokenMachine.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

An actual finite Boolean-stack machine which removes formula/clause markers from valid ordinary-binary 3CNF encodings. Literal signs and every bit of each framed binary name survive in their original occurrence order. The first pass accumulates the output in reverse; the checked transfer routine restores order.

The machine is specified on the semantic encoded-input domain. It does not claim to reject every malformed or noncanonical input. In particular, the name-copying loop does not check canonicality: valid input already supplies it. All transitions inspect only finite control and one popped bit. No branch or load computes a whole-list function or converts a binary name to unary.

abbrev OAI.UniqueGamesTheorem.BinaryTokenMachine.Tape line 29
abbrev OAI.UniqueGamesTheorem.BinaryTokenMachine.Alphabet line 30
abbrev OAI.UniqueGamesTheorem.BinaryTokenMachine.State line 31
inductive OAI.UniqueGamesTheorem.BinaryTokenMachine.Label line 33
def OAI.UniqueGamesTheorem.BinaryTokenMachine.afterName line 42
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.afterName_zero line 45
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.afterName_one line 46
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.afterName_two line 47
def OAI.UniqueGamesTheorem.BinaryTokenMachine.jump line 49
def OAI.UniqueGamesTheorem.BinaryTokenMachine.clauseInstruction line 53
Source documentation
Discard a clause marker, or finish at the final formula terminator.
```
def clauseInstruction : TM2.Stmt Alphabet Label State :=
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryTokenMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryTokenMachine.Label, OAI.UniqueGamesTheorem.BinaryTokenMachine.State
def OAI.UniqueGamesTheorem.BinaryTokenMachine.signInstruction line 60
def OAI.UniqueGamesTheorem.BinaryTokenMachine.nameInstruction line 67
Source documentation
Copy both symbols of a payload pair, or copy the name terminator.
```
def nameInstruction (slot : Fin 3) : TM2.Stmt Alphabet Label State :=
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryTokenMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryTokenMachine.Label, OAI.UniqueGamesTheorem.BinaryTokenMachine.State
def OAI.UniqueGamesTheorem.BinaryTokenMachine.program line 79
abbrev OAI.UniqueGamesTheorem.BinaryTokenMachine.machine line 87
def OAI.UniqueGamesTheorem.BinaryTokenMachine.tapes line 98
def OAI.UniqueGamesTheorem.BinaryTokenMachine.cfg line 101
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tapes_zero line 105
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tapes_one line 108
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tapes_two line 111
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.update_zero line 114
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.update_one line 120
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.clauseStep line 126
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.finalStep line 133
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.signStep line 140
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.nameEndStep line 148
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.nameDigitStep line 156
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.nameTrace line 165
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.literalTrace line 182
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.joinTrace line 199

theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.clauseTrace line 204

Source documentation

Three literal subroutines return to the next clause boundary.

theorem clauseTrace (clause : Clause) (suffix reversed output : List Bool)
    (register : Option Bool) :
    (advance machine.step)^[clauseNameSize clause + 6]
      (some (cfg (some (.sign 0)) (clauseBits clause ++ suffix) reversed output register)) =
      some (cfg (some .clause) suffix ((clauseBits clause).reverse ++ reversed) output) := by
…

Mentions: OAI.UniqueGamesTheorem.BinaryTokenMachine.cfg

def OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens line 225
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens_nil line 227
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens_cons line 229
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens_length line 233

theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.stripTrace line 243

Source documentation

Exact first-pass run, retaining the unread suffix and ambient output.

theorem stripTrace (clauses : List Clause) (suffix reversed output : List Bool)
    (register : Option Bool) :
    (advance machine.step)^[7 * clauses.length + namesBitSize clauses + 1]
      (some (cfg (some .clause) (clausesBits clauses ++ suffix) reversed output register)) =
      some (cfg (some .restore) suffix ((tokens clauses).reverse ++ reversed) output) := by
…

Mentions: OAI.UniqueGamesTheorem.BinaryTokenMachine.cfg, OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens

theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.restoreTrace line 275
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.initList_eq line 292
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.haltList_eq line 299
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.acceptTrace line 306
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.haltStep line 324

theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tokenTrace line 330

Source documentation

Exact transition count for the complete finite-machine computation.

theorem tokenTrace (formula : Formula) :
    (advance machine.step)^[13 * formula.clauses.length +
        3 * namesBitSize formula.clauses + 3]
      (some (initList machine (formulaBits formula))) =
      some (haltList machine (tokens formula.clauses)) := by
…

Mentions: OAI.UniqueGamesTheorem.BinaryTokenMachine.machine, OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens

theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.tokenSteps_le line 339
def OAI.UniqueGamesTheorem.BinaryTokenMachine.outputsInTime line 345
def OAI.UniqueGamesTheorem.BinaryTokenMachine.computableInPolyTime line 354
Source documentation
A displayed finite machine and linear polynomial in the ordinary input bit length, proved by the transitions above rather than assumed by a caller.
```
noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime BinaryEncoding.formulaBits (id : List Bool → List Bool)
      (fun formula => tokens formula.clauses) where
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits, OAI.UniqueGamesTheorem.BinaryTokenMachine.tokens
theorem OAI.UniqueGamesTheorem.BinaryTokenMachine.machine_finiteAlphabet line 369