ZigzagGraphsLemmas.lean`

93 declarations, 0 contain sorry, 0 declared as axioms

Actual graph squares and zigzag products

Rotations operate on actual vertex-port pairs. All returned ports are retained, including ports belonging to loops and parallel edges. Each construction is a palindrome of involutions and hence defines a reversible regular port graph.

def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.involutionEquiv line 26
Source documentation
Regard a checked involution as a permutation with the same inverse.
```
def involutionEquiv {A : Type*} (f : A → A) (hf : Function.Involutive f) : A ≃ A where
…
```

theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 33

Source documentation

A palindrome of two involutions is itself an involution.

theorem palindrome_involutive {A : Type*} (B P : A ≃ A)
    (hB : Function.Involutive B) (hP : Function.Involutive P) :
    Function.Involutive (B.trans (P.trans B)) := by
…

def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.squareFirst line 41
Source documentation
Cross an original edge using the first port; retain its return port.
```
def squareFirst (G : PortGraph V D) (s : V × (D × D)) : V × (D × D) :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 45
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.squareSwap line 51
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 53
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.square line 58
Source documentation
The actual graph square. The two return ports appear in reverse order.
```
def square (G : PortGraph V D) : PortGraph V (D × D) := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.square_rot_apply line 66
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.square_next line 72
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.cloudFirst line 76
Source documentation
One inner step in a cloud, retaining its return port and the unused port.
```
def cloudFirst (H : PortGraph D E) (s : (V × D) × (E × E)) :
    (V × D) × (E × E) :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 81
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.crossCloud line 89
Source documentation
Cross the outer graph edge and swap the two inner ports.
```
def crossCloud (G : PortGraph V D) (s : (V × D) × (E × E)) :
    (V × D) × (E × E) := (G.rot s.1, (s.2.2, s.2.1))
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 92
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.zigzag line 99
Source documentation
The actual zigzag product: inner step, outer edge, inner step.
```
def zigzag (G : PortGraph V D) (H : PortGraph D E) : PortGraph (V × D) (E × E) := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 107
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 115
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 118
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 122
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 125
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 128
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.cloudOperator line 138
Source documentation
Average only the inner cloud coordinate, keeping the outer vertex fixed.
```
def cloudOperator [Fintype E] (H : PortGraph D E) (f : V × D → ℝ) (x : V × D) : ℝ :=
…
```
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.graphPermutation line 142
Source documentation
The permutation on cloud vertices induced by the actual outer rotation.
```
def graphPermutation (G : PortGraph V D) (f : V × D → ℝ) (x : V × D) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 146
Source documentation
Uniform averaging on the graph square is two original averaging steps.
```
theorem averagingOperator_square [Fintype D] (G : PortGraph V D) (f : V → ℝ) :
    SpectralReturn.averagingOperator (square G) f =
      SpectralReturn.averagingOperator G (SpectralReturn.averagingOperator G f) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.averagingOperator, OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.square
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 157
Source documentation
The zigzag operator is precisely inner average, outer permutation, inner average. This factorization follows from the actual rotation formula.
```
theorem averagingOperator_zigzag [Fintype E] (G : PortGraph V D)
    (H : PortGraph D E) (f : V × D → ℝ) :
    SpectralReturn.averagingOperator (zigzag G H) f =
      cloudOperator H (graphPermutation G (cloudOperator H f)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.averagingOperator, OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.zigzag, OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.cloudOperator, OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagGraphs.graphPermutation
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudMean line 195
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.liftCloud line 198
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.projection line 200
def OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.centered line 203
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.mean_liftCloud line 205
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.energy_liftCloud line 211
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.mean_cloudMean line 215
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.energy_prod line 218
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudMean_centered_zero line 222
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.energy_centered_eq_sub line 228
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.projection_energy_decomposition line 251
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.energy_projection_le line 256
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.energy_centered_le line 262
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.mean_sq_le_energy line 268
Source documentation
Squared normalized mean is bounded by normalized squared energy.
```
theorem mean_sq_le_energy {A : Type*} [Fintype A] [Nonempty A] (f : A → ℝ) :
    mean f ^ 2 ≤ energy f := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.averaging_energy_le line 274
Source documentation
Every actual reversible regular graph average is an energy contraction.
```
theorem averaging_energy_le [Fintype V] [Fintype D] [Nonempty V] [Nonempty D]
    (G : PortGraph V D) (f : V → ℝ) : energy (averagingOperator G f) ≤ energy f := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudOperator_add line 283
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudOperator_sub line 288
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudOperator_projection line 293
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudOperator_centered line 299
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.graphPermutation_energy line 305
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloud_energy_le line 309
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloud_centered_contraction line 319
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloud_residual_bound line 331
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.projection_graphPermutation_projection line 342
Source documentation
Cloud projection of the outer permutation is the genuine outer graph average when its input is constant on each cloud.
```
theorem projection_graphPermutation_projection [Fintype D] (G : PortGraph V D)
    (f : V × D → ℝ) :
    projection (graphPermutation G (projection f)) =
      liftCloud (averagingOperator G (cloudMean f)) := rfl
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.projection, OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.liftCloud, OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.cloudMean
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.projected_outer_bound line 347
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.energy_add_three_le line 361

theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.zigzag_energy_bound line 374

Source documentation

A deliberately loose bound sufficient for the expander iteration.

theorem zigzag_energy_bound [Fintype V] [Fintype D] [Fintype E]
    [Nonempty D] [Nonempty E]
    (G : PortGraph V D) (H : PortGraph D E) (lambdaG lambdaH : ℝ)
    (hG : SpectralCertificate G lambdaG) (hH : SpectralCertificate H lambdaH)
    (f : V × D → ℝ) (hf : mean f = 0) :
    energy (averagingOperator (zigzag G H) f) ≤
      3 * (lambdaG ^ 2 + lambdaH ^ 2) * energy f := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.square_certificate line 426

theorem OAI.UniqueGamesTheorem.Foundations.PCP.ZigzagSpectral.square_zigzag_halfCertificate line 446

Source documentation

Squaring an outer graph with certificate 1/2, then zigzagging with an inner graph with certificate 1/100, again has certificate 1/2.

theorem square_zigzag_halfCertificate [Fintype V] [Fintype D] [Fintype E]
    [Nonempty V] [Nonempty D] [Nonempty E]
    (G : PortGraph V D) (H : PortGraph (D × D) E)
    (hG : SpectralCertificate G (1 / 2)) (hH : SpectralCertificate H (1 / 100)) :
    SpectralCertificate (zigzag (square G) H) (1 / 2) where
…

abbrev OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Port line 481
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.CloudPort line 482
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth line 483
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.card_port line 485
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.card_cloudPort line 489
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth_gt_one line 495
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 498
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 502
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.baseOnCloud line 505
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 508
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Vertex line 511
instance OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.vertexFintype line 515
instance OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.basePortNonempty line 523
instance OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.vertexNonempty line 526
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.graph line 535
Source documentation
The family is a recursive rotation algorithm when its fixed base is given.
```
def graph (H : PortGraph CloudPort BasePort) : (n : Nat) → PortGraph (Vertex n) Port
  | 0 => { rot := Equiv.refl _, rot_involutive := fun _ => rfl }
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.CloudPort, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Port
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.graph_certificate line 539
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.family line 562
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.family_certificate line 564
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.card_vertex line 567
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.level line 576
Source documentation
The least geometric level covering a requested size. Nat.clog is the ordinary finite ceiling logarithm algorithm.
```
def level (k : Nat) : Nat := Nat.clog growth k
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth
def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.size line 578
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.le_size line 580
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.size_le_mul line 582
theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.padded_family_size line 596
def OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.paddedSize line 625
Source documentation
Leave empty clouds empty; pad every positive size to a geometric level.
```
def paddedSize (k : Nat) : Nat := if k = 0 then 0 else ExpanderFamily.size k
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.size
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.paddedSize_zero line 627
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.paddedSize_of_pos line 629
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.le_paddedSize line 633
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.paddedSize_le_mul line 640
def OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.paddedCloudEquiv line 649
Source documentation
The actual padded tail fiber contains old darts and exactly the dummy darts indexed by that tail, with transport along the sigma index equality.
```
def paddedCloudEquiv (G : ConstraintGraph V E A) (dummy : V → Type*) (v : V) :
    Cloud (paddedGraph G dummy) v ≃ Cloud G v ⊕ dummy v where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy
def OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dartCloudEquiv line 673
Source documentation
Every original dart occurs in exactly one cloud.
```
def dartCloudEquiv (G : ConstraintGraph V E A) : E ≃ Σ v : V, Cloud G v where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.sum_card_cloud line 686
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_padded_cloud line 690
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy line 697
Source documentation
The precise number of always-accepting loop darts to add at each vertex.
```
abbrev dummy (G : ConstraintGraph V E A) (v : V) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_cloud line 700
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_dummy_of_empty line 708
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_cloud_of_empty line 712
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_cloud_eq_family line 717
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_paddedDart_eq_sum line 726
Source documentation
Exact count over all padded tail fibers, including empty original fibers.
```
theorem card_paddedDart_eq_sum (G : ConstraintGraph V E A) :
    Fintype.card (PaddedDart G (dummy G)) =
      ∑ v, paddedSize (Fintype.card (Cloud G v)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.paddedSize
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.card_paddedDart_le line 740
Source documentation
Padding increases the total number of darts by at most the fixed family growth factor, independent of the number of empty vertices.
```
theorem card_paddedDart_le (G : ConstraintGraph V E A) :
    Fintype.card (PaddedDart G (dummy G)) ≤ ExpanderFamily.growth * Fintype.card E := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth