Vec.lean`

75 declarations, 0 contain sorry, 0 declared as axioms

Exact tree gate and slice symmetry. Sign values are encoded in ZMod 2: b encodes (-1)^b.

abbrev OAI.OptimalMaxCut.Unweighted.Vec line 11
def OAI.OptimalMaxCut.Unweighted.dot line 13
theorem OAI.OptimalMaxCut.Unweighted.card_vec line 17
theorem OAI.OptimalMaxCut.Unweighted.dot_comm line 21
theorem OAI.OptimalMaxCut.Unweighted.dot_add_right line 24
theorem OAI.OptimalMaxCut.Unweighted.dot_sub_left line 28
theorem OAI.OptimalMaxCut.Unweighted.dot_zero_right line 32
def OAI.OptimalMaxCut.Unweighted.dotChar line 34
theorem OAI.OptimalMaxCut.Unweighted.norm_stdChar line 39
theorem OAI.OptimalMaxCut.Unweighted.dotChar_ne_one line 43
theorem OAI.OptimalMaxCut.Unweighted.sum_dotChar line 55
theorem OAI.OptimalMaxCut.Unweighted.conj_stdChar line 63
theorem OAI.OptimalMaxCut.Unweighted.orthogonality line 67
theorem OAI.OptimalMaxCut.Unweighted.rectangle_energy line 76
theorem OAI.OptimalMaxCut.Unweighted.rectangle_character_bound line 89
def OAI.OptimalMaxCut.Unweighted.beta line 120
Source documentation
Fourier coefficient of the residue indicator, probability normalization.
```
noncomputable def beta (I : Finset (ZMod p)) (h : ZMod p) : ℂ :=
…
```
theorem OAI.OptimalMaxCut.Unweighted.beta_zero line 123
theorem OAI.OptimalMaxCut.Unweighted.beta_norm_le_one line 126
theorem OAI.OptimalMaxCut.Unweighted.residue_fourier line 139
def OAI.OptimalMaxCut.Unweighted.rectangleCount line 157
theorem OAI.OptimalMaxCut.Unweighted.rectangle_fourier line 161
Source documentation
Isolate the zero frequency in the rectangle count.
```
theorem rectangle_fourier (I : Finset (ZMod p)) (S T : Finset (Vec p)) :
    (rectangleCount I S T : ℂ) - (I.card : ℂ) / p * S.card * T.card =
      ∑ h ∈ (univ : Finset (ZMod p)).erase 0,
        beta I h * ∑ x ∈ S, ∑ y ∈ T, ZMod.stdAddChar (h * dot x y) := by
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec, OAI.OptimalMaxCut.Unweighted.rectangleCount, OAI.OptimalMaxCut.Unweighted.beta, OAI.OptimalMaxCut.Unweighted.dot
theorem OAI.OptimalMaxCut.Unweighted.rectangle_discrepancy_count line 182
Source documentation
Absolute discrepancy in edge counts before dividing by Q=p^12.
```
theorem rectangle_discrepancy_count (I : Finset (ZMod p)) (S T : Finset (Vec p)) :
    |(rectangleCount I S T : ℝ) - (I.card : ℝ) / p * S.card * T.card| ≤ (p : ℝ) ^ 10 := by
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec, OAI.OptimalMaxCut.Unweighted.rectangleCount
def OAI.OptimalMaxCut.Unweighted.residueSet line 207
theorem OAI.OptimalMaxCut.Unweighted.card_residueSet line 210
theorem OAI.OptimalMaxCut.Unweighted.residue_density_error line 223
Source documentation
The exact rounding loss uses the original rational weight, not a renormalized one.
```
theorem residue_density_error (w : ℚ) (hw : 0 ≤ w) (hw1 : w ≤ 1) :
    |((residueSet (p := p) w).card : ℝ) / p - w| ≤ 1 / (p : ℝ) := by
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.residueSet
theorem OAI.OptimalMaxCut.Unweighted.rectangle_discrepancy line 238
def OAI.OptimalMaxCut.Unweighted.cutMass line 292
theorem OAI.OptimalMaxCut.Unweighted.sum_cutMass line 295
theorem OAI.OptimalMaxCut.Unweighted.cutMass_nonneg line 301

theorem OAI.OptimalMaxCut.Unweighted.independent_pair line 308

Source documentation

Two distinct coordinates of a product law, proved by finite product expansion.

theorem independent_pair (f : V → Bool → ℝ) (hf : ∀ i, ∑ b : Bool, f i b = 1)
    (u v : V) (huv : u ≠ v) (g k : Bool → ℝ) :
    ∑ σ : V → Bool, (∏ i, f i (σ i)) * g (σ u) * k (σ v) =
      (∑ b : Bool, f u b * g b) * (∑ b : Bool, f v b * k b) := by
…

theorem OAI.OptimalMaxCut.Unweighted.cutMass_crossing line 335

Source documentation

Probability that two distinct vertices receive different cut signs.

theorem cutMass_crossing (a : V → ℝ) (u v : V) (huv : u ≠ v) :
    ∑ σ : V → Bool, cutMass a σ * (if σ u ≠ σ v then 1 else 0) =
      a u * (1 - a v) + (1 - a u) * a v := by
…

Mentions: OAI.OptimalMaxCut.Unweighted.cutMass

def OAI.OptimalMaxCut.Unweighted.weightedCut line 355
Source documentation
Weighted cut on unordered distinct vertex pairs, on the original weight scale.
```
def weightedCut {N : ℕ} (w : Fin N → Fin N → ℝ) (σ : Fin N → Bool) : ℝ :=
…
```
def OAI.OptimalMaxCut.Unweighted.weightedMax line 358
theorem OAI.OptimalMaxCut.Unweighted.weightedCut_le_max line 361
theorem OAI.OptimalMaxCut.Unweighted.weightedMax_attained line 365
def OAI.OptimalMaxCut.Unweighted.fractionalCut line 372
Source documentation
Expected cut weight under independent randomized rounding.
```
def fractionalCut {N : ℕ} (w : Fin N → Fin N → ℝ) (a : Fin N → ℝ) : ℝ :=
…
```
theorem OAI.OptimalMaxCut.Unweighted.fractionalCut_expectation line 375
theorem OAI.OptimalMaxCut.Unweighted.fractionalCut_le_max line 396
Source documentation
Rounding cannot exceed an actual integral maximum cut.
```
theorem fractionalCut_le_max {N : ℕ} (w : Fin N → Fin N → ℝ) (a : Fin N → ℝ)
    (ha : ∀ u, 0 ≤ a u ∧ a u ≤ 1) : fractionalCut w a ≤ weightedMax w := by
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.fractionalCut, OAI.OptimalMaxCut.Unweighted.weightedMax
def OAI.OptimalMaxCut.Unweighted.vecEquiv line 405
def OAI.OptimalMaxCut.Unweighted.vertexEquiv line 410
Source documentation
Explicit lexicographic indexing of all Np^6 output vertices.
```
def vertexEquiv (N : ℕ) : (Fin N × Vec p) ≃ Fin (N * p ^ 6) :=
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec
theorem OAI.OptimalMaxCut.Unweighted.vertexEquiv_val line 413
theorem OAI.OptimalMaxCut.Unweighted.vertexEquiv_lt_of_lt line 416
theorem OAI.OptimalMaxCut.Unweighted.vertexEquiv_lt_iff_of_ne line 423
def OAI.OptimalMaxCut.Unweighted.blowupGraph line 433
Source documentation
The actual simple unweighted finite output graph, not an abstract promise.
```
def blowupGraph {N : ℕ} (w : Fin N → Fin N → ℚ) (hw : ∀ u v, w u v = w v u) : Graph where
…
```
Mentions: OAI.OptimalMaxCut.Graph
def OAI.OptimalMaxCut.Unweighted.blowupOutput line 446
Source documentation
The scale is p^12, not the output number of edges.
```
def blowupOutput {N : ℕ} (w : Fin N → Fin N → ℚ) (hw : ∀ u v, w u v = w v u) : ScaledGraph where
…
```
Mentions: OAI.OptimalMaxCut.ScaledGraph
theorem OAI.OptimalMaxCut.Unweighted.blowup_adj line 451
def OAI.OptimalMaxCut.Unweighted.clusterCutCount line 458
Source documentation
A cut expressed in cluster coordinates.
```
def clusterCutCount {N : ℕ} (w : Fin N → Fin N → ℚ) (σ : Fin N → Vec p → Bool) : ℕ :=
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec
theorem OAI.OptimalMaxCut.Unweighted.blowup_cutSize line 463
def OAI.OptimalMaxCut.Unweighted.cutSet line 499
Source documentation
Either side of a cut inside one cluster.
```
def cutSet (σ : Vec p → Bool) (b : Bool) : Finset (Vec p) :=
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec
theorem OAI.OptimalMaxCut.Unweighted.mem_cutSet line 502
theorem OAI.OptimalMaxCut.Unweighted.cutSet_card_partition line 505
def OAI.OptimalMaxCut.Unweighted.cutFraction line 512
Source documentation
Fraction of a cluster on the positive side, on the exact p^6 scale.
```
noncomputable def cutFraction (σ : Vec p → Bool) : ℝ := (cutSet σ true).card / (p : ℝ) ^ 6
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec, OAI.OptimalMaxCut.Unweighted.cutSet
theorem OAI.OptimalMaxCut.Unweighted.cutFraction_mem line 514
theorem OAI.OptimalMaxCut.Unweighted.cutFraction_false line 523
def OAI.OptimalMaxCut.Unweighted.pairCutCount line 533
Source documentation
The exact edge count crossing between two distinct clusters.
```
def pairCutCount (w : ℚ) (σ τ : Vec p → Bool) : ℕ :=
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.Vec
theorem OAI.OptimalMaxCut.Unweighted.rectangle_cutSet line 536
theorem OAI.OptimalMaxCut.Unweighted.pairCutCount_rectangles line 549
theorem OAI.OptimalMaxCut.Unweighted.pairCutCount_discrepancy line 562

theorem OAI.OptimalMaxCut.Unweighted.twice_pair_count line 583

Source documentation

Twice the number of unordered distinct pairs, including N=0 and N=1.

theorem twice_pair_count (N : ℕ) :
    (∑ u : Fin N, ∑ v : Fin N, if u < v then (2 : ℝ) else 0) =
      (N : ℝ) * ((N : ℝ) - 1) := by
…

theorem OAI.OptimalMaxCut.Unweighted.clusterCutCount_discrepancy line 595

Source documentation

Summing the exact pair loss on the common unnormalized scale.

theorem clusterCutCount_discrepancy {N : ℕ} (w : Fin N → Fin N → ℚ)
    (hbound : ∀ u v, u < v → 0 ≤ w u v ∧ w u v ≤ 1)
    (σ : Fin N → Vec p → Bool) :
    |(clusterCutCount w σ : ℝ) / (p : ℝ) ^ 12 -
      fractionalCut (fun u v => (w u v : ℝ)) (fun u => cutFraction (σ u))| ≤
      (N : ℝ) * ((N : ℝ) - 1) * (1 / (p : ℝ) + 1 / (p : ℝ) ^ 2) := by
…

Mentions: OAI.OptimalMaxCut.Unweighted.Vec, OAI.OptimalMaxCut.Unweighted.clusterCutCount, OAI.OptimalMaxCut.Unweighted.fractionalCut, OAI.OptimalMaxCut.Unweighted.cutFraction

theorem OAI.OptimalMaxCut.Unweighted.graph_cut_le_max line 633
Source documentation
Every cut lies below the finite unweighted optimum.
```
theorem graph_cut_le_max (G : Graph) (σ : Fin G.vertices → Bool) :
    G.cutSize σ ≤ G.maxCut := by
…
```
Mentions: OAI.OptimalMaxCut.Graph
theorem OAI.OptimalMaxCut.Unweighted.graph_max_attained line 639
Source documentation
The finite unweighted optimum is attained by an actual cut.
```
theorem graph_max_attained (G : Graph) : ∃ σ, G.cutSize σ = G.maxCut := by
…
```
Mentions: OAI.OptimalMaxCut.Graph
theorem OAI.OptimalMaxCut.Unweighted.cutFraction_const line 646
theorem OAI.OptimalMaxCut.Unweighted.fractionalCut_integral line 651
theorem OAI.OptimalMaxCut.Unweighted.blowup_maxCut_error line 662
Source documentation
Full optimum comparison for the actual simple finite graph. No complexity certificate is asserted in this analytic/combinatorial theorem.
```
theorem blowup_maxCut_error {N : ℕ} (w : Fin N → Fin N → ℚ)
    (hw : ∀ u v, w u v = w v u)
    (hbound : ∀ u v, u < v → 0 ≤ w u v ∧ w u v ≤ 1) :
    |((blowupGraph (p := p) w hw).maxCut : ℝ) / (p : ℝ) ^ 12 -
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.blowupGraph
def OAI.OptimalMaxCut.Unweighted.totalWeight line 694
theorem OAI.OptimalMaxCut.Unweighted.normalized_pair_bound line 697
def OAI.OptimalMaxCut.Unweighted.searchPrime line 719
Source documentation
Bounded deterministic prime search. Its bound follows from Bertrand, not a prime oracle or an unbounded assumed operation.
```
def searchPrime (m : ℕ) : ℕ :=
…
```
theorem OAI.OptimalMaxCut.Unweighted.searchPrime_spec line 722
def OAI.OptimalMaxCut.Unweighted.deterministicOutput line 740
theorem OAI.OptimalMaxCut.Unweighted.selected_prime_error line 746
theorem OAI.OptimalMaxCut.Unweighted.deterministicOutput_error line 778
theorem OAI.OptimalMaxCut.Unweighted.deterministicOutput_vertex_bound line 791
Source documentation
Explicit polynomial vertex bound for fixed K. It is a size bound, not by itself a certificate of polynomial running time.
```
theorem deterministicOutput_vertex_bound {N : ℕ} (K : ℕ)
    (w : Fin N → Fin N → ℚ) (hw : ∀ u v, w u v = w v u) :
    (deterministicOutput K w hw).graph.vertices ≤ N * (2 * (K * (N + 1) ^ 2 + 1)) ^ 6 := by
…
```
Mentions: OAI.OptimalMaxCut.Unweighted.deterministicOutput
theorem OAI.OptimalMaxCut.Unweighted.deterministicOutput_scale_bound line 796
theorem OAI.OptimalMaxCut.Unweighted.unweighted_finite_error line 801