DimensionSelection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Logical dimension is chosen after the inverse density and row bound, and before the tuple length. All row maps, including deficient-rank maps, satisfy the resulting small trivial-character bound.

theorem OAI.UniqueGamesTheorem.Decoder.DimensionSelection.exists_logical_dimension line 19
theorem OAI.UniqueGamesTheorem.Decoder.DimensionSelection.kernel_fraction_le line 44
Source documentation
Uniform choice of ell bounds the trivial character fraction for every possible public row map without conditioning on its rank.
```
theorem kernel_fraction_le {ell r : ℕ}
    (A : (Fin ell → ZMod 2) →ₗ[ZMod 2] (Fin r → ZMod 2)) [Fintype A.ker] :
    1 / (Fintype.card A.ker : ℝ) ≤ 1 / (2 : ℝ) ^ (ell - r) := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.DimensionSelection.kernel_fraction_lt line 53