MachineBinaryHeaderMachine.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

An actual finite Boolean-stack routine prepending two unary header words to an already restored serialized body. It consumes counters containing n and m true bits, respectively, in exactly n + m + 4 transitions. All ambient stacks and the finite ambient state are preserved. The input counters need no separate counting pass: a caller can accumulate them while constructing the body.

The generic placement theorem uses only four displayed instruction equations. The concrete machine below has three Boolean stacks and four control labels; its final transfer halts directly. This is a staged configuration computation, not a single-input initList assertion that silently assumes two extra inputs.

abbrev OAI.UniqueGamesTheorem.BinaryHeaderMachine.Alphabet line 27
abbrev OAI.UniqueGamesTheorem.BinaryHeaderMachine.State line 28
def OAI.UniqueGamesTheorem.BinaryHeaderMachine.delimiter line 35
Source documentation
A fixed one-bit push; the finite register is cleared before continuation.
```
def delimiter (destination : K) (next : Λ) : TM2.Stmt (Alphabet (K := K)) Λ (State A) :=
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryHeaderMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryHeaderMachine.State
def OAI.UniqueGamesTheorem.BinaryHeaderMachine.tapes line 39
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.tapes_variables line 44
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.tapes_clauses line 51
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.tapes_destination line 58
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.tapes_other line 64
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.update_variables line 70
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.update_clauses line 87
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.update_destination line 101
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.clauseDelimiterStep line 120
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.variableDelimiterStep line 132
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.clauseCounterTrace line 144
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.variableCounterTrace line 164
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.joinTrace line 183

theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.headerTrace line 190

Source documentation

The actual four-phase routine, with exact unary header and preserved body.

theorem headerTrace (n m : Nat) (body : List Bool) (register : Option Bool) :
    (advance (TM2.step program))^[n + m + 4]
      (some ⟨some clauseStart, (ambient, register),
        tapes variableTape clauses destination base
          (List.replicate n true) (List.replicate m true) body⟩) =
      some ⟨exit, (ambient, none),
        tapes variableTape clauses destination base [] [] (encodeWord n ++ encodeWord m ++ body)⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.BinaryHeaderMachine.tapes

def OAI.UniqueGamesTheorem.BinaryHeaderMachine.headerInTime line 219
abbrev OAI.UniqueGamesTheorem.BinaryHeaderMachine.ConcreteTape line 234
abbrev OAI.UniqueGamesTheorem.BinaryHeaderMachine.ConcreteLabel line 235
def OAI.UniqueGamesTheorem.BinaryHeaderMachine.concreteProgram line 237
abbrev OAI.UniqueGamesTheorem.BinaryHeaderMachine.machine line 244
def OAI.UniqueGamesTheorem.BinaryHeaderMachine.start line 256
Source documentation
Concrete entry configuration carries two physical counters and the body.
```
def start (n m : Nat) (body : List Bool) : machine.Cfg :=
…
```
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.haltList_eq line 260
def OAI.UniqueGamesTheorem.BinaryHeaderMachine.machineInTime line 269
Source documentation
Genuine staged execution of the concrete four-label finite machine.
```
def machineInTime (n m : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime machine.step (start n m body)
      (some (haltList machine (encodeWord n ++ encodeWord m ++ body))) (n + m + 4) := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryHeaderMachine.start, OAI.UniqueGamesTheorem.BinaryHeaderMachine.machine
theorem OAI.UniqueGamesTheorem.BinaryHeaderMachine.machine_finiteAlphabet line 279