GenericFieldChoice.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One field for every rank up to a fixed threshold

The extension degree is chosen using only the rank threshold and the requested genericity error. In particular it is fixed before the logical dimension in the later enlargement construction. A generic top-rank space exists in the same field.

instance OAI.UniqueGamesTheorem.Quadratic.binaryFieldFintype line 26
theorem OAI.UniqueGamesTheorem.Quadratic.exists_uniform_generic_field line 31
Source documentation
Simultaneous quantitative genericity, with the precise threshold order used by the latent gadget. The conclusion covers rank zero as well.
```
theorem exists_uniform_generic_field (r₀ : ℕ) (ε : ℚ) (hε : 0 < ε) :
    ∃ d : ℕ, 0 < d ∧ r₀ ≤ 3 * d ∧
      (∀ r : ℕ, r ≤ r₀ → nongenericFraction (BinaryField d) r ≤ ε) ∧
      (∃ S : RankSpace (ZMod 2) (Fin 3 → BinaryField d) r₀, IsGeneric S.1) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.nongenericFraction, OAI.UniqueGamesTheorem.Quadratic.BinaryField, OAI.UniqueGamesTheorem.Quadratic.IsGeneric