Product.lean`

68 declarations, 0 contain sorry, 0 declared as axioms

The independent graph product in the last step of the v2 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.MaxCutGames.Explicit.BipartiteGame.product line 28
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_left line 44
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_right line 47
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_permutation line 50
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_isTranslation line 54
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_edge_card line 62
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_left_card line 65
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_right_card line 68
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_edges_nonempty line 71
def OAI.MaxCutGames.Explicit.BipartiteGame.toGame line 80
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.toGame_accepts_on_edge line 88
theorem OAI.MaxCutGames.Explicit.BipartiteGame.toGame_isProjection line 103
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) :
    MaxCutGames.Repetition.IsProjection G.toGame := by
…
```
Mentions: OAI.MaxCutGames.Explicit.BipartiteGame, OAI.MaxCutGames.Repetition.IsProjection
def OAI.MaxCutGames.Explicit.BipartiteGame.occurrenceSuccess line 115
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.toGame_success line 121
theorem OAI.MaxCutGames.Explicit.BipartiteGame.toGame_success_eq_satisfiedCount line 142
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_uniform_edge_law line 157
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.MaxCutGames.Explicit.BipartiteGame.product_success_eq_repetition line 164
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_coordinate_success line 195
theorem OAI.MaxCutGames.Explicit.BipartiteGame.one_sub_mul_one_sub_le_pow line 202
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.MaxCutGames.Explicit.BipartiteGame.product_coordinate_completeness line 215

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.MaxCutGames.Explicit.BipartiteGame

theorem OAI.MaxCutGames.Explicit.BipartiteGame.toGame_value line 230
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_value_eq_repetition line 244
theorem OAI.MaxCutGames.Explicit.BipartiteGame.product_completeness line 256
def OAI.MaxCutGames.Explicit.BipartiteGame.relabel line 266
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.MaxCutGames.Explicit.BipartiteGame
theorem OAI.MaxCutGames.Explicit.BipartiteGame.relabel_isTranslation line 273

theorem OAI.MaxCutGames.Explicit.BipartiteGame.relabel_success line 288

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.MaxCutGames.Explicit.BipartiteGame

theorem OAI.MaxCutGames.Explicit.BipartiteGame.relabel_success_forward line 309
theorem OAI.MaxCutGames.Explicit.BipartiteGame.relabel_value line 318
def OAI.MaxCutGames.Explicit.BipartiteGame.binaryProductEquiv line 335
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.MaxCutGames.Explicit.BipartiteGame.binaryProduct line 347
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_isTranslation line 351
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_dimension_positive line 356
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_alphabet_card line 359
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_value_eq_repetition line 366
theorem OAI.MaxCutGames.Explicit.BipartiteGame.binaryProduct_completeness line 371
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.row line 403
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.render line 409
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.render_length line 419
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.render_get line 423
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.simpleBipartite line 431
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.count line 460
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.extendLabelings line 474
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.extendLabelings_left line 480
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.extendLabelings_right line 486
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.maxSatisfied line 491
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.Embedded.value line 508
abbrev OAI.MaxCutGames.Explicit.ProductPaddedOutput.Left line 522
abbrev OAI.MaxCutGames.Explicit.ProductPaddedOutput.Right line 523
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.graph line 525
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.vertices line 532
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.MaxCutGames.Explicit.ProductPaddedOutput.Left, OAI.MaxCutGames.Explicit.ProductPaddedOutput.Right
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.side line 564
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.side_left line 567
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.side_right line 575
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.outputRow line 583
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.output line 588
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_vertices line 592
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_constraints line 595
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_length line 598
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.simpleBipartite line 601
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.outputRow_source line 605
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.outputRow_target line 611
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.outputRow_images line 617
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_gameWords line 626
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_value_eq_repetition line 634
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_completeness line 644
def OAI.MaxCutGames.Explicit.ProductPaddedOutput.finalCoordinates line 655
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.finalCoordinates_apply line 661
theorem OAI.MaxCutGames.Explicit.ProductPaddedOutput.output_translations line 666