MatrixSubspaceCount.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Actual subspace cardinality bounds used in (5.12)--(5.13).

Every subspace is the image of a projection endomorphism. Thus the set of all subspaces is a quotient of the endomorphism space. The exact finite-field linear-map count is reused from Appendix.CompressionCount.

theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.endomorphism_range_surjective line 24
Source documentation
Taking the image of an endomorphism reaches every actual subspace.
```
theorem endomorphism_range_surjective :
    Function.Surjective (fun f : V →ₗ[K] V => LinearMap.range f) := by
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.card_subspaces_le_endomorphisms line 30
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.finite_color_space line 42
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.finite_endomorphisms line 46
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.finite_subspaces line 50
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.card_binary_subspaces_le line 54
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.card_binary_subspaces_le_of_finrank_le line 61
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.card_admissible_subspaces_le line 66
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.card_color_admissible_subspaces_le line 74
Source documentation
Counting fixed colors together with actual admissible subspaces gives precisely the q * 2^(s*s) denominator budget from (5.13).
```
theorem card_color_admissible_subspaces_le (P : Submodule F2 C → Prop) :
    Nat.card (C × {S : Submodule F2 C // P S}) ≤
      Nat.card C * 2 ^ (finrank F2 C * finrank F2 C) := by
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixSubspaceCount.card_color_admissible_subspaces_le_of_finrank_le line 80