OAI/Computability/UniqueGames/PCP/PreprocessingRegularTablesLemmas.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Executable degree replacement on the actual finite constraint rows

Vertices are numbered by first listing the original darts, then the dummy darts in original-vertex order. Each local cloud uses its explicit filtered dart list. Internal ports carry equality; the final port retains the original constraint, or an always-accepting loop at a dummy dart. The constructor is total, including inputs with no darts. The fixed base expander is supplied once; every input-dependent operation is an explicit finite calculation.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.paddingList line 25

    Source documentation

    Dummy coordinates, in increasing original vertex and local index order.

    def paddingList {n : Nat} (padding : Fin n → Nat) :
    List (Σ v : Fin n, Fin (padding v)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding

  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 29
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 33
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 38
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 43
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 49

    Source documentation

    Explicit list search/get indexing, with an erased cardinality cast.

    def paddingOrder {n : Nat} (padding : Fin n → Nat) :
    (Σ v : Fin n, Fin (padding v)) ≃ Fin (∑ v, padding v) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding

  7. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.Vertex line 53
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount line 56
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 60

    Source documentation

    The original darts precede all the newly added dummy darts.

    def vertexOrder (t : GraphTables.Table) (padding : Fin t.vertices → Nat) :
    Vertex t padding ≃ Fin (vertexCount t padding) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount

  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 64
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 68
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.unitOrder line 73
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.portOrder line 80

    Source documentation

    Internal cloud ports precede the one inherited-constraint port.

    def portOrder (q : Nat) : (Fin q ⊕ Unit) ≃ Fin (q + 1) :=
…
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 83
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 86
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 90

    Source documentation

    A supplied finite cloud rotation is transported by the explicit cloud list.

    def cloudGraphs (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    {q : Nat} (tables : ∀ v, ExpanderTables.Table
      (PreprocessingCloudIndex.cloudSize t v + padding v) q) (v : Fin t.vertices) :
    PortGraph (Cloud (paddedGraph (GraphTables.semantics t)
      (fun w => Fin (padding w))) v) (Fin q) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics

  17. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 98
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 105
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 113
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 120
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 128
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 142

    Source documentation

    Materialize every reverse index and every 4096-bit constraint row.

    def ofCloudTables (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    {q : Nat} (tables : ∀ v, ExpanderTables.Table
      (PreprocessingCloudIndex.cloudSize t v + padding v) q) :
    PortTables.Table (vertexCount t padding) (q + 1) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount

  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 149
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 161
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 172
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.accepts_original line 182
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 193
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 203
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 221

    Source documentation

    Numbering preserves the rejection count for every labeling.

    theorem rejectionCount_ofCloudTables (t : GraphTables.Table)
    (padding : Fin t.vertices → Nat) {q : Nat}
    (tables : ∀ v, ExpanderTables.Table
      (PreprocessingCloudIndex.cloudSize t v + padding v) q)
    (labels : Fin (vertexCount t padding) → GraphTables.Label) :
    (PortTables.baseGraph (ofCloudTables t padding tables)).rejectionCount labels =
      (sourceGraph t padding tables).rejectionCount
        (fun z => labels (vertexOrder t padding z)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.ofCloudTables, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.sourceGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexOrder

  30. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 237
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 243
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.emptyTable line 257

    Source documentation

    An empty cloud has a total, vacuous rotation table.

    def emptyTable (q : Nat) : ExpanderTables.Table 0 q :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table

  33. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.resizeTable line 261

    Source documentation

    Change only a proof-equal size index, without selecting any new numbering.

    def resizeTable {n m q : Nat} (h : n = m) (table : ExpanderTables.Table n q) :
    ExpanderTables.Table m q := h ▸ table

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table

  34. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.BaseTable line 264
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.internalDegree line 268
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding line 270
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 274
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 279
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 286
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 292
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 299

    Source documentation

    Select the family level by the bounded multiplication search.

    def familyCloudTable (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices) :
    ExpanderTables.Table (PreprocessingCloudIndex.cloudSize t v + padding t v)
      internalDegree :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.internalDegree

  42. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.regularize line 313

    Source documentation

    The actual regularized output rows; no runtime proof or positivity input.

    def regularize (H : BaseTable) (t : GraphTables.Table) :
    PortTables.Table (vertexCount t (padding t)) (internalDegree + 1) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.padding, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.internalDegree

  43. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 317
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.rotationWords_resizeTable line 338

    Source documentation

    Transporting only the size equality leaves every serialized rotor entry unchanged; no relabeling or alternative numbering is introduced.

    theorem rotationWords_resizeTable {n m q : Nat} (h : n = m)
    (table : ExpanderTables.Table n q) :
    rotationWords (resizeTable h table) = rotationWords table := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table

  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.familyRotor_eq_familyCloudTable line 347

    Source documentation

    This left side is definitionally the output MachineRegularFamily.rotor for the request on its physical core tape 4. The right side is exactly the archive expected on core tape 7 by the internal-row machine.

    theorem familyRotor_eq_familyCloudTable (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (hk : 0 < cloudSize t v) :
    encodeWords (rotationWords (ExpanderTables.family H
      (PreprocessingLevels.boundedLevel (cloudSize t v)))) =
      encodeWords (rotationWords (familyCloudTable H t v)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.family, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel

  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_dart line 358

    Source documentation

    An actual original dart supplies a member of its owner's cloud.

    theorem cloudSize_pos_of_dart (t : GraphTables.Table) (e : Fin t.darts) :
    0 < cloudSize t t.rows[e].tail := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table

  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.padding_zero_of_cloudSize_zero line 364

    Source documentation

    An empty cloud has no padding vertices either.

    theorem padding_zero_of_cloudSize_zero (t : GraphTables.Table) (v : Fin t.vertices)
    (hk : cloudSize t v = 0) : padding t v = 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table

  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_dummy line 369

    Source documentation

    Every actual dummy vertex also belongs to a positive original cloud.

    theorem cloudSize_pos_of_dummy (t : GraphTables.Table) (v : Fin t.vertices)
    (j : Fin (padding t v)) : 0 < cloudSize t v := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table

  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_paddedCloud line 378

    Source documentation

    The same positivity fact for the common local coordinate interface.

    theorem cloudSize_pos_of_paddedCloud (t : GraphTables.Table) (v : Fin t.vertices)
    (x : PaddedCloud t (padding t) v) : 0 < cloudSize t v := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table

  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFamilyBridge.familyCloudWords_of_zero line 388

    Source documentation

    The zero-cloud branch remains genuinely empty, including its serialized rotor archive. It is not replaced by the geometric family at request zero.

    theorem familyCloudWords_of_zero (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (hk : cloudSize t v = 0) :
    encodeWords (rotationWords (familyCloudTable H t v)) = [] := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table