OAI/Computability/UniqueGames/Machines/FinalCNFMachineLemmas.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Buffer line 26
2. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.readUnarySlots line 34

   Source documentation

   Read fixed register slots from the actual unary 0/1 word encoding. Each slot consumes one symbol for false and two symbols for true.

   def readUnarySlots (source : K) : List (Fin N) →
       TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) →
       TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N)
     | [], next => next
     | i :: slots, next =>
         .pop source (fun state head =>
           (state.1, Function.update state.2 i (head.getD false)))
           (.branch (fun state => state.2 i)
             (.pop source (fun state _ => state) (readUnarySlots source slots next))
             (readUnarySlots source slots next))

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Buffer

3. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBits line 45
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBits_eq_encodeWords line 48
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBits_length_le line 55
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.statementPushBound_readUnarySlots line 65
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.stepAux_readUnarySlots line 77

   Source documentation

   Exact stack and register semantics, retaining every unread suffix bit.

   theorem stepAux_readUnarySlots (source : K) (slots : List (Fin N))
       (next : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N))
       (ambient : σ) (bits buffer : Buffer N) (tapes : K → List Bool)
       (suffix : List Bool) :
       TM2.stepAux (readUnarySlots source slots next) (ambient, buffer)
           (Function.update tapes source (unaryBits slots bits ++ suffix)) =
         TM2.stepAux next (ambient, MachineFixedBlockMap.fill slots bits buffer)
           (Function.update tapes source suffix) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Buffer, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.readUnarySlots, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedBlockMap.fill

8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.stepAux_readUnaryAll line 101
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBlockMapAt line 116

   Source documentation

   A fixed table lookup or fixed pattern permutation can follow immediately after the physical unary decoding, with one genuine finite TM2 transition.

   def unaryBlockMapAt {M : Nat} (source destination : K) (F : Buffer N → Buffer M)
       (exit : Option Λ) : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Buffer

10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.stepAux_unaryBlockMapAt line 124
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.step_unaryBlockMapAt line 139
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBlockInTime line 152
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.unaryBits_relation line 169
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.readerStateEquiv line 182

    Source documentation

    Merely rearranges finite registers to match the affine-emitter state. No tape content or unbounded integer is moved into the internal state.

    def readerStateEquiv (σ : Type) (N : Nat) :
        (((σ × Unit) × Option Bool) × Buffer N) ≃ (((σ × Buffer N) × Unit) × Option Bool) where
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Buffer

15. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.State line 193
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.readRelationAt line 195
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.stepAux_readRelationAt line 200
18. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape line 221
19. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList line 226
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_getElem?_ctorIdx_eq line 229
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape.enumList_nodup line 233
22. instance OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.(instance at line 235) line 235
23. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient line 239
24. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan line 240
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.values line 242
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan line 246

    Source documentation

    Output variable count and output clause count, in the checked CNF codec.

    def headerPlan : Plan :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan

27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_length line 250
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_bits line 253
29. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.source line 261
30. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Label line 264
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guard line 276
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program line 285

    Source documentation

    The actual finite program. All graph-dependent naturals remain on unary stacks. The only buffered graph data is one fixed 4096-bit relation table.

    def program (headerPlan rowPlan : Plan) :
        Label headerPlan.length rowPlan.length →
          TM2.Stmt (fun _ : Tape => Bool) (Label headerPlan.length rowPlan.length) (State Unit)
      | .copyFirst => Reduction.MachineTransfer.loopAt .input .scratch id false .copyFirst
          (some .copySecond)
      | .copySecond => MachineCopy.forkLoop .scratch .input .archive false .copySecond
          (some .startVertices)
      | .startVertices => Hastad.SourceMachine.fieldStart .vertices .readVertices
      | .readVertices => Hastad.SourceMachine.fieldLoop .input .vertices .readVertices (some .startDarts)
      | .startDarts => Hastad.SourceMachine.fieldStart .darts .readDarts
      | .readDarts => Hastad.SourceMachine.fieldLoop .input .darts .readDarts (some .seedIndex)
      | .seedIndex => .push .rowIndex (fun _ => false)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.State, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStart, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldLoop

33. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.machine line 332
34. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles line 343
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_injective line 347
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime line 352

    Source documentation

    The head-access call is part of this concrete program, with its actual finite labels and framed tape effects. Its data are read from the table.

    def headPhaseInTime (headerPlan rowPlan : Plan) (base : Tape → List Bool)
        (table : GenericGraphTables.Table 64) (e : Fin table.darts)
        (hTable : base .archive = GenericGraphTables.tableBits table)
        (hReverse : base .reverseIndex = encodeWord (Lookup.headIndex table e).val)
        (hHead : base .head = []) (hScratch : base .scratch = []) (ambient : Ambient) :
        StateTransition.EvalsToInTime (TM2.step (program headerPlan rowPlan))
          ⟨some .headTableFirst, ((ambient, ()), none), base⟩
          (some ⟨some .readRelation, ((ambient, ()), none),
            Lookup.headLookupTapes headRoles base table e⟩)
          (Lookup.headTimePolynomial.eval (GenericGraphTables.tableBits table).length) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles

37. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.workingTapes line 368
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.workingTapes_operands line 381
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.update_working_input line 388
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.update_working_tail line 395
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.update_working_head line 402
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.update_working_accumulator line 409
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.update_working_rowIndex line 416
44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.source_ne_scratch line 424
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.source_ne_accumulator line 427
46. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.redirectLabel line 444
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.redirectCfg line 448
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.redirectStmt line 453

    Source documentation

    Structural redirection changes only the destinations of goto and halt.

    def redirectStmt (labels : Λ → Λ') (haltTarget : Option Λ') :
        TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ' σ
      | .push k f next => .push k f (redirectStmt labels haltTarget next)
      | .peek k f next => .peek k f (redirectStmt labels haltTarget next)
      | .pop k f next => .pop k f (redirectStmt labels haltTarget next)
      | .load f next => .load f (redirectStmt labels haltTarget next)
      | .branch test yes no => .branch test
          (redirectStmt labels haltTarget yes) (redirectStmt labels haltTarget no)
      | .goto label => .goto (fun state => labels (label state))
      | .halt => match haltTarget with
        | none => .halt
        | some label => .goto (fun _ => label)

49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.stepAux_redirect line 466
50. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.chosen line 487

    Source documentation

    The raw machine has thirteen tapes. These are precisely the twelve non-output tapes, including the original input and retained archive.

    def chosen : List Tape :=
    …

51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.chosen_length line 491
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.mem_chosen line 493
53. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.Label line 496
54. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.cleanupLabel line 500
55. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.resetLabel line 503
56. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.cleanupEntry line 505
57. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.completedProgram line 508
58. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.completedMachine line 516
59. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.embeddedCfg line 527
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.step_simulation line 532
61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.embedded_init line 551
62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.finalTapes_eq line 555
63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.haltList_eq line 565
64. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.cleanupExecution line 572

    Source documentation

    Actual drains followed by a real state-reset instruction reach canonical halt.

    def cleanupExecution (headerPlan rowPlan : Plan) (state : State Unit) (base : Tape → List Bool) :
        StateTransition.EvalsToInTime (completedMachine headerPlan rowPlan).step
          ⟨cleanupEntry headerPlan rowPlan, state, base⟩
          (some (haltList (completedMachine headerPlan rowPlan) (base .output)))
          (MachineDrainMany.steps chosen base + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.completedMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.cleanupEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.chosen

65. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.outputsInTime line 605

    Source documentation

    The extra cost is bounded from the actual raw execution, independently of the contents of its dirty private tapes and finite state.

    def outputsInTime (headerPlan rowPlan : Plan) (input output : List Bool)
        (state : State Unit) (base : Tape → List Bool) (budget : Nat)
        (raw : StateTransition.EvalsToInTime
          (FinalCNFMachine.Program.machine headerPlan rowPlan).step
          (initList (FinalCNFMachine.Program.machine headerPlan rowPlan) input)
          (some ⟨none, state, base⟩) budget)
        (correctOutput : base .output = output) :
        TM2OutputsInTime (completedMachine headerPlan rowPlan) input (some output)
          (budget + 12 * (input.length + budget *
            Runtime.programPushBound (FinalCNFMachine.Program.machine headerPlan rowPlan) + 1) + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.completedMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound

66. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.completedTime line 638

    Source documentation

    For fixed raw plans, polynomial raw time gives polynomial cleanup time.

    noncomputable def completedTime (headerPlan rowPlan : Plan) (rawTime : Polynomial Nat) : Polynomial Nat :=
    …

67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFCleanup.completedTime_eval line 642
68. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerFrame line 663

    Source documentation

    Explicit tape frame used during the header phase; all unlisted work tapes are empty. The archive is separate from the unread input.

    def headerFrame (input archive vertices darts rowIndex tail head accumulator : List Bool) :
        Tape → List Bool
      | .input => input
      | .archive => archive
      | .vertices => vertices
      | .darts => darts
      | .rowIndex => rowIndex
      | .tail => tail
      | .head => head
      | .accumulator => accumulator
      | _ => []

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape

69. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes line 675
70. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes line 680

    Source documentation

    Exact row-guard handoff: the original table is protected in archive, the output header is accumulated in reverse, and the row index is unary zero.

    def headerResultTapes (n m : Nat) (rowsBits : List Bool) : Tape → List Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape

71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_input line 685
72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_archive line 688
73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_accumulator line 691
74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_rowIndex line 695
75. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial line 699

    Source documentation

    A fixed polynomial in the complete encoded input length.

    noncomputable def headerTimePolynomial : Polynomial Nat :=
    …

76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial_eval line 702
77. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerInTime line 708

    Source documentation

    An actual entry-to-guard trace, valid for any unread row suffix and every finite ambient buffer. No execution premise is supplied by the caller.

    def headerInTime (rowPlan : Plan) (n m : Nat) (rowsBits : List Bool) (ambient : Ambient) :
        StateTransition.EvalsToInTime (TM2.step (program headerPlan rowPlan))
          ⟨some .copyFirst, ((ambient, ()), none),
            headerInputTapes (encodeWords [n, m] ++ rowsBits)⟩
          (some ⟨some .guard, ((ambient, ()), none), headerResultTapes n m rowsBits⟩)
          (headerTimePolynomial.eval (encodeWords [n, m] ++ rowsBits).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes

78. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits line 838

    Source documentation

    The unread graph rows in the actual graph codec.

    def tableRowsBits (table : PCP.GenericGraphTables.Table 64) : List Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table

79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tableBits_header_rows line 841
80. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tableHeaderInTime line 848

    Source documentation

    Specialization to the entire input of the actual numbered graph codec.

    def tableHeaderInTime (rowPlan : Plan) (table : PCP.GenericGraphTables.Table 64)
        (ambient : Ambient) :
        StateTransition.EvalsToInTime (TM2.step (program headerPlan rowPlan))
          ⟨some .copyFirst, ((ambient, ()), none),
            headerInputTapes (PCP.GenericGraphTables.tableBits table)⟩
          (some ⟨some .guard, ((ambient, ()), none),
            headerResultTapes table.vertices table.darts (tableRowsBits table)⟩)
          (headerTimePolynomial.eval (PCP.GenericGraphTables.tableBits table).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits

81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerInput_configuration line 859
82. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime line 869

    Source documentation

    The same bounded phase begins at the machine's genuine initial configuration.

    def initializedTableHeaderInTime (rowPlan : Plan) (table : PCP.GenericGraphTables.Table 64) :
        StateTransition.EvalsToInTime (machine headerPlan rowPlan).step
          (initList (machine headerPlan rowPlan) (PCP.GenericGraphTables.tableBits table))
          (some ⟨some .guard, ((((), fun _ => false), ()), none),
            headerResultTapes table.vertices table.darts (tableRowsBits table)⟩)
          (headerTimePolynomial.eval (PCP.GenericGraphTables.tableBits table).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits