OAI/Computability/UniqueGames/PCP/InputLemmas.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Serialization boundaries and direct row lookup for the shared executable fixed-alphabet graph codec. The alphabet is a fixed parameter. Rows remain in their stored order, including repeated darts and loops. Word offsets are fixed; bit offsets are represented by actual encoded prefixes because unary fields have data-dependent lengths. These are data identities, not runtime certificates.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowWidth line 46
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowOffset line 49

    Source documentation

    Offset measured in natural-word fields, including the two header fields.

    def rowOffset (q e : Nat) : Nat := 2 + rowWidth q * e

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowWidth

  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowsWords_split line 52

    Source documentation

    Exact decomposition before, at, and after a selected stored row.

    theorem rowsWords_split (rows : List (DartRow q n m)) (e : Nat)
    (he : e < rows.length) :
    rows.flatMap rowWords = (rows.take e).flatMap rowWords ++
      (rowWords rows[e] ++ (rows.drop (e + 1)).flatMap rowWords) := by
…
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowsBits_split line 63

    Source documentation

    The unary serialization keeps exactly the same row boundaries, with separate encoded prefixes rather than an assumed constant bit offset.

    theorem rowsBits_split (rows : List (DartRow q n m)) (e : Nat)
    (he : e < rows.length) :
    encodeWords (rows.flatMap rowWords) =
      encodeWords ((rows.take e).flatMap rowWords) ++
        (encodeWords (rowWords rows[e]) ++
          encodeWords ((rows.drop (e + 1)).flatMap rowWords)) := by
…
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowsBits_append_split line 73

    Source documentation

    A selected row can be followed by an arbitrary caller-owned suffix.

    theorem rowsBits_append_split (rows : List (DartRow q n m)) (e : Nat)
    (he : e < rows.length) (suffix : List Bool) :
    encodeWords (rows.flatMap rowWords) ++ suffix =
      encodeWords ((rows.take e).flatMap rowWords) ++
        (encodeWords (rowWords rows[e]) ++
          (encodeWords ((rows.drop (e + 1)).flatMap rowWords) ++ suffix)) := by
…
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.prefixWords line 82
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.suffixWords line 85
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.prefixWords_length line 88
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_at_row line 93
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableBits_at_row line 102
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableBits_header line 109

    Source documentation

    Removing precisely the two encoded header words exposes the stored rows.

    theorem tableBits_header (table : Table q) :
    tableBits table = encodeWord table.vertices ++
      (encodeWord table.darts ++ encodeWords ((rowList table).flatMap rowWords)) := by
…
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_drop_row line 114
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_take_row line 121
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_get_tail line 127
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_get_reverse line 132
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_drop_relation line 137
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.relationWords_get line 143
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_get_relation line 148
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.tableWords_get_predicate line 158
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.rowOffset_lt_length line 165
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Input.relationOffset_lt_length line 173
  22. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet line 204
  23. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.State line 205
  24. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.relationEquiv line 208

    Source documentation

    The relation register is a finite tuple of bits, with no unbounded storage.

    def relationEquiv (q : Nat) : RelationTable q ≃ (Fin (q * q) → Bool) where
…
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.relationFintype line 215

    Source documentation

    Executable enumeration used when assembling the finite machine state.

    @[instance_reducible] def relationFintype (q : Nat) : Fintype (RelationTable q) :=
…
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.stateFintype line 218
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.readSlot line 224

    Source documentation

    Read one encoded Boolean into a fixed slot of the finite relation register.

    def readSlot (source : K) (i : Fin (q * q))
    (next : TM2.Stmt (Alphabet (K := K)) Λ (State σ q)) :
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.State

  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlot line 234
  29. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.readSlots line 244
  30. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords line 250
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots line 253
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_preserves_correct line 259
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_mem line 271
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_finRange line 284
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords_finRange line 291
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlots line 304

    Source documentation

    Each stored register bit is obtained from its actual serialized field.

    theorem stepAux_readSlots (source : K) (indices : List (Fin (q * q)))
    (relation : RelationTable q)
    (next : TM2.Stmt (Alphabet (K := K)) Λ (State σ q))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.State

  37. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.readRelation line 321

    Source documentation

    Fixed finite program fragment; it can be inserted before any continuation.

    def readRelation (source : K)
    (next : TM2.Stmt (Alphabet (K := K)) Λ (State σ q)) :
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.State

  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation line 326
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation_fromTapes line 337
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.readSlots_pushBound line 351
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.readRelation_pushBound line 361
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.parser line 367
  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.parser_pushBound line 372
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.parserStep line 377
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.parserTrace line 392

    Source documentation

    One transition executes the fixed chain of q*q slot readers.

    theorem parserTrace (source : K) (readLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ q))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.State

  46. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.parserInTime line 404
  47. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.encodingPolynomial line 437
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.encodingPolynomial_eval line 440
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.encodingPolynomial_mono line 444
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.rowBound_le_polynomial line 450
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.generic_size_add_two_le_bits line 460
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.generic_bits_le_polynomial line 466
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.generic_bits_le_of_size_le line 472
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.size_add_two_le_bits line 477
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.bits_le_polynomial line 483
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTableComplexity.bits_le_of_size_le line 489
  57. def OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.bitCount line 507
  58. def OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean line 510
  59. def OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.splitTape line 513
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.bitCount_succ line 521
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_congr line 525
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_const line 530
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_add line 533
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_sub line 537
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_mul line 541
  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_zero line 545
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.expect_bool line 548
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_succ line 552
  69. def OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.score line 563
  70. def OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.scoreMean line 565
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.scoreMean_zero line 568
  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.scoreMean_succ line 571
  73. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.score_identity line 591

    Source documentation

    Exact finite integration by parts for the fair Boolean-tape law.

    theorem score_identity (n : ℕ) (g : ℕ → ℝ) :
    scoreMean (n + 1) g = ((n : ℝ) + 1) / 2 *
      (binomialMean n g - binomialMean n (fun k => g (k + 1))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.scoreMean, OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean

  74. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.score_mean_zero line 601
  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.score_second_moment line 609

    Source documentation

    The score variance is proved from the actual tape distribution.

    theorem score_second_moment (n : ℕ) :
    binomialMean n (fun k => score n k ^ 2) = (n : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean, OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.score

  76. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.score_difference line 628
  77. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 636

    Source documentation

    Cauchy--Schwarz yields an adjacent-length bound without any support or small-parameter caveat. The square form avoids introducing square roots.

    theorem adjacent_difference_sq (n : ℕ) (g : ℕ → ℝ)
    (hg : ∀ k, 0 ≤ g k ∧ g k ≤ 1) :
    4 * ((n : ℝ) + 1) *
      (binomialMean n g - binomialMean (n + 1) g) ^ 2 ≤ 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean

  78. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.adjacent_difference_le line 670
  79. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_shift_le line 683
  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 702
  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.mean_window_le line 708
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.square_window_le line 731

    Source documentation

    A convenient square center for a fixed alphabet.

    theorem square_window_le (q M m : ℕ) (hq : 1 ≤ q) (hM : 1 ≤ M)
    (hlo : (4 * q * M) ^ 2 - M ≤ m) (hhi : m ≤ (4 * q * M) ^ 2 + M)
    (g : ℕ → ℝ) (hg : ∀ k, 0 ≤ g k ∧ g k ≤ 1) :
    |binomialMean m g - binomialMean ((4 * q * M) ^ 2) g| ≤ 1 / (4 * (q : ℝ)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean

  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.modal_transfer line 759

    Source documentation

    A modal event of probability at least 1/q retains probability 1/(2q) throughout the middle window used in lazy-walk powering.

    theorem modal_transfer (q M m : ℕ) (hq : 1 ≤ q) (hM : 1 ≤ M)
    (hlo : (4 * q * M) ^ 2 - M ≤ m) (hhi : m ≤ (4 * q * M) ^ 2 + M)
    (g : ℕ → ℝ) (hg : ∀ k, 0 ≤ g k ∧ g k ≤ 1)
    (hmodal : 1 / (q : ℝ) ≤ binomialMean ((4 * q * M) ^ 2) g) :
    1 / (2 * (q : ℝ)) ≤ binomialMean m g := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.LazySmoothing.binomialMean