CayleySpectral.lean`

103 declarations, 0 contain sorry, 0 declared as axioms

Walsh diagonalization of actual Boolean-cube Cayley graphs

Every port is an indexed generator. The rotation keeps the port and adds its generator by pointwise xor, so loops and repeated generators keep their full multiplicity. The Fourier multiplier and energy estimate are proved for this actual averaging operator; no Fourier/operator compatibility is assumed.

def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.zeroFrequency line 26
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 28
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cubeXor_assoc line 33
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 39
def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.xorTranslation line 45
Source documentation
Uniform cube measure is invariant under this explicit xor translation.
```
def xorTranslation (y : Cube I) : Cube I ≃ Cube I where
…
```
def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.rotate line 51
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.rotate_involutive line 54
def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyGraph line 60
Source documentation
The undirected regular port graph generated by the indexed cube vectors.
```
def cayleyGraph (g : D → Cube I) : PortGraph (Cube I) D where
…
```
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 68
def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.splitPortWord line 72
Source documentation
Expose the first actual port in a finite port word.
```
def splitPortWord (n : Nat) : (Fin (n + 1) → D) ≃ D × (Fin n → D) where
…
```

def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.powerGenerators line 81

Source documentation

The generator of a powered port is the xor of its original port word.

def powerGenerators (g : D → Cube I) : (n : Nat) → (Fin n → D) → Cube I
  | 0, _ => zeroFrequency
  | n + 1, p => cubeXor (g (p 0)) (powerGenerators g n (fun j => p j.succ))

/-- These are actual walk displacements, including repeated vertices and ports. -/

Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.zeroFrequency

theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 86
Source documentation
These are actual walk displacements, including repeated vertices and ports.
```
theorem wordEnd_eq_powerGenerators (g : D → Cube I) (n : Nat)
    (x : Cube I) (p : Fin n → D) :
    wordEnd (cayleyGraph g) n x p = cubeXor x (powerGenerators g n p) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyGraph, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.powerGenerators
def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyAverage line 99
Source documentation
Average along the actual outgoing ports of the Cayley graph.
```
def cayleyAverage (g : D → Cube I) (f : Cube I → ℝ) (x : Cube I) : ℝ :=
…
```
def OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue line 103
Source documentation
The eigenvalue is the empirical bias of the generator characters.
```
def eigenvalue (g : D → Cube I) (s : Cube I) : ℝ :=
…
```
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 107
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 110
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 115
Source documentation
Change «variables» through xor translation in the actual Fourier average.
```
theorem coefficient_xorTranslation (f : Cube I → ℝ) (s v : Cube I) :
    coefficient (fun x => f (cubeXor x v)) s = walsh s v * coefficient f s := by
…
```
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 137
Source documentation
Each Walsh character is an eigenvector of the actual Cayley averaging.
```
theorem cayleyAverage_walsh (g : D → Cube I) (s x : Cube I) :
    cayleyAverage g (walsh s) x = eigenvalue g s * walsh s x := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyAverage, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 146
Source documentation
Full Walsh diagonalization, obtained by swapping the two finite averages.
```
theorem coefficient_cayleyAverage (g : D → Cube I) (f : Cube I → ℝ) (s : Cube I) :
    coefficient (cayleyAverage g f) s = eigenvalue g s * coefficient f s := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyAverage, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 164
Source documentation
Uniform finite port-word splitting multiplies the actual eigenvalues.
```
theorem eigenvalue_powerGenerators (g : D → Cube I) (n : Nat) (s : Cube I) :
    eigenvalue (powerGenerators g n) s = eigenvalue g s ^ n := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.powerGenerators
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.power_port_card line 190
Source documentation
The port degree of the powered graph is the exact number of port words.
```
theorem power_port_card (n : Nat) :
    Fintype.card (Fin n → D) = Fintype.card D ^ n := by
…
```
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.seven_power_port_card line 194
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 202
Source documentation
A bias bound on all nonconstant generator characters contracts the actual mean-zero function energy. The constant coefficient is eliminated by its exact identification with the mean, and every other coefficient is bounded termwise.
```
theorem cayley_energy_contraction (g : D → Cube I) (lambda : ℝ) (_hlambda : 0 ≤ lambda)
    (hbias : ∀ s : Cube I, s ≠ zeroFrequency → |eigenvalue g s| ≤ lambda)
    (f : Cube I → ℝ) (hmean : (𝔼 x, f x) = 0) :
    (𝔼 x, cayleyAverage g f x ^ 2) ≤ lambda ^ 2 * (𝔼 x, f x ^ 2) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.zeroFrequency, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyAverage
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 236
Source documentation
The Fourier proof supplies the graph certificate used in return bounds.
```
theorem cayley_spectralCertificate (g : D → Cube I) (lambda : ℝ)
    (hlambda : 0 ≤ lambda) (hlambdaone : lambda < 1)
    (hbias : ∀ s : Cube I, s ≠ zeroFrequency → |eigenvalue g s| ≤ lambda) :
    SpectralReturn.SpectralCertificate (cayleyGraph g) lambda where
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.zeroFrequency, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyGraph
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 247
theorem OAI.MaxCutGames.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 259
Source documentation
Seven actual generator steps turn one-half character bias into 2⁻⁷.
```
theorem sevenStep_halfCertificate (g : D → Cube I)
    (hbias : ∀ s : Cube I, s ≠ zeroFrequency → |eigenvalue g s| ≤ (1 / 2 : ℝ)) :
    SpectralReturn.SpectralCertificate (cayleyGraph (powerGenerators g 7))
      ((1 / 2 : ℝ) ^ 7) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.CayleySpectral.zeroFrequency, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.eigenvalue, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.cayleyGraph, OAI.MaxCutGames.Foundations.PCP.CayleySpectral.powerGenerators
abbrev OAI.MaxCutGames.Foundations.PCP.Expanders.Generators line 293
def OAI.MaxCutGames.Foundations.PCP.Expanders.badFrequency line 296
Source documentation
The zero character is excluded from the bad-event count.
```
def badFrequency {n m : Nat} (g : Generators n m) (s : Cube (Fin n)) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.Expanders.Generators
def OAI.MaxCutGames.Foundations.PCP.Expanders.badMass line 300
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.badFrequency_nonnegative line 303
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.mean_badFrequency_le line 308
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.mean_badMass_le line 320
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.exists_generators line 335
Source documentation
Actual finite generators with a simultaneous bound for every nonconstant Walsh character. The proof selects a point with bad-event count less than one.
```
theorem exists_generators (n m : Nat) (hm : 3 * (n + 2) ≤ m) :
    ∃ g : Generators n m, ∀ s : Cube (Fin n),
      s ≠ zeroFrequency → |eigenvalue g s| ≤ (1 / 2 : ℝ) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.Expanders.Generators
def OAI.MaxCutGames.Foundations.PCP.Expanders.baseDimension line 356
def OAI.MaxCutGames.Foundations.PCP.Expanders.initialDegree line 357
def OAI.MaxCutGames.Foundations.PCP.Expanders.initialQuarterDegree line 358
def OAI.MaxCutGames.Foundations.PCP.Expanders.basePower line 359
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.base_arithmetic line 361
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.exists_initial_generators line 373
abbrev OAI.MaxCutGames.Foundations.PCP.Expanders.BaseVertex line 379
abbrev OAI.MaxCutGames.Foundations.PCP.Expanders.BasePort line 380
def OAI.MaxCutGames.Foundations.PCP.Expanders.baseDegree line 381
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.card_basePort line 383
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.card_baseVertex line 388
theorem OAI.MaxCutGames.Foundations.PCP.Expanders.exists_baseGraph line 395
Source documentation
A genuine finite regular graph with the exact degree/size relation needed for zigzag. Its spectral certificate follows from the actual generator witness.
```
theorem exists_baseGraph :
    ∃ H : PoweringWalks.PortGraph BaseVertex BasePort,
      SpectralReturn.SpectralCertificate H (1 / 100 : ℝ) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringWalks.PortGraph, OAI.MaxCutGames.Foundations.PCP.Expanders.BaseVertex, OAI.MaxCutGames.Foundations.PCP.Expanders.BasePort, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.SpectralCertificate
def OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex line 419
theorem OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex_rot line 431
theorem OAI.MaxCutGames.Foundations.PCP.GraphTransport.operator_reindex line 440
theorem OAI.MaxCutGames.Foundations.PCP.GraphTransport.energy_reindex line 449
theorem OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex_spectralCertificate line 455
Source documentation
A coordinate change preserves the actual spectral certificate, including the uniform measure on the port alphabet.
```
theorem reindex_spectralCertificate (G : PortGraph V D) (vertices : V ≃ W)
    (ports : D ≃ E) (lambda : ℝ) (certificate : SpectralCertificate G lambda) :
    SpectralCertificate (reindex G vertices ports) lambda where
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.involutionEquiv line 491
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 498

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.MaxCutGames.Foundations.PCP.ZigzagGraphs.squareFirst line 506
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 510
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.squareSwap line 516
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 518
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.square line 523
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.square_rot_apply line 531
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.square_next line 537
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.cloudFirst line 541
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 546
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.crossCloud line 554
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 557
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.zigzag line 564
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 572
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 580
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 583
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 587
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 590
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 593
def OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.cloudOperator line 603
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.graphPermutation line 607
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.MaxCutGames.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 611
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.MaxCutGames.Foundations.PCP.SpectralReturn.averagingOperator, OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.square
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 622
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.MaxCutGames.Foundations.PCP.SpectralReturn.averagingOperator, OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.zigzag, OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.cloudOperator, OAI.MaxCutGames.Foundations.PCP.ZigzagGraphs.graphPermutation
def OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudMean line 656
def OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.liftCloud line 659
def OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.projection line 661
def OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.centered line 664
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.mean_liftCloud line 666
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.energy_liftCloud line 672
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.mean_cloudMean line 676
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.energy_prod line 679
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudMean_centered_zero line 683
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.energy_centered_eq_sub line 689
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.projection_energy_decomposition line 712
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.energy_projection_le line 717
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.energy_centered_le line 723
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.mean_sq_le_energy line 729
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.MaxCutGames.Foundations.PCP.ZigzagSpectral.averaging_energy_le line 735

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.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_add line 744
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_sub line 749
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_projection line 754
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_centered line 760
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.graphPermutation_energy line 766
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloud_energy_le line 770
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloud_centered_contraction line 780
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloud_residual_bound line 792
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.projection_graphPermutation_projection line 803
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.MaxCutGames.Foundations.PCP.ZigzagSpectral.projection, OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.liftCloud, OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.cloudMean
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.projected_outer_bound line 808
theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.energy_add_three_le line 822

theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.zigzag_energy_bound line 835

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.MaxCutGames.Foundations.PCP.ZigzagSpectral.square_certificate line 887

theorem OAI.MaxCutGames.Foundations.PCP.ZigzagSpectral.square_zigzag_halfCertificate line 907

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
…