OAI/Computability/UniqueGames/PCP/RawInitialMachineRows.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The six incidence rows are emitted by the actual finite program, with their exact order, full relation lists, transition count, and tape frame.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.advance line 16
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.outputTapes line 18
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.outputTapes_reversed line 21
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.outputTapes_other line 24
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.outputTapes_twice line 28
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.trace_trans line 35
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.copyTrace line 39
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.closeTailTrace line 47
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.closeReverseTrace line 55
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.reverse_encodeWord_add line 65
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.rowEndBits line 71
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.rowEndTrace line 75
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.rowEndBits_append line 107
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.falseRowTrace line 116
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.trueRowTrace line 154
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.pairWords line 183
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.pairTrace line 188
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.rowsTrace line 216

    Source documentation

    Exact execution of all six incidence rows. Relation tables stay symbolic; no entry is discarded and every non-output tape is preserved.

    theorem rowsTrace (base : Tape → List Bool) (n i : ℕ)
    (names : RawInitialRows.Names) (signs : Signs)
    (hvariables : base .variables = encodeWord n) (hindex : base .index = encodeWord i)
    (hname0 : base (.field 0) = encodeWord names.1)
    (hname2 : base (.field 2) = encodeWord names.2.1)
    (hname4 : base (.field 4) = encodeWord names.2.2)
    (hscratch : base .scratch = []) :
    advance^[6 * n + 18 * i + 2 * (names.1 + names.2.1 + names.2.2) + 48]
      (some ⟨some (.scan (.tailVariables 0)), (signs, none), base⟩) =
      some ⟨some (.cleanupField 0), (signs, none),
        outputTapes base (encodeWords (RawInitialRows.clauseWords n i names signs)).reverse⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.Names, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.advance, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.outputTapes, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseWords

  19. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineRows.rowsInTime line 263