CompareLoop.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.Label line 13
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList line 18
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_getElem?_ctorIdx_eq line 21
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_nodup line 25
instance OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.(instance at line 27) line 27

def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.statement line 34

Source documentation

A composable block with exactly seven internal control labels.

def statement (labels : Label → Λ) (next : Λ) :
    Label → TM2.Stmt Alphabet Λ (State q)
  | .leftFirst => compareStatement (MachineFieldProfile.copyStatement
      (Reduction.MachineTransfer.loopAt .tail .scratch id false
        (labels .leftFirst) (some (labels .leftSecond))))
  | .leftSecond => compareStatement (MachineFieldProfile.copyStatement
      (MachineCopy.forkLoop .scratch .tail .compareLeft false
        (labels .leftSecond) (some (labels .rightFirst))))
  | .rightFirst => compareStatement (MachineFieldProfile.copyStatement
      (Reduction.MachineTransfer.loopAt .head .scratch id false
        (labels .rightFirst) (some (labels .rightSecond))))
  | .rightSecond => compareStatement (MachineFieldProfile.copyStatement
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.Label, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt

theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.compareProgram_at line 53

def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime line 65

Source documentation

Compare arbitrary words while restoring every tape, including work tapes. All program hypotheses specify only the statements at the seven labels.

def compareWordsInTime (labels : Label → Λ) (next : Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State q))
    (atLabel : ∀ label, program (labels label) = statement labels next label)
    (base : Tape → List Bool)
    (hLeft : base .compareLeft = []) (hRight : base .compareRight = [])
    (hScratch : base .scratch = [])
    (relation : GenericGraphTables.RelationTable q) (oldLoop : Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .leftFirst), normal relation oldLoop, base⟩
      (some ⟨some next, normal relation (decide (base .tail = base .head)), base⟩)
      (2 * ((base .tail).length + 1) + 2 * ((base .head).length + 1) +
        max (base .tail).length (base .head).length + 2) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.statement, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.RelationTable

def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime line 121
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.encodeWord_eq_iff line 124

def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.compareInTime line 134

Source documentation

The stored flag is equality of the actual unary endpoint names.

def compareInTime (labels : Label → Λ) (next : Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State q))
    (atLabel : ∀ label, program (labels label) = statement labels next label)
    (base : Tape → List Bool) (tailName headName : Nat)
    (hTail : base .tail = encodeWord tailName) (hHead : base .head = encodeWord headName)
    (hLeft : base .compareLeft = []) (hRight : base .compareRight = [])
    (hScratch : base .scratch = [])
    (relation : GenericGraphTables.RelationTable q) (oldLoop : Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .leftFirst), normal relation oldLoop, base⟩
      (some ⟨some next, normal relation (decide (tailName = headName)), base⟩)
      (comparisonTime tailName headName) := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le line 151
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le_of_lt line 158

def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime_bounded line 166

Source documentation

A linear word-length budget, with the actual complete execution retained.

def compareWordsInTime_bounded (labels : Label → Λ) (next : Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State q))
    (atLabel : ∀ label, program (labels label) = statement labels next label)
    (base : Tape → List Bool)
    (hLeft : base .compareLeft = []) (hRight : base .compareRight = [])
    (hScratch : base .scratch = [])
    (relation : GenericGraphTables.RelationTable q) (oldLoop : Bool)
    (N : Nat) (hTail : (base .tail).length ≤ N) (hHead : (base .head).length ≤ N) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .leftFirst), normal relation oldLoop, base⟩
      (some ⟨some next, normal relation (decide (base .tail = base .head)), base⟩)
      (5 * N + 6) := by
…

def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop line 185
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.rowState line 188
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop_eq_graph line 191
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.rowContext_eq line 198
def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.compareRowInTime line 205
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.relationFromRowState line 223