ProductLemmas.lean`

88 declarations, 0 contain sorry, 0 declared as axioms

The independent graph product in the last step of the reduction.

Edges are tuples of actual base edges. The endpoint maps remain injective, the edge law is exactly uniform, and the associated game agrees with ordinary parallel repetition for every pair of local strategies, including strategies depending on their whole question tuples. Only the completeness lower bound uses coordinatewise strategies; no repetition soundness bound is assumed here.

def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product line 36
Source documentation
Independent tuples of edges and labels. The two endpoint types keep the two parts separate, even when the base sets happen to have the same type.
```
def product (G : BipartiteGame L R E A) (t : ℕ) :
    BipartiteGame (Fin t → L) (Fin t → R) (Fin t → E) (Fin t → A) where
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_left line 52
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_right line 55
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_permutation line 58
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_isTranslation line 62
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_edge_card line 70
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_left_card line 73
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_right_card line 76
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_edges_nonempty line 79
def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.toGame line 88
Source documentation
Each actual edge has equal weight. Simplicity makes the acceptance predicate at its endpoint pair exactly its permutation constraint.
```
def toGame (G : BipartiteGame L R E A) : Game L R A A := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.toGame_accepts_on_edge line 96
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.toGame_isProjection line 111
Source documentation
At most one accepting right answer exists for each local question pair and left answer, including question pairs with zero edge weight.
```
theorem toGame_isProjection (G : BipartiteGame L R E A) :
    UniqueGamesTheorem.Repetition.IsProjection G.toGame := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame, OAI.UniqueGamesTheorem.Repetition.IsProjection
def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.occurrenceSuccess line 123
Source documentation
Acceptance probability directly on the uniform occurrence set.
```
def occurrenceSuccess (G : BipartiteGame L R E A)
    (strategy : Strategy L R A A) : ℝ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.toGame_success line 129
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.toGame_success_eq_satisfiedCount line 150
Source documentation
The probabilistic game evaluates the same unweighted edge fraction as the explicit graph's integer occurrence counter.
```
theorem toGame_success_eq_satisfiedCount [DecidableEq A]
    (G : BipartiteGame L R E A) (strategy : Strategy L R A A) :
    G.toGame.success strategy =
      (G.satisfiedCount strategy.1 strategy.2 : ℝ) / Fintype.card E := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_uniform_edge_law line 165
Source documentation
Independent uniform draws of base edges are exactly the uniform product edge law, without reweighting or collapsing occurrences.
```
theorem product_uniform_edge_law (t : ℕ) :
    (FiniteDistribution.uniform E).iid t =
      FiniteDistribution.uniform (Fin t → E) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_success_eq_repetition line 172
Source documentation
The graph construction agrees with the ordinary independent repeated game for arbitrary local tuple strategies. This is the soundness interface.
```
theorem product_success_eq_repetition (G : BipartiteGame L R E A) (t : ℕ)
    (strategy : Strategy (Fin t → L) (Fin t → R) (Fin t → A) (Fin t → A)) :
    (G.product t).toGame.success strategy = (G.toGame.repetition t).success strategy := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_coordinate_success line 203
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.one_sub_mul_one_sub_le_pow line 210
Source documentation
Scalar union bound, proved for the actual base success probability.
```
theorem one_sub_mul_one_sub_le_pow {p : ℝ} (hp0 : 0 ≤ p) (_hp1 : p ≤ 1) (t : ℕ) :
    1 - (t : ℝ) * (1 - p) ≤ p ^ t := by
…
```
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_coordinate_completeness line 223
Source documentation
The coordinatewise honest labeling loses at most t times the base error. This does not restrict the strategies covered by the soundness bridge.
```
theorem product_coordinate_completeness (G : BipartiteGame L R E A) (t : ℕ)
    (strategy : Strategy L R A A) {error : ℝ}
    (hcomplete : 1 - error ≤ G.toGame.success strategy) :
    1 - (t : ℝ) * error ≤
      (G.product t).toGame.success (Game.repeatStrategy strategy t) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.toGame_value line 238
Source documentation
The finite maximum over arbitrary local strategies is exactly the explicit graph value used by the subdivision identity.
```
theorem toGame_value [DecidableEq A] (G : BipartiteGame L R E A) :
    G.toGame.value = G.value := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_value_eq_repetition line 252
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_completeness line 264
def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.relabel line 274
Source documentation
A change of alphabet coordinates keeps endpoints and edge identities.
```
def relabel {B : Type*} (G : BipartiteGame L R E A) (e : A ≃ B) :
    BipartiteGame L R E B where
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.relabel_isTranslation line 281

theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.relabel_success line 296

Source documentation

Alphabet coordinates are changed locally at each endpoint.

theorem relabel_success (G : BipartiteGame L R E A) (e : A ≃ B)
    (strategy : Strategy L R B B) :
    (G.relabel e).toGame.success strategy =
      G.toGame.success (fun x => e.symm (strategy.1 x), fun y => e.symm (strategy.2 y)) := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame

theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.relabel_success_forward line 317
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.relabel_value line 326
def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProductEquiv line 343
Source documentation
The explicit binary vector coordinates of the final alphabet. The coordinate order is (base bit, repetition coordinate).
```
def binaryProductEquiv (ell t : ℕ) :
    (Fin t → Fin ell → ZMod 2) ≃+ (Fin (ell * t) → ZMod 2) where
…
```
def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct line 355
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_isTranslation line 359
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_dimension_positive line 364
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_alphabet_card line 367
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_value_eq_repetition line 372
theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_completeness line 377
def OAI.UniqueGamesTheorem.Explicit.ProductOutput.tupleCode line 406
Source documentation
Explicit tuple address, with coordinate zero the least significant digit.
```
def tupleCode {X : Type*} {n : ℕ} (code : X ≃ Fin n) (t : ℕ) :
    (Fin t → X) ≃ Fin (n ^ t) where
…
```
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.tupleCode_apply line 413
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.tupleCode_symm_apply line 417
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.tupleCode_val line 421
def OAI.UniqueGamesTheorem.Explicit.ProductOutput.vertexCode line 425
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.vertexCode_left line 429
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.vertexCode_right line 434
def OAI.UniqueGamesTheorem.Explicit.ProductOutput.graph line 440
Source documentation
The label tuple is numbered by its explicit base-q radix code.
```
def graph (G : BipartiteGame L R E (Fin q)) (t : ℕ) :
    BipartiteGame (Fin t → L) (Fin t → R) (Fin t → E) (Fin (q ^ t)) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
def OAI.UniqueGamesTheorem.Explicit.ProductOutput.tables line 444

def OAI.UniqueGamesTheorem.Explicit.ProductOutput.outputRow line 449

Source documentation

A row indexed by its actual place in the emitted edge list.

def outputRow (G : BipartiteGame L R E (Fin q))
    (leftCode : L ≃ Fin l) (rightCode : R ≃ Fin r) (edgeCode : E ≃ Fin m)
    (t : ℕ) (i : Fin (m ^ t)) : Constraint (l ^ t + r ^ t) (q ^ t) :=
…

Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame

def OAI.UniqueGamesTheorem.Explicit.ProductOutput.output line 456
Source documentation
The executable output list has one row for each radix edge-tuple address.
```
def output (G : BipartiteGame L R E (Fin q))
    (leftCode : L ≃ Fin l) (rightCode : R ≃ Fin r) (edgeCode : E ≃ Fin m)
    (t : ℕ) (hm : 0 < m) : Instance (q ^ t) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.output_constraints line 462
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.output_length line 468
def OAI.UniqueGamesTheorem.Explicit.ProductOutput.output_simpleBipartite line 474
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.outputRow_source line 481
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.outputRow_target line 489

theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.outputRow_images line 499

Source documentation

Each complete output-table entry is coordinatewise application of the base permutation, followed by the same radix alphabet encoding.

theorem outputRow_images (G : BipartiteGame L R E (Fin q))
    (leftCode : L ≃ Fin l) (rightCode : R ≃ Fin r) (edgeCode : E ≃ Fin m)
    (t : ℕ) (i : Fin (m ^ t)) (a : Fin (q ^ t)) :
    (outputRow G leftCode rightCode edgeCode t i).permutation.images[a] =
      finFunctionFinEquiv (fun j =>
        G.permutation (edgeCode.symm (finFunctionFinEquiv.symm i j))
          (finFunctionFinEquiv.symm a j)) := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame, OAI.UniqueGamesTheorem.Explicit.ProductOutput.outputRow

theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.output_value line 511
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.output_value_eq_repetition line 518
theorem OAI.UniqueGamesTheorem.Explicit.ProductOutput.output_completeness line 530
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.row line 563
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.render line 569
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.render_length line 579
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.render_get line 583
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.simpleBipartite line 591
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.count line 620
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.extendLabelings line 634
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.extendLabelings_left line 640
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.extendLabelings_right line 646
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.maxSatisfied line 651
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Embedded.value line 668
abbrev OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Left line 682
abbrev OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Right line 683
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.graph line 685
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.vertices line 692
Source documentation
The two genuine product vertex sets embed into the common global radix space. Opposite sides cannot collide because the repetition count is positive.
```
def vertices (t : ℕ) (ht : 0 < t) :
    ((Fin t → Left H presentation) ⊕ (Fin t → Right H presentation)) ↪
      Fin (H.vertices ^ t) where
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Left, OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.Right
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.side line 724
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.side_left line 727
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.side_right line 735
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.outputRow line 743
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output line 748
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_vertices line 752
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_constraints line 755
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_length line 758
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.simpleBipartite line 761
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.outputRow_source line 765
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.outputRow_target line 771
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.outputRow_images line 777
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_gameWords line 786
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_value_eq_repetition line 794
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_completeness line 804
def OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.finalCoordinates line 815
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.finalCoordinates_apply line 821
theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_translations line 826