RawInitialMachineStart.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Actual execution of the raw initial graph machine from its standard input configuration to the first clause-loop guard. The unread clause bits are preserved verbatim, and all tape contents at the boundary are explicit.

def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.inputTapes line 16
def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.firstTapes line 20
def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.counterTapes line 25
def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.headerTapes line 31

def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.startTapes line 39

Source documentation

Complete machine frame at the first clause-loop guard.

def startTapes (n m : ℕ) (clauseBits : List Bool) : Tape → List Bool
  | .input => clauseBits
  | .variables => encodeWord n
  | .counter => encodeWord m
  | .index => [false]
  | .reversed => (encodeWords [n + m + 1, 6 * m + 1]).reverse
  | _ => []

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.initList_eq line 47
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.trace_trans line 56

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.readCountersTrace line 61

Source documentation

The two actual header-field readers reach the prepared counter boundary.

theorem readCountersTrace (n m : ℕ) (clauseBits : List Bool) :
    (MachineComposition.advance (TM2.step program))^[n + m + 4]
      (some (initList machine (encodeWords [n, m] ++ clauseBits))) =
      some ⟨some .scanN, initialState, counterTapes n m clauseBits⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.counterTapes

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.headersTrace line 95
Source documentation
Instantiation of the checked arithmetic phase in the actual global program.
```
theorem headersTrace (n m : ℕ) (clauseBits : List Bool) :
    (MachineComposition.advance (TM2.step program))^[2 * n + 4 * m + 8]
      (some ⟨some .scanN, initialState, counterTapes n m clauseBits⟩) =
      some ⟨some .initializeIndex, initialState, headerTapes n m clauseBits⟩ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.counterTapes, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.headerTapes
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.initializeIndexTrace line 114

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.startTrace line 127

Source documentation

Exact startup trace for arbitrary encoded clause-tail data.

theorem startTrace (n m : ℕ) (clauseBits : List Bool) :
    (MachineComposition.advance (TM2.step program))^[3 * n + 5 * m + 13]
      (some (initList machine (encodeWords [n, m] ++ clauseBits))) =
      some ⟨some .guard, initialState, startTapes n m clauseBits⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.startTapes

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.formulaStartTrace line 138

Source documentation

Startup from the actual serialized CNF, with its untouched clause tail.

theorem formulaStartTrace (F : Target.Formula) :
    (MachineComposition.advance (TM2.step program))^[
        3 * F.variables + 5 * F.clauses.length + 13]
      (some (initList machine (formulaBits F))) =
      some ⟨some .guard, initialState,
        startTapes F.variables F.clauses.length
          (encodeWords (F.clauses.flatMap clauseWords))⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.startTapes

def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.startInTime line 148
def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineStart.formulaStartInTime line 157