MatrixParity.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Actual binary matrix and linear-map parity used in Lemma 5.3.

theorem OAI.MaxCutGames.Fourier.MatrixParity.trace_rankOne line 17
Source documentation
The rank-one shift c τ paired against S evaluates the functional τ S at c, exactly the parity appearing in the decoding condition.
```
theorem trace_rankOne {m n : Nat} (c : Vector n) (τ : Vector m)
    (S : Matrix (Fin m) (Fin n) F2) :
    Matrix.trace (Matrix.vecMulVec c τ * S) = τ ⬝ᵥ (S *ᵥ c) := by
…
```
def OAI.MaxCutGames.Fourier.MatrixParity.MatrixValid line 24
Source documentation
Coordinate form of the requirement τ ∘ T ≠ 0.
```
def MatrixValid {m n : Nat} (τ : Vector m) (S : Matrix (Fin m) (Fin n) F2) : Prop :=
…
```
theorem OAI.MaxCutGames.Fourier.MatrixParity.matrixValid_iff_exists line 27
theorem OAI.MaxCutGames.Fourier.MatrixParity.exists_matrixValid line 45

theorem OAI.MaxCutGames.Fourier.MatrixParity.comp_ne_zero_iff_exists line 65

Source documentation

Abstract linear-map form of the nonzero-parity condition.

theorem comp_ne_zero_iff_exists {E C : Type*}
    [AddCommGroup E] [Module F2 E] [AddCommGroup C] [Module F2 C]
    (τ : E →ₗ[F2] F2) (T : C →ₗ[F2] E) :
    τ.comp T ≠ 0 ↔ ∃ c, τ (T c) = 1 := by
…

def OAI.MaxCutGames.Fourier.MatrixParity.Valid line 89
theorem OAI.MaxCutGames.Fourier.MatrixParity.valid_iff_exists line 91
theorem OAI.MaxCutGames.Fourier.MatrixParity.exists_valid line 96
Source documentation
Any nonzero parity functional admits a parity-valid map out of a nontrivial binary vector space. This also proves the candidate family is nonempty.
```
theorem exists_valid [Nontrivial C] (τ : E →ₗ[F2] F2) (hτ : τ ≠ 0) :
    ∃ S : C →ₗ[F2] E, Valid τ S := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixParity.Valid

theorem OAI.MaxCutGames.Fourier.MatrixParity.trace_smulRight_comp line 113

Source documentation

Generic trace pairing of a rank-one color shift.

theorem trace_smulRight_comp [FiniteDimensional F2 C]
    (τ : E →ₗ[F2] F2) (c : C) (S : C →ₗ[F2] E) :
    LinearMap.trace F2 C ((τ.smulRight c).comp S) = τ (S c) := by
…

theorem OAI.MaxCutGames.Fourier.MatrixParity.card_linearMaps line 123
Source documentation
The exact number of binary linear maps, supplying the count in (5.20). Taking E to be the subspace W counts precisely maps whose image lies in W.
```
theorem card_linearMaps [FiniteDimensional F2 E] [FiniteDimensional F2 C]
    [Fintype (C →ₗ[F2] E)] :
    Fintype.card (C →ₗ[F2] E) =
      2 ^ (Module.finrank F2 C * Module.finrank F2 E) := by
…
```
theorem OAI.MaxCutGames.Fourier.MatrixParity.card_linearMaps_le line 137

theorem OAI.MaxCutGames.Fourier.MatrixParity.folded_indicator_sum_le_one line 157

Source documentation

A folded map hits a fixed color at most once along its C-shift orbit. The injection models the inclusion of the subspace C' in the full color space.

theorem folded_indicator_sum_le_one (τ : E →ₗ[F2] F2)
    (inclusion : C →ₗ[F2] D) (inclusion_injective : Function.Injective inclusion)
    (F : (E →ₗ[F2] C) → D)
    (folded : ∀ X c, F (X + τ.smulRight c) = F X + inclusion c)
    (X : E →ₗ[F2] C) (y : D) :
    (∑ c : C, if F (X + τ.smulRight c) = y then (1 : ℝ) else 0) ≤ 1 := by
…

theorem OAI.MaxCutGames.Fourier.MatrixParity.folded_indicator_average_le line 180

Source documentation

Equation (5.19)'s first bound, with the actual finite folded shift average.

theorem folded_indicator_average_le (τ : E →ₗ[F2] F2)
    (inclusion : C →ₗ[F2] D) (inclusion_injective : Function.Injective inclusion)
    (F : (E →ₗ[F2] C) → D)
    (folded : ∀ X c, F (X + τ.smulRight c) = F X + inclusion c)
    (X : E →ₗ[F2] C) (y : D) :
    (∑ c : C, if F (X + τ.smulRight c) = y then (1 : ℝ) else 0) /
        Fintype.card C ≤ 1 / (Fintype.card C : ℝ) := by
…

def OAI.MaxCutGames.Fourier.MatrixParity.parityCharacter line 199
Source documentation
The character of the color-shift group indexed by the functional τ S.
```
def parityCharacter (τ : E →ₗ[F2] F2) (S : C →ₗ[F2] E) : AddChar C ℂ where
…
```
theorem OAI.MaxCutGames.Fourier.MatrixParity.parityCharacter_eq_zero_iff line 204

theorem OAI.MaxCutGames.Fourier.MatrixParity.linearTrace_shift_sum line 219

Source documentation

Unnormalized annihilator identity for exactly the c τ shift subgroup.

theorem linearTrace_shift_sum [Fintype C] [FiniteDimensional F2 C]
    (τ : E →ₗ[F2] F2) (S : C →ₗ[F2] E) :
    (∑ c : C, linearTraceCharacter S (τ.smulRight c)) =
      if τ.comp S = 0 then (Fintype.card C : ℂ) else 0 := by
…

theorem OAI.MaxCutGames.Fourier.MatrixParity.linearTrace_shift_average line 231

Source documentation

Averaging the Fourier character in the folding directions kills precisely the indices with nonzero τ S, the multiplier used in Equation (5.19).

theorem linearTrace_shift_average [Fintype C] [FiniteDimensional F2 C]
    (τ : E →ₗ[F2] F2) (S : C →ₗ[F2] E) :
    (∑ c : C, linearTraceCharacter S (τ.smulRight c)) / (Fintype.card C : ℂ) =
      if τ.comp S = 0 then 1 else 0 := by
…