PreprocessingPaddingTables.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Executable whole-vertex padding of regular constraint tables

The first n vertex rows retain their old rotation and complete relation tables. Every additional vertex has one self-reversing, always-accepting loop at each port. An explicit finite sum equivalence identifies these stored rows with VertexPadding.pad; rejection counts are preserved for every labeling.

The construction materializes finite vectors. No machine runtime bound is claimed here.

def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 27
Source documentation
Old vertices occupy the initial interval and dummy vertices the final one.
```
def vertexEquiv (h : n ≤ m) : Fin n ⊕ Fin (m - n) ≃ Fin m :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 30
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 33
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 36
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 41
Source documentation
The port number is retained by the coordinate conversion.
```
def dartEquiv (h : n ≤ m) :
    (Fin n ⊕ Fin (m - n)) × Fin d ≃ Fin m × Fin d :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 45
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 50
Source documentation
Concrete sum-type padding, before converting to integer vertex indices.
```
def sumGraph (table : Table n d) (m : Nat) :
    ConstraintGraph (Fin n ⊕ Fin (m - n))
      ((Fin n ⊕ Fin (m - n)) × Fin d) Label :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 56
Source documentation
The same graph, with the explicit initial/final-interval vertex ordering.
```
def paddedGraph (table : Table n d) (h : n ≤ m) :
    ConstraintGraph (Fin m) (Fin m × Fin d) Label where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 73
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 81
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad line 89
Source documentation
Executable materialization of every padded rotation and predicate row.
```
def pad (table : Table n d) (h : n ≤ m) : Table m d :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 95
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 99
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 105
Source documentation
These are the actual finite table validity laws, not additional premises.
```
theorem pad_valid (table : Table n d) (h : n ≤ m) :
    Function.Involutive (rotation (pad table h)) ∧
      ∀ e a b, PortTables.accepts (pad table h) (rotation (pad table h) e) b a =
        PortTables.accepts (pad table h) e a b :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext line 111
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 126
Source documentation
Full semantic identity with the concrete padding and explicit reindexing.
```
@[simp] theorem baseGraph_pad (table : Table n d) (h : n ≤ m) :
    baseGraph (pad table h) = paddedGraph table h := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.paddedGraph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 134
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 142
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 149
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 156
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 163
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 169
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 175
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.relation_ext line 181
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 191
Source documentation
The entire old 4096-bit relation row is retained.
```
theorem relations_pad_old (table : Table n d) (h : n ≤ m)
    (v : Fin n) (p : Fin d) :
    (pad table h).relations[rowIndex m d (v.castLE h, p)] =
      table.relations[rowIndex n d (v, p)] := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 200
Source documentation
Every bit of every added relation row accepts.
```
theorem relations_pad_new (table : Table n d) (h : n ≤ m)
    (v : Fin (m - n)) (p : Fin d) :
    (pad table h).relations[rowIndex m d (vertexEquiv h (Sum.inr v), p)] =
      Vector.replicate 4096 true := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 211
Source documentation
Pointwise satisfaction commutes with the explicit sum-coordinate map.
```
theorem paddedGraph_edgeSatisfied_equiv (table : Table n d) (h : n ≤ m)
    (labeling : Fin m → Label) (e : (Fin n ⊕ Fin (m - n)) × Fin d) :
    (paddedGraph table h).edgeSatisfied labeling (dartEquiv h e) =
      (sumGraph table m).edgeSatisfied (fun v => labeling (vertexEquiv h v)) e := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.paddedGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.sumGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 224
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 231
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 239
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 246
Source documentation
Exact occurrence counts for arbitrary labels on all old and added vertices.
```
theorem pad_rejectionCount (table : Table n d) (h : n ≤ m)
    (labeling : Fin m → Label) :
    (baseGraph (pad table h)).rejectionCount labeling =
      (baseGraph table).rejectionCount (fun v => labeling (v.castLE h)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 265
Source documentation
A particular padded labeling satisfies exactly when its old restriction does.
```
theorem pad_labeling_satisfies_iff (table : Table n d) (h : n ≤ m)
    (labeling : Fin m → Label) :
    (∀ e, (baseGraph (pad table h)).edgeSatisfied labeling e = true) ↔
      ∀ e, (baseGraph table).edgeSatisfied (fun v => labeling (v.castLE h)) e = true := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 281
Source documentation
A computable extension uses label zero on every dummy vertex.
```
def extendLabeling (h : n ≤ m) (labeling : Fin n → Label) : Fin m → Label :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 284
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 288