BlockDimension.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The binary-linear parametrization and dimension of the v2 quadratic block.

abbrev OAI.UniqueGamesTheorem.Quadratic.lineBinary line 19
abbrev OAI.UniqueGamesTheorem.Quadratic.hyperplaneBinary line 22
theorem OAI.UniqueGamesTheorem.Quadratic.Q_cancel line 26
def OAI.UniqueGamesTheorem.Quadratic.blockParametrization line 34
Source documentation
The parametrization (a,w) ↦ (a,Q(a)+w) is a binary-linear bijection. It is not asserted to be field-linear: squaring along a field line is only binary-linear.
```
def blockParametrization (v : Vec F) :
    (lineBinary v × hyperplaneBinary v) ≃ₗ[ZMod 2] U v where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.lineBinary, OAI.UniqueGamesTheorem.Quadratic.hyperplaneBinary, OAI.UniqueGamesTheorem.Quadratic.U
def OAI.UniqueGamesTheorem.Quadratic.dotLinear line 76
Source documentation
The dot-product functional over the large field.
```
def dotLinear (v : Vec F) : Vec F →ₗ[F] F where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.dotLinear_apply line 82
theorem OAI.UniqueGamesTheorem.Quadratic.dotLinear_ker line 85
theorem OAI.UniqueGamesTheorem.Quadratic.dotLinear_surjective line 88
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_hyperplane line 107
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_line line 116
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_lineBinary line 123
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_hyperplaneBinary line 129
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_U line 137
Source documentation
If the field has binary dimension d, every nonzero-generator block has binary dimension 3d, the dimension of its input/output alphabet.
```
theorem finrank_U (v : Vec F) (hv : v ≠ 0) :
    Module.finrank (ZMod 2) (U v) = 3 * Module.finrank (ZMod 2) F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_U_eq_finrank_vec line 143