RawInitialMachineReadClause.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Read exactly one concrete six-field CNF clause in the actual global machine, then execute its real sign-loading instruction. No extra finish transition is inserted. Every unrelated tape and the unread input suffix are preserved.

def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.fieldValue line 17
Source documentation
The six actual serialized fields, in name/sign/name/sign/name/sign order.
```
def fieldValue {n : ℕ} (c : Target.Clause n) (j : Fin 6) : ℕ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Clause
def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.recordTapes line 23
Source documentation
Full caller frame after the clause fields have been consumed.
```
def recordTapes {n : ℕ} (base : Tape → List Bool) (c : Target.Clause n)
    (suffix : List Bool) : Tape → List Bool
  | .input => suffix
  | .field j => encodeWord (fieldValue c j)
  | k => base k
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.fieldValue
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.recordTapes_input line 29
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.recordTapes_field line 33
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.recordTapes_other line 37
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.recordTapes_name line 45
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.trace_trans line 51

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.fieldsTrace line 56

Source documentation

Six actual field routines, stopping directly at the global sign loader.

theorem fieldsTrace {n : ℕ} (base : Tape → List Bool) (c : Target.Clause n)
    (suffix : List Bool)
    (hinput : base .input = encodeWords (Complexity.clauseWords c) ++ suffix)
    (hempty : ∀ j, base (.field j) = []) (state : State) :
    (MachineComposition.advance (TM2.step program))^[
        (encodeWords (Complexity.clauseWords c)).length + 6]
      (some ⟨some (.fieldStart 0), state, base⟩) =
      some ⟨some .loadSigns, (state.1, none), recordTapes base c suffix⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Complexity.clauseWords, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.recordTapes

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.readClauseTrace line 152
def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineReadClause.readClauseInTime line 172