OAI/Computability/UniqueGames/PCP/SourceFieldArrayLemmas.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.finish line 15
2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.finishStep line 19
3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes line 30

   Source documentation

   Exact successive stack updates, in the original field order.

   def sequenceTapes (source : K) (destination : Nat → K) (base : K → List Bool)
       (offset : Nat) (values : List Nat) (suffix : List Bool) : K → List Bool :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination

4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTrace line 40

   Source documentation

   The trace is built from the actual single-field transitions. The only program premises identify the finitely many statements used by this record.

   theorem sequenceTrace (source : K) (destination : Nat → K)
       (start loopLabel : Nat → Λ) (exit : Option Λ)
       (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.loopLabel, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.program

5. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceInTime line 99
6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequence_time_eq_length line 121
7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes_other line 126
8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes_source line 141
9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes_selected line 157

   Source documentation

   Distinct field destinations contain exactly their own encoded value.

   theorem sequenceTapes_selected (source : K) (destination : Nat → K)
       (base : K → List Bool) (offset : Nat) (values : List Nat) (suffix : List Bool)
       (j : Nat) (hj : j < values.length)
       (hsep : ∀ r, r < values.length → source ≠ destination (offset + r))
       (hdist : ∀ r s, r < values.length → s < values.length →
         destination (offset + r) = destination (offset + s) → r = s) :
       sequenceTapes source destination base offset values suffix (destination (offset + j)) =
         encodeWord (values[j]'hj) ++ base (destination (offset + j)) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes

10. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.boundedIndex line 206

    Source documentation

    Extend finite indices harmlessly outside the range used by the machine.

    def boundedIndex (q j : Nat) : Fin (q + 1) := ⟨min j q, by omega⟩

11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.boundedIndex_val line 208
12. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination line 211
13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.startLabel line 212
14. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.loopLabel line 213
15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination_ne_source line 215
16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination_injective_below line 223
17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination_eq_succ line 230
18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.output_source line 234
19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.output_field line 242
20. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.program line 256

    Source documentation

    Every label either seeds one field, scans that field, or executes the final halt.

    def program (q : Nat) (label : Fin (q + 1) × Bool) :
        TM2.Stmt (fun _ : Fin (q + 1) => Bool) (Fin (q + 1) × Bool) (Unit × Option Bool) :=
    …

21. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.machine line 265
22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.atStart line 276
23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.atLoop line 280
24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.atDone line 285
25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.machineInTime line 288
26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound line 318

    Source documentation

    The same actual execution has a linear bound measured in the complete input stack, including its unread suffix.

    def machineInTime_inputBound (q : Nat) (values : List Nat) (hlen : values.length = q)
        (base : Fin (q + 1) → List Bool) (suffix : List Bool)
        (hinput : base 0 = encodeWords values ++ suffix) (register : Option Bool) :
        StateTransition.EvalsToInTime (machine q).step
          ⟨some (startLabel q 0), ((), register), base⟩
          (some ⟨none, ((), none), sequenceTapes (0 : Fin (q + 1)) (destination q) base 0 values suffix⟩)
          ((base 0).length + q + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.machine, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.startLabel, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination

27. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sixFieldsInTime line 333

    Source documentation

    The six natural fields of a three-literal clause use seven actual stacks.

    def sixFieldsInTime (base : Fin 7 → List Bool) (a b c d e f : Nat) (suffix : List Bool)
        (hinput : base 0 = encodeWords [a, b, c, d, e, f] ++ suffix) (register : Option Bool) :
        StateTransition.EvalsToInTime (machine 6).step
          ⟨some (startLabel 6 0), ((), register), base⟩
          (some ⟨none, ((), none),
            sequenceTapes (0 : Fin 7) (destination 6) base 0 [a, b, c, d, e, f] suffix⟩)
          (a + b + c + d + e + f + 13) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.machine, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.startLabel, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.destination

28. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.discardFieldsTrace line 359

    Source documentation

    Compose the actual unary scanners for a fixed sequence of control labels. The zero-field case is an identity, so the head register starts and ends clear.

    theorem discardFieldsTrace (source : K) (label : Nat → Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program

29. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape line 402
30. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Label line 406
31. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.fieldDestination line 412
32. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readStart line 413
33. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readLoop line 414
34. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.skipLabel line 415
35. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.headerLabel line 416
36. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program line 421

    Source documentation

    Ten binary stacks and fixed finite control. Every loop scans one actual bit or tests one actual counter bit; there is no arithmetic oracle in the state.

    def program : Label → TM2.Stmt (fun _ : Tape => Bool) Label (Unit × Option Bool)
      | .copyOut => Reduction.MachineTransfer.loopAt .formula .scratch id false
          .copyOut (some .copyBack)
      | .copyBack => MachineCopy.forkLoop .scratch .formula .work false
          .copyBack (some .headerFirst)
      | .headerFirst => MachineLookup.discard .work .headerFirst .headerSecond
      | .headerSecond => MachineLookup.discard .work .headerSecond .guard
      | .guard => MachineUnaryCounter.guard .index (skipLabel 0) (readStart 0)
      | .skip slot => MachineLookup.discard .work (.skip slot) (skipLabel (slot.val + 1))
      | .read slot =>
          if slot.1.val < 6 then
            if slot.2 then
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.skipLabel, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readStart

37. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.machine line 438
38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.atSkip line 449
39. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.atReadStart line 453
40. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.atReadLoop line 457
41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.atReadDone line 462
42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.discardHeadersTrace line 466

    Source documentation

    The two header fields are physically consumed from the work copy.

    theorem discardHeadersTrace (base : Tape → List Bool) (variableCount clauses : Nat)
        (suffix : List Bool) (hinput : base .work = encodeWords [variableCount, clauses] ++ suffix) :
        (advance (TM2.step program))^[variableCount + clauses + 2]
          (some ⟨some .headerFirst, ((), none), base⟩) =
          some ⟨some .guard, ((), none), Function.update base .work suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program

43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.discardSixTrace line 480

    Source documentation

    The fixed skip body consumes six complete unary fields and returns to the same counter guard, preserving the counter and every other tape.

    theorem discardSixTrace (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 6) (suffix : List Bool)
        (hinput : base .work = encodeWords values ++ suffix) :
        (advance (TM2.step program))^[(encodeWords values).length]
          (some ⟨some (skipLabel 0), ((), none), base⟩) =
          some ⟨some .guard, ((), none), Function.update base .work suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.skipLabel

44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readSixTrace line 491

    Source documentation

    Read the selected six fields using the already checked scanner.

    theorem readSixTrace (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 6) (suffix : List Bool)
        (hinput : base .work = encodeWords values ++ suffix) :
        (advance (TM2.step program))^[(encodeWords values).length + 7]
          (some ⟨some (readStart 0), ((), none), base⟩) =
          some ⟨none, ((), none),
            SourceFieldArray.sequenceTapes .work fieldDestination base 0 values suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readStart, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.fieldDestination

45. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanTapes line 508

    Source documentation

    Normal form for the changing counter and consumed work-copy prefix.

    def scanTapes (base : Tape → List Bool) (index : Nat)
        (indexSuffix input : List Bool) : Tape → List Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape

46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanTapes_work line 512
47. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanTapes_index line 516
48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanTapes_other line 521
49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.update_scanTapes_work line 526
50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.skipClausesTrace line 535

    Source documentation

    Each clause-index bit causes one genuine guard transition and exactly six field-discard loops. The final zero guard enters the field reader.

    theorem skipClausesTrace {n : Nat} (base : Tape → List Bool)
        (prior : List (Target.Clause n)) (indexSuffix suffix : List Bool)
        (register : Option Bool) :
        (advance (TM2.step program))^[(encodeWords (prior.flatMap clauseWords)).length + prior.length + 1]
          (some ⟨some .guard, ((), register), scanTapes base prior.length indexSuffix
            (encodeWords (prior.flatMap clauseWords) ++ suffix)⟩) =
          some ⟨some (readStart 0), ((), none), scanTapes base 0 indexSuffix suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readStart

51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.fieldDestination_eq line 583
52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.fieldDestination_injective_below line 589
53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readSix_output_field line 596

    Source documentation

    Each field stack receives exactly its own unary value, in formula order.

    theorem readSix_output_field (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 6) (suffix : List Bool) (j : Fin 6) :
        SourceFieldArray.sequenceTapes .work fieldDestination base 0 values suffix (.field j) =
          encodeWord (values[j.val]'(by omega)) ++ base (.field j) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.fieldDestination

54. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readSix_output_work line 608
55. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.readSix_output_frame line 616
56. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes line 624
57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanSteps line 630
58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanReadTrace line 637

    Source documentation

    A complete skip-and-read phase after the non-destructive formula copy.

    theorem scanReadTrace {n : Nat} (base : Tape → List Bool) (variableCount declaredClauses : Nat)
        (prior : List (Target.Clause n)) (clause : Target.Clause n)
        (indexSuffix suffix : List Bool) :
        (advance (TM2.step program))^[scanSteps variableCount declaredClauses prior clause]
          (some ⟨some .headerFirst, ((), none), scanTapes base prior.length indexSuffix
            (encodeWords [variableCount, declaredClauses] ++
              (encodeWords (prior.flatMap clauseWords) ++
                (encodeWords (clauseWords clause) ++ suffix)))⟩) =
          some ⟨none, ((), none), outputTapes base clause indexSuffix suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanSteps, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.scanTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes

59. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupSteps line 665
60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupWithSplitTrace line 672

    Source documentation

    Actual formula lookup with a displayed prefix/selected-clause/suffix split. The formula stack is restored before scanning, and the index is consumed down to its retained zero delimiter. Field-stack suffixes are preserved.

    theorem lookupWithSplitTrace (F : Target.Formula) (prior : List (Target.Clause F.variables))
        (clause : Target.Clause F.variables) (after : List (Target.Clause F.variables))
        (hsplit : F.clauses = prior ++ clause :: after)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hformula : base .formula = formulaBits F)
        (hindex : base .index = encodeWord prior.length ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (register : Option Bool) :
        (advance (TM2.step program))^[lookupSteps F prior clause]
          (some ⟨some .copyOut, ((), register), base⟩) =
          some ⟨none, ((), none),
            outputTapes base clause indexSuffix (encodeWords (after.flatMap clauseWords))⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupSteps, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes

61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.output_formula line 703

    Source documentation

    The preserved input copy is exactly the original serialized formula.

    theorem output_formula {n : Nat} (base : Tape → List Bool) (clause : Target.Clause n)
        (indexSuffix suffix : List Bool) :
        outputTapes base clause indexSuffix suffix .formula = base .formula := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes

62. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.output_index line 709
63. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.output_work line 715
64. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.output_field line 721
65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.output_frame line 728
66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.clauseWords_six line 736

    Source documentation

    Explicit variable/sign order consumed by later finite-control phases.

    theorem clauseWords_six {n : Nat} (clause : Target.Clause n) :
        clauseWords clause =
          [clause[0].variableIndex.val, if clause[0].positive then 1 else 0,
           clause[1].variableIndex.val, if clause[1].positive then 1 else 0,
           clause[2].variableIndex.val, if clause[2].positive then 1 else 0] := rfl

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Clause

67. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.fieldWords line 742
68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.output_fieldWords line 746
69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupSteps_le_input line 752
70. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.timePolynomial line 771
71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.timePolynomial_eval line 773
72. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime line 777

    Source documentation

    A polynomial bound on the actual complete copy/skip/read execution.

    def lookupWithSplitInTime (F : Target.Formula) (prior : List (Target.Clause F.variables))
        (clause : Target.Clause F.variables) (after : List (Target.Clause F.variables))
        (hsplit : F.clauses = prior ++ clause :: after)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hformula : base .formula = formulaBits F)
        (hindex : base .index = encodeWord prior.length ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some .copyOut, ((), register), base⟩
          (some ⟨none, ((), none),
            outputTapes base clause indexSuffix (encodeWords (after.flatMap clauseWords))⟩)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes

73. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.lookupInTime line 800

    Source documentation

    Lookup at a valid numbered clause, starting with its ordinary unary index. The output fields are those of F.clauses[i], with the rest of the work copy and the original formula retained exactly as stated by the frame lemmas.

    def lookupInTime (F : Target.Formula) (i : Fin F.clauses.length)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hformula : base .formula = formulaBits F)
        (hindex : base .index = encodeWord i.val ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some .copyOut, ((), register), base⟩
          (some ⟨none, ((), none), outputTapes base F.clauses[i.val] indexSuffix
            (encodeWords ((F.clauses.drop (i.val + 1)).flatMap clauseWords))⟩)
          (timePolynomial.eval (formulaBits F).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes

74. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.machineInTime line 820

    Source documentation

    The same proved run stated directly for the concrete finite machine.

    def machineInTime (F : Target.Formula) (i : Fin F.clauses.length)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hformula : base .formula = formulaBits F)
        (hindex : base .index = encodeWord i.val ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (register : Option Bool) :
        StateTransition.EvalsToInTime machine.step
          ⟨some .copyOut, ((), register), base⟩
          (some ⟨none, ((), none), outputTapes base F.clauses[i.val] indexSuffix
            (encodeWords ((F.clauses.drop (i.val + 1)).flatMap clauseWords))⟩)
          (timePolynomial.eval (formulaBits F).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceClauseLookup.outputTapes