MachineCompare.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

A destructive equality test on two actual Bool stacks

Each loop transition pops both stacks and compares only the two finite head registers. A sticky mismatch flag makes the loop continue after disagreement. The final empty/empty test selects an equal or different continuation and resets all comparison registers. The ambient state and every other tape are preserved.

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.Alphabet line 24
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State line 25
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.exitAt line 28
Source documentation
An optional continuation, without reading or writing any tape.
```
def exitAt (exit : Option Λ) : TM2.Stmt (Alphabet K) Λ (State σ) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.finish line 34
Source documentation
Clear both head registers and the mismatch flag after choosing the exit.
```
def finish (exit : Option Λ) : TM2.Stmt (Alphabet K) Λ (State σ) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.loop line 39
Source documentation
The only comparison performed by the program is on two Option Bool heads. In particular, no statement is given a whole-list equality oracle.
```
def loop (left right : K) (loopLabel : Λ) (equalExit differentExit : Option Λ) :
    TM2.Stmt (Alphabet K) Λ (State σ) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch line 50
Source documentation
Specification-only outcome, also recording an earlier mismatch.
```
def mismatch (flag : Bool) (leftWord rightWord : List Bool) : Bool :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch_nil_nil line 53
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch_nil_cons line 56
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch_cons_nil line 59
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch_true line 62
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch_cons line 65
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.stepAux_exitAt line 70
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.stepAux_finish line 75
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.update_left line 81
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.update_right line 94
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.step_empty line 100
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.step_nil_cons line 117
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.step_cons_nil line 132
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.step_cons_cons line 147
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.trace_left_empty line 164

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.compareTrace_flag line 191

Source documentation

The exact trace with a possibly pre-existing mismatch. Every input symbol is consumed even when disagreement has already been detected.

theorem compareTrace_flag (left right : K) (distinct : left ≠ right)
    (loopLabel : Λ) (equalExit differentExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet K) Λ (State σ))
    (atLoop : program loopLabel = loop left right loopLabel equalExit differentExit)
    (base : K → List Bool) (leftWord rightWord : List Bool) (ambient : σ) (flag : Bool)
    (leftRegister rightRegister : Option Bool) :
    (MachineComposition.advance (TM2.step program))^[max leftWord.length rightWord.length + 1]
      (some ⟨some loopLabel, (ambient, flag, leftRegister, rightRegister),
        tapesAt left right base leftWord rightWord⟩) =
      some ⟨if mismatch flag leftWord rightWord then differentExit else equalExit,
        (ambient, false, none, none), tapesAt left right base [] []⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.loop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.mismatch

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.compareTrace line 228

Source documentation

With a clear initial flag, the final continuation tests equality of the two complete original words. Both tapes and all comparison registers are empty.

theorem compareTrace (left right : K) (distinct : left ≠ right)
    (loopLabel : Λ) (equalExit differentExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet K) Λ (State σ))
    (atLoop : program loopLabel = loop left right loopLabel equalExit differentExit)
    (base : K → List Bool) (leftWord rightWord : List Bool) (ambient : σ)
    (leftRegister rightRegister : Option Bool) :
    (MachineComposition.advance (TM2.step program))^[max leftWord.length rightWord.length + 1]
      (some ⟨some loopLabel, (ambient, false, leftRegister, rightRegister),
        tapesAt left right base leftWord rightWord⟩) =
      some ⟨if leftWord = rightWord then equalExit else differentExit,
        (ambient, false, none, none), tapesAt left right base [] []⟩ := by
…

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.compareTrace_fromTapes line 243
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.drained_other line 257
Source documentation
The final tape family agrees with the original at every unselected tape.
```
theorem drained_other (left right k : K) (notLeft : k ≠ left) (notRight : k ≠ right)
    (base : K → List Bool) : tapesAt left right base [] [] k = base k :=
…
```

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.compareInTime line 262

Source documentation

An actual timed execution witness, with the exact stored transition count.

def compareInTime (left right : K) (distinct : left ≠ right)
    (loopLabel : Λ) (equalExit differentExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet K) Λ (State σ))
    (atLoop : program loopLabel = loop left right loopLabel equalExit differentExit)
    (base : K → List Bool) (ambient : σ) (leftRegister rightRegister : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some loopLabel, (ambient, false, leftRegister, rightRegister), base⟩
      (some ⟨if base left = base right then equalExit else differentExit,
        (ambient, false, none, none), tapesAt left right base [] []⟩)
      (max (base left).length (base right).length + 1) where
…

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.compareInTime_steps line 277