OAI/Computability/MaxCut/PCP/LoopOrder.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple line 14

    Source documentation

    Interpret a radix tuple using the declared domain and codomain numbering.

    def decodeTuple {α β : Type} (a : Encoding α) (b : Encoding β)
    (digits : Fin a.size → Fin b.size) : α → β :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding

  2. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_function line 20

    Source documentation

    Increasing function rank is exactly the controller's tuple order, followed by the explicit coordinate decoder. This includes empty domains and codomains.

    theorem enumerate_function {α β : Type} (a : Encoding α) (b : Encoding β) :
    (a.function b).enumerate =
      (tupleOrder b.size a.size).map (decodeTuple a b) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple

  3. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_fin_function line 26
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.tupleTapeOrder line 38
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_eq_tupleTapeOrder line 46
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_flatMap_tupleTapeOrder line 53
  7. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.rankedQuery line 61

    Source documentation

    Total extension of the declared tape decoder, for the query loop's natural index register. Out-of-range values are never visited by that loop.

    def rankedQuery (u D : ℕ) (fallback : SourceQueryLoop.Query u D)
    (i : ℕ) : SourceQueryLoop.Query u D :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.Query

  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.rankedQuery_at line 67
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_ofFn line 72
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_enumerate line 87
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_tupleTapeOrder line 101
  12. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder line 112

    Source documentation

    Clause, slot, left-query, noise, right-query loops, from outermost to innermost. Within each tuple loop coordinate zero changes fastest.

    def tupleSourceOrder (F : Formula) (u D : ℕ) : List (SourceIndex F u D) :=
…
  13. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.sourceIndexEncoding_eq_tupleSourceOrder line 118
  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.rawSourceList_eq_tupleOrder line 137

    Source documentation

    Equality of ordered equation lists preserves every repeated occurrence.

    theorem rawSourceList_eq_tupleOrder (F : Formula) (u D : ℕ) :
    rawSourceList F u D = (tupleSourceOrder F u D).map (sourceEquation F u D) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder

  15. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.sourceList_eq_tupleOrder line 142
  16. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.rawSourceList_flatMap_tupleOrder line 146
  17. def OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.reverseAppend line 154

    Source documentation

    The stack update performed by one record append.

    def reverseAppend {α β : Type} (encode : α → List β)
    (accumulator : List β) (record : α) : List β :=
…
  18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend line 160

    Source documentation

    After any ascending prefix, the accumulator is its reversed encoding followed by the original accumulator.

    theorem foldl_reverseAppend {α β : Type} (encode : α → List β)
    (records : List α) (accumulator : List β) :
    records.foldl (reverseAppend encode) accumulator =
      (records.flatMap encode).reverse ++ accumulator := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.reverseAppend

  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_header line 170
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_prefix line 178

    Source documentation

    The prefix invariant is stated without requiring that the prefix end on the last record. A later suffix continues from exactly this accumulator.

    theorem foldl_reverseAppend_prefix {α β : Type} (encode : α → List β)
    (emitted remaining : List α) (header : List β) :
    (emitted ++ remaining).foldl (reverseAppend encode) header.reverse =
      remaining.foldl (reverseAppend encode)
        (header ++ emitted.flatMap encode).reverse := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.reverseAppend

  21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.foldl_resultTapes line 187

    Source documentation

    The actual tape update used by SourceTestAppend has this same invariant; all other tapes remain the original tapes.

    theorem foldl_resultTapes {α K : Type} [DecidableEq K]
    (layout : SourceTestAppend.Layout K) (encode : α → List Bool)
    (records : List α) (base : K → List Bool) :
    records.foldl (fun tapes record =>
        SourceTestAppend.resultTapes layout tapes (encode record)) base =
      Function.update base layout.accumulator
        ((records.flatMap encode).reverse ++ base layout.accumulator) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes

  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.inputBits_eq_header_records line 205
  23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.input_reverse_accumulator line 217
  24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.sourceInput_tuple_reverse_accumulator line 227

    Source documentation

    The nonempty-formula branch can feed the accumulator directly from the tuple controller's occurrence order. The total-input invariant above also covers the separate singleton empty-formula branch.

    theorem sourceInput_tuple_reverse_accumulator (F : Formula) (u D : ℕ)
    (hD : 0 < D) (hne : F.clauses ≠ []) :
    (tupleSourceOrder F u D).foldl
        (reverseAppend (fun p => encodeWords
          (SourceEncoding.equationWords (sourceEquation F u D p))))
        (encodeWords [nBits F u, (sourceList F u D).length]).reverse =
      (SourceEncoding.inputBits (sourceInput F u D hD)).reverse := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder, OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.reverseAppend

  25. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.finalReverse_steps line 244

    Source documentation

    Applying the existing reversal machine to the accumulated records returns the exact serialized input in inputBits.length + 1 transitions. This is only the final reversal stage, not a bound for generating the records.

    theorem finalReverse_steps (input : SourceEncoding.Input) (register : Option Bool) :
    MachineReverse.next^[(SourceEncoding.inputBits input).length + 1]
      (some (MachineReverse.running
        (input.equations.foldl
          (reverseAppend (fun e => encodeWords (SourceEncoding.equationWords e)))
          (encodeWords [input.«variables», input.equations.length]).reverse)
        [] register)) =
      some (MachineReverse.halted (SourceEncoding.inputBits input)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLoopOrder.reverseAppend

  26. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.Tape line 265
  27. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.currentAt line 269
  28. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.remainingAt line 272
  29. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits line 277

    Source documentation

    Set the active low coordinates; higher digits and every other tape retain their original contents. Unary digit stacks have no unread suffix.

    def setDigits (m : ℕ) {q : ℕ} (digits : Fin q → ℕ)
    (base : Tape u Extra → List Bool) : Tape u Extra → List Bool
  | .current i => if h : i.val < q then encodeWord (digits ⟨i.val, h⟩)
      else base (.current i)
  | .remaining i => if h : i.val < q then encodeWord (m - 1 - digits ⟨i.val, h⟩)
      else base (.remaining i)
  | k => base k

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.Tape

  30. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc line 285
  31. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit line 288
  32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_zero line 292
  33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_extra line 298
  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_self line 302
  35. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_setAcc line 306
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_apply line 310
  37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_setAcc line 313
  38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit_extra line 319
  39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit_setAcc line 323
  40. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_putDigit line 331

    Source documentation

    The low-coordinate assignment commutes with a separate higher digit.

    theorem setDigits_putDigit (m q : ℕ) (hq : q < u) (digits : Fin q → ℕ)
    (base : Tape u Extra → List Bool) (d r : ℕ) :
    setDigits m digits (putDigit ⟨q, hq⟩ base d r) =
      putDigit ⟨q, hq⟩ (setDigits m digits base) d r := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit

  41. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc line 352

    Source documentation

    The last coordinate is the outside loop coordinate.

    theorem setDigits_snoc (m q : ℕ) (hq : q < u) (digits : Fin q → ℕ)
    (d : ℕ) (base : Tape u Extra → List Bool) :
    setDigits m (Fin.snoc digits d) base =
      putDigit ⟨q, hq⟩ (setDigits m digits base) d (m - 1 - d) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit

  42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc_base line 388
  43. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.allBits line 394
  44. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix line 397
  45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_eq_ofFn line 401
  46. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.blocks line 410
  47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_all line 413
  48. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.configuration line 420
  49. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.BodyTrace line 423
  50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.val_snoc line 434
  51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.zeros_snoc line 440
  52. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.initialConfiguration line 445
  53. def OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.finalConfiguration line 449
  54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.exists_schedule line 455
  55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.traversalInTime line 589

    Source documentation

    The time bound is derived from the concrete schedule, not from the number of tuples alone. Dimension zero consists of its single actual body trace.

    theorem traversalInTime
    (program : Λ → TM2.Stmt (fun _ : Tape u Extra => Bool) Λ (σ × Option Bool))
    (bodyLabel : Λ) (next resetLabel : ℕ → Λ) (canonical : σ) (accumulator : Extra)
    (positive : 0 < m) (B : ℕ) (base : Tape u Extra → List Bool)
    (bits : (Fin u → Fin m) → List Bool)
    (atCheck : ∀ i, i < u → program (next i) =
      increment (currentAt accumulator i) (remainingAt accumulator i) bodyLabel (resetLabel i))
    (atReset : ∀ i, i < u → program (resetLabel i) =
      reset (currentAt accumulator i) (remainingAt accumulator i) (resetLabel i) (next (i + 1)))
    (bodies : BodyTrace program bodyLabel (next 0) canonical accumulator base bits B) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step program)
      (initialConfiguration (m := m) u bodyLabel canonical base)
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.currentAt, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.remainingAt, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.BodyTrace, OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.initialConfiguration

  56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.initial_current line 611
  57. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.initial_remaining line 617
  58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.final_current line 622
  59. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.final_remaining line 628
  60. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOdometerSchedule.final_accumulator line 634