SubdivisionTarget.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Concrete numbered, full-table output for the four-edge subdivision. Original vertices keep their names. The new names are n+e, n+Q+2e, and n+Q+2e+1, and each input occurrence emits four consecutive rows.

def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance line 19
Source documentation
Retain every original list occurrence as its own edge identifier.
```
def ofInstance {q : Nat} (H : Instance q) :
    OccurrenceGame (Fin H.vertices) (Fin H.constraints.length) (Fin q) where
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance_count line 25
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance_maxSatisfied line 35
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance_value line 45
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericRightEquiv line 52
Source documentation
Number p_e by 2e and r_e by 2e+1.
```
def numericRightEquiv (Q : Nat) : Fin Q × Bool ≃ Fin (Q * 2) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericRightEquiv_false_val line 55
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericRightEquiv_true_val line 60
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv line 66
Source documentation
Original vertices, middle vertices, then interleaved p_e,r_e.
```
def numericVertexEquiv (n Q : Nat) :
    (Fin n ⊕ Fin Q) ⊕ (Fin Q × Bool) ≃ Fin (n + 3 * Q) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv_original_val line 74
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv_middle_val line 77
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv_p_val line 80
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv_r_val line 85
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericEdgeEquiv line 91
Source documentation
The occurrence e occupies output indices 4e,4e+1,4e+2,4e+3.
```
def numericEdgeEquiv (Q : Nat) : Fin (4 * Q) ≃ Fin Q × Fin 4 :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericEdgeEquiv_symm_val line 94
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.tables line 99
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.tables_correspond line 104
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.vertexFields line 113
Source documentation
The five physical fields consumed by the checked row-emission phase.
```
def vertexFields {q : Nat} (H : Instance q) (e : Fin H.constraints.length) :
    Fin 5 → Fin (H.vertices + 3 * H.constraints.length) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.vertexFields_val line 121
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.rows_eq line 130
Source documentation
Four consecutive semantic rows are exactly the four full-table rows emitted by the machine phase, including the inverse table in the final row.
```
theorem rows_eq {q : Nat} (H : Instance q) (e : Fin H.constraints.length) :
    List.ofFn (fun i : Fin 4 => ProductTarget.row (Subdivision.game (ofInstance H))
      (numericVertexEquiv H.vertices H.constraints.length)
      (numericEdgeEquiv H.constraints.length) (tables H)
      ((numericEdgeEquiv H.constraints.length).symm (e, i))) =
    MachineSubdivisionRows.rows (vertexFields H e) H.constraints[e].permutation := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.ProductTarget.row, OAI.UniqueGamesTheorem.Explicit.Subdivision.game, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericEdgeEquiv, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.tables, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.rows, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.vertexFields
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.tables_translation line 139
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide line 159
Source documentation
A deterministic full-table occurrence list with exactly four rows per input row.
```
def subdivide {q : Nat} (H : Instance q) : Instance q :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide_vertices line 165
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide_length line 168
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide_translation line 172
def OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.simpleBipartite line 181
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numeric_side line 184
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.simpleBipartite_side line 204
Source documentation
The concrete left side is precisely the first n+Q numeric names.
```
theorem simpleBipartite_side {q : Nat} (H : Instance q) (v : Fin (subdivide H).vertices) :
    (simpleBipartite H).side v = decide (H.vertices + H.constraints.length ≤ v.val) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.simpleBipartite
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide_count line 209
Source documentation
Satisfaction correspondence for every labeling of the actual numbered output.
```
theorem subdivide_count {q : Nat} (H : Instance q)
    (a : Fin (H.vertices + 3 * H.constraints.length) → Fin q) :
    countSatisfied a (subdivide H).constraints =
      (Subdivision.game (ofInstance H)).satisfiedCount
        (fun l => a (numericVertexEquiv H.vertices H.constraints.length (Sum.inl l)))
        (fun r => a (numericVertexEquiv H.vertices H.constraints.length (Sum.inr r))) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide, OAI.UniqueGamesTheorem.Explicit.Subdivision.game, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.numericVertexEquiv
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide_value line 218
Source documentation
The serialized output has exactly the abstract subdivision value.
```
theorem subdivide_value {q : Nat} (H : Instance q) :
    Integration.InstanceValue.value (subdivide H) =
      (Subdivision.game (ofInstance H)).value :=
…
```
Mentions: OAI.UniqueGamesTheorem.Integration.InstanceValue.value, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide, OAI.UniqueGamesTheorem.Explicit.Subdivision.game, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.ofInstance
theorem OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.value_eq line 224
Source documentation
Exact equation (bipartization-value) for the concrete list/table format.
```
theorem value_eq {q : Nat} (H : Instance q) (hq : 0 < q) :
    Integration.InstanceValue.value (subdivide H) =
      1 - (1 - Integration.InstanceValue.value H) / 4 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Integration.InstanceValue.value, OAI.UniqueGamesTheorem.Explicit.SubdivisionTarget.subdivide