OAI/Computability/UniqueGames/PCP/PreprocessingRegularLoopWordsLemmas.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Prefix and suffix invariants for regular-table row loops

These finite block identities apply to original-vertex blocks, to dummy blocks within an owner, and to whole owner blocks. They expose exactly the next emitted block while preserving the codec's established order.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix line 26

    Source documentation

    Bits emitted by the first k blocks.

    def blocksPrefix {n : Nat} (f : Fin n → List Bool) (k : Nat) : List Bool :=
…
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix line 30

    Source documentation

    Bits remaining after the first k blocks.

    def blocksSuffix {n : Nat} (f : Fin n → List Bool) (k : Nat) : List Bool :=
…
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_zero line 33
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_all line 37
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_succ line 43
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_zero line 51
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_all line 55
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_succ line 61
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_append_suffix line 69

    Source documentation

    The completed and remaining portions partition the original bitstream.

    theorem blocksPrefix_append_suffix {n : Nat} (f : Fin n → List Bool) (k : Nat) :
    blocksPrefix f k ++ blocksSuffix f k = (List.ofFn f).flatten := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix

  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.offset_succ line 89
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.blocksPrefix_length_le line 97
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.header line 103
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.ownerBits line 106
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.originalPrefix line 111
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix line 116
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix line 122
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.originalPrefix_length_le line 130
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix_length_le line 138
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix_length_le line 149
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.regular_originalPrefix_le line 163
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.regular_ownerPrefix_le line 170
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.regular_dummyPrefix_le line 177
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.visits_le_input line 186

    Source documentation

    The number of original and dummy vertex visits is exactly the constructed vertex count; adding owner visits still gives a linear bound in input bits.

    theorem visits_le_input :
    t.darts + t.vertices + (∑ v, padding t v) + 1 ≤
      (ExpanderFamily.growth + 1) * PreprocessingMachineBounds.inputLength t + 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.inputLength

  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularBounds.sum_body_costs_le line 198

    Source documentation

    An elementary budget aggregation for the actual three finite loops. The per-call bounds must be supplied from the separately checked subprogram runs.

    theorem sum_body_costs_le (old : Fin t.darts → Nat) (owners : Fin t.vertices → Nat)
    (dummy : ∀ v : Fin t.vertices, Fin (padding t v) → Nat) (setup cap : Nat)
    (hs : setup ≤ cap) (ho : ∀ e, old e ≤ cap) (hv : ∀ v, owners v ≤ cap)
    (hd : ∀ v j, dummy v j ≤ cap) :
    setup + (∑ e, old e) + (∑ v, owners v) + (∑ v, ∑ j, dummy v j) ≤
      ((ExpanderFamily.growth + 1) * PreprocessingMachineBounds.inputLength t + 1) * cap := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.inputLength

  25. inductive OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.Tape line 231
  26. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.Signs line 236
  27. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.State line 237
  28. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.Alphabet line 238
  29. inductive OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.CopyPhase line 240
  30. inductive OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.Label line 248
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.initialState line 262
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.stateKeys line 264
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.stateKeys_complete line 269
  34. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.nameField line 275
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.copySource line 277
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.copyScale line 282
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.copyNext line 286
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.relationNext line 295
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.finalTape line 301
  40. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.drain line 304
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.headerTape line 307
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.relationOutput line 309
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.program line 313
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineModel.machine line 363