Dictator.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.OptimalMaxCut.LongCode.bitSign_not line 15
theorem OAI.OptimalMaxCut.LongCode.corrAverage_coordinate line 18
def OAI.OptimalMaxCut.LongCode.Game.dictator line 36
Source documentation
The honest assignment is an actual Boolean cut (coordinate dictators).
```
def dictator (lx : X → Fin q) (x : X) (z : Cube (Fin q)) : ℝ := bitSign (z (lx x))
```
theorem OAI.OptimalMaxCut.LongCode.Game.testCut_complete line 38
def OAI.OptimalMaxCut.LongCode.Law.push line 97
Source documentation
Exact aggregation of rational masses; all collisions are added, not silently treated as different edges.
```
def push (p : Law I) (f : I → J) : Law J where
…
```
Mentions: OAI.OptimalMaxCut.LongCode.Law
theorem OAI.OptimalMaxCut.LongCode.Law.push_average line 104
def OAI.OptimalMaxCut.LongCode.aggregate line 116
Source documentation
A general finite rational law of ordered test endpoints becomes an ordinary symmetric rational graph by adding both orientations and deleting loops.
```
def aggregate {N : ℕ} (p : Law (Fin N × Fin N)) (u v : Fin N) : ℚ :=
…
```
Mentions: OAI.OptimalMaxCut.LongCode.Law
theorem OAI.OptimalMaxCut.LongCode.aggregate_symm line 119
theorem OAI.OptimalMaxCut.LongCode.aggregate_nonneg line 124
theorem OAI.OptimalMaxCut.LongCode.upper_triangle_symmetrize line 131
theorem OAI.OptimalMaxCut.LongCode.aggregate_cut line 148
theorem OAI.OptimalMaxCut.LongCode.aggregate_total line 164
def OAI.OptimalMaxCut.LongCode.Game.edgeDistribution line 191
Source documentation
Fixed explicit vertex enumeration, supplied as a finite equivalence. The semantic theorem does not hide an unweighted conversion or an edge multiset.
```
def edgeDistribution (G : Game X Y E q) (t : ℚ) (ht : t ∈ Set.Icc (-1 : ℚ) 1)
    (enum : X × Cube (Fin q) ≃ Fin N) : Law (Fin N × Fin N) :=
…
```
Mentions: OAI.OptimalMaxCut.LongCode.Game, OAI.OptimalMaxCut.LongCode.Law
def OAI.OptimalMaxCut.LongCode.Game.weights line 195
theorem OAI.OptimalMaxCut.LongCode.Game.weightedCut_testCut line 199
theorem OAI.OptimalMaxCut.LongCode.Game.weightedMax_complete line 209
theorem OAI.OptimalMaxCut.LongCode.Game.exists_weighted_soundness line 221
def OAI.OptimalMaxCut.LongCode.Game.output line 248
Source documentation
The actual simple, unweighted output. Its common integer scale is printed; loops and both orientations have already been handled by exact aggregation.
```
def output (G : Game X Y E q) (t : ℚ) (ht : t ∈ Set.Icc (-1 : ℚ) 1)
    (enum : X × Cube (Fin q) ≃ Fin N) (K : ℕ) : ScaledGraph :=
…
```
Mentions: OAI.OptimalMaxCut.LongCode.Game, OAI.OptimalMaxCut.ScaledGraph
theorem OAI.OptimalMaxCut.LongCode.Game.output_error line 252
theorem OAI.OptimalMaxCut.LongCode.Game.output_complete line 259
theorem OAI.OptimalMaxCut.LongCode.Game.output_vertex_bound line 268

theorem OAI.OptimalMaxCut.LongCode.Game.exists_unweighted_gap_parameters line 276

Source documentation

All constants for the Max-Cut gap, and the fixed deterministic graph transformation, are selected before the input game. This is the semantic component, not the still-required machine-level reduction certificate.

 theorem exists_unweighted_gap_parameters (α : ℝ) (hα : alphaGW < α) (hα1 : α ≤ 1) :
    ∃ (t ε y n : ℚ) (δ : ℝ) (K : ℕ) (ht : t ∈ Set.Icc (-1 : ℚ) 1),
      0 < t ∧ t < 1 ∧ 0 < ε ∧ (ε : ℝ) < 1 / 2 ∧ 0 < δ ∧ δ < 1 / 2 ∧
      0 < K ∧ 0 < y ∧ 0 ≤ n ∧ (n : ℝ) < α * (y : ℝ) ∧
      (∀ {X Y E : Type} [Fintype X] [Fintype Y] [Fintype E]
        {q N : ℕ} (G : Game X Y E q) (enum : X × Cube (Fin q) ≃ Fin N),
        (∃ lx ly, 1 - (ε : ℝ) ≤ G.satisfied lx ly) →
          (y : ℝ) ≤ ((G.output t ht enum K).graph.maxCut : ℝ) / (G.output t ht enum K).scale) ∧
      (∀ {X Y E : Type} [Fintype X] [Fintype Y] [Fintype E]
        {q N : ℕ} (_hq : 0 < q) (G : Game X Y E q) (enum : X × Cube (Fin q) ≃ Fin N),
        G.Sound δ → ((G.output t ht enum K).graph.maxCut : ℝ) / (G.output t ht enum K).scale ≤ (n : ℝ)) := by
…

Mentions: OAI.OptimalMaxCut.alphaGW, OAI.OptimalMaxCut.LongCode.Game

def OAI.OptimalMaxCut.LongCode.Law.fiberSize line 330
theorem OAI.OptimalMaxCut.LongCode.Law.fiberSize_eq_sum line 335
theorem OAI.OptimalMaxCut.LongCode.Law.sum_fiberSize line 341
theorem OAI.OptimalMaxCut.LongCode.Law.fiberSize_pos line 348
def OAI.OptimalMaxCut.LongCode.Law.fiberMarginal line 352
def OAI.OptimalMaxCut.LongCode.Law.fiberConditional line 359
theorem OAI.OptimalMaxCut.LongCode.Law.fiber_joint line 374
theorem OAI.OptimalMaxCut.LongCode.Law.fiber_average line 389
def OAI.OptimalMaxCut.LongCode.InstanceAdapter.ofInstance line 410
theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.satisfaction_formula line 419

theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.count_as_sum line 432

Source documentation

Occurrences retain their list identity: no parallel edge or denominator is silently discarded in the adapter.

 theorem count_as_sum {n : ℕ} (cs : List (Constraint n q)) (l : Fin n → Fin q) :
    (countSatisfied l cs : ℝ) =
      ∑ e : Fin cs.length, if cs[e].permutation.images[l cs[e].source] =
        l cs[e].target then (1 : ℝ) else 0 := by
…

theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.satisfaction_diagonal line 446
def OAI.OptimalMaxCut.LongCode.InstanceAdapter.merge line 450
theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.satisfaction_merge line 454
theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.complete line 464
theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.sound line 470