ProductTarget.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Explicit numbered permutation-table outputs for bipartite graphs and products. All numbering maps are supplied as actual equivalences; the product uses the computable radix equivalence with division/remainder inverse, never an arbitrary finite-type enumeration. The value bridge preserves every list occurrence.

def OAI.UniqueGamesTheorem.Explicit.ProductTarget.fullTable line 26
Source documentation
Full forward and inverse tables of an explicit finite permutation.
```
def fullTable (p : Equiv.Perm (Fin q)) : PermutationTable q where
…
```
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.fullTable_images line 32
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.permutationEquiv_fullTable line 35
def OAI.UniqueGamesTheorem.Explicit.ProductTarget.row line 41
Source documentation
One explicitly addressed row, with a separately supplied complete table.
```
def row (G : BipartiteGame L R E (Fin q)) (vertices : (L ⊕ R) ≃ Fin N)
    (edges : Fin M ≃ E) (tables : E → PermutationTable q) (i : Fin M) :
    Constraint N q where
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
def OAI.UniqueGamesTheorem.Explicit.ProductTarget.render line 48
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_length line 59
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_get line 65
def OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_simpleBipartite line 74

theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_count line 103

Source documentation

A full vertex labeling pulls back to two independently local labelings.

theorem render_count (G : BipartiteGame L R E (Fin q))
    (vertices : (L ⊕ R) ≃ Fin N) (edges : Fin M ≃ E)
    (tables : E → PermutationTable q) (hM : 0 < M)
    (htable : ∀ e, permutationEquiv (tables e) = G.permutation e)
    (labeling : Fin N → Fin q) :
    countSatisfied labeling (render G vertices edges tables hM).constraints =
      G.satisfiedCount (fun x => labeling (vertices (Sum.inl x)))
        (fun y => labeling (vertices (Sum.inr y))) := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame, OAI.UniqueGamesTheorem.Explicit.ProductTarget.render

def OAI.UniqueGamesTheorem.Explicit.ProductTarget.mergeLabelings line 121
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.mergeLabelings_left line 125
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.mergeLabelings_right line 130
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_count_merge line 135
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_maxSatisfied line 147
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.render_value line 167
def OAI.UniqueGamesTheorem.Explicit.ProductTarget.tuples line 181
Source documentation
The product order is increasing radix address, with coordinate zero the least significant digit. The inverse computes each digit by division/modulo.
```
def tuples (n t : ℕ) : List (Fin t → Fin n) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.tuples_length line 184
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.tuples_mem line 187
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.tuples_nodup line 191
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.tuples_get line 194
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.tuple_address line 199
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.address_eq_ofDigits line 205
Source documentation
The explicit address and ofDigits share the same least-significant-first coordinate order, with no restriction on the radix beyond the digit type.
```
theorem address_eq_ofDigits {n t : ℕ} (f : Fin t → Fin n) :
    (finFunctionFinEquiv f : ℕ) = Nat.ofDigits n (List.ofFn (fun i => (f i : ℕ))) := by
…
```
theorem OAI.UniqueGamesTheorem.Explicit.ProductTarget.address_eq_horner line 218
Source documentation
A forward Horner controller reads the coordinate words in reverse order. This is a word-order identity, separate from its machine execution theorem.
```
theorem address_eq_horner {n t : ℕ} (f : Fin t → Fin n) :
    (finFunctionFinEquiv f : ℕ) =
      (List.ofFn (fun i => (f i : ℕ))).reverse.foldl
        (fun acc digit => n * acc + digit) 0 := by
…
```