OAI/Computability/MaxCut/PCP/FieldArray.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.finish line 13
2. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.finishStep line 17
3. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes line 28

   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.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination

4. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTrace line 38

   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.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.loopLabel, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.program

5. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceInTime line 97
6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequence_time_eq_length line 119
7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_other line 124
8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_source line 139
9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_selected line 155

   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.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes

10. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.boundedIndex line 204

    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.MaxCutGames.Foundations.Hastad.SourceFieldArray.boundedIndex_val line 206
12. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination line 209
13. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.startLabel line 210
14. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.loopLabel line 211
15. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination_ne_source line 213
16. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination_injective_below line 221
17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination_eq_succ line 228
18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.output_source line 232
19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.output_field line 240
20. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.program line 254

    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.MaxCutGames.Foundations.Hastad.SourceFieldArray.machine line 263
22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.atStart line 274
23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.atLoop line 278
24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.atDone line 283
25. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.machineInTime line 286
26. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound line 316

    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.MaxCutGames.Foundations.Hastad.SourceFieldArray.machine, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.startLabel, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination

27. def OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sixFieldsInTime line 331

    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.MaxCutGames.Foundations.Hastad.SourceFieldArray.machine, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.startLabel, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.destination

28. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.discardFieldsTrace line 357

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program

29. inductive OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape line 400
30. inductive OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Label line 404
31. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination line 410
32. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readStart line 411
33. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readLoop line 412
34. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.skipLabel line 413
35. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.headerLabel line 414
36. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program line 419

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Label, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.skipLabel, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readStart

37. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.machine line 436
38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.atSkip line 447
39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.atReadStart line 451
40. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.atReadLoop line 455
41. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.atReadDone line 460
42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.discardHeadersTrace line 464

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program

43. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.discardSixTrace line 478

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.skipLabel

44. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readSixTrace line 489

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readStart, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination

45. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanTapes line 506

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape

46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanTapes_work line 510
47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanTapes_index line 514
48. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanTapes_other line 519
49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.update_scanTapes_work line 524
50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.skipClausesTrace line 533

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanTapes, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readStart

51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_eq line 581
52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_injective_below line 587
53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readSix_output_field line 594

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceFieldArray.sequenceTapes, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.fieldDestination

54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readSix_output_work line 606
55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.readSix_output_frame line 614
56. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes line 622
57. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanSteps line 628
58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanReadTrace line 635

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanSteps, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.scanTapes, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes

59. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupSteps line 663
60. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitTrace line 670

    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.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupSteps, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes

61. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.output_formula line 701

    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.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes

62. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.output_index line 707
63. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.output_work line 713
64. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.output_field line 719
65. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.output_frame line 726
66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.clauseWords_six line 734

    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.MaxCutGames.Foundations.Target.Clause

67. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.fieldWords line 740
68. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.output_fieldWords line 744
69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupSteps_le_input line 750
70. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.timePolynomial line 769
71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.timePolynomial_eval line 771
72. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime line 775

    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.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes

73. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.lookupInTime line 798

    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.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.program, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes

74. def OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.machineInTime line 818

    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.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceClauseLookup.outputTapes