Block.lean`

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.UniqueGamesTheorem.Quadratic.Vec line 15
def OAI.UniqueGamesTheorem.Quadratic.Q line 20
Source documentation
The three-coordinate quadratic block from equation (2.4).
```
def Q (x : Vec F) : Vec F := ![x 1 * x 2, x 0 * x 2, x 0 * x 1]
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.D line 24
Source documentation
Its polar cross-terms. In characteristic two these equal Q (x + a) + Q x + Q a.
```
def D (x a : Vec F) : Vec F :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.dot line 29
Source documentation
Field dot product, with all three coordinates displayed.
```
def dot (v y : Vec F) : F := v 0 * y 0 + v 1 * y 1 + v 2 * y 2
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.Q_zero line 31
theorem OAI.UniqueGamesTheorem.Quadratic.Q_add line 35
theorem OAI.UniqueGamesTheorem.Quadratic.D_zero_left line 39
theorem OAI.UniqueGamesTheorem.Quadratic.D_zero_right line 43
theorem OAI.UniqueGamesTheorem.Quadratic.D_comm line 47
theorem OAI.UniqueGamesTheorem.Quadratic.D_add_left line 51
theorem OAI.UniqueGamesTheorem.Quadratic.D_add_right line 55
theorem OAI.UniqueGamesTheorem.Quadratic.D_smul_left line 58
theorem OAI.UniqueGamesTheorem.Quadratic.D_smul_right line 62
theorem OAI.UniqueGamesTheorem.Quadratic.dot_zero_right line 65
theorem OAI.UniqueGamesTheorem.Quadratic.dot_zero_left line 66
theorem OAI.UniqueGamesTheorem.Quadratic.dot_add_right line 68
theorem OAI.UniqueGamesTheorem.Quadratic.dot_smul_right line 72
theorem OAI.UniqueGamesTheorem.Quadratic.dot_smul_left line 76
def OAI.UniqueGamesTheorem.Quadratic.line line 81
Source documentation
The field line generated by v.
```
def line (v : Vec F) : Submodule F (Vec F) := Submodule.span F {v}
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.hyperplane line 84
Source documentation
The field hyperplane perpendicular to the generator of the line.
```
def hyperplane (v : Vec F) : Submodule F (Vec F) where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.mem_hyperplane line 94
theorem OAI.UniqueGamesTheorem.Quadratic.mem_line_iff line 96
theorem OAI.UniqueGamesTheorem.Quadratic.vec_add_self line 103
theorem OAI.UniqueGamesTheorem.Quadratic.D_eq_polar line 107
theorem OAI.UniqueGamesTheorem.Quadratic.cross_self_zero line 113
theorem OAI.UniqueGamesTheorem.Quadratic.D_smul_smul_zero line 120
Source documentation
The polar expression vanishes on any pair of vectors in the same field line.
```
theorem D_smul_smul_zero (v : Vec F) (t s : F) : D (t • v) (s • v) = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.D
theorem OAI.UniqueGamesTheorem.Quadratic.dot_D_smul line 125
Source documentation
Every cross-term arising from a shift along Fv is perpendicular to v.
```
theorem dot_D_smul (v x : Vec F) (t : F) : dot v (D x (t • v)) = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.D
theorem OAI.UniqueGamesTheorem.Quadratic.D_mem_hyperplane line 134
theorem OAI.UniqueGamesTheorem.Quadratic.D_eq_zero_of_mem_line line 139
theorem OAI.UniqueGamesTheorem.Quadratic.Q_add_of_mem_line line 146
Source documentation
The restriction of the quadratic map to one field line is additive.
```
theorem Q_add_of_mem_line (v a b : Vec F)
    (ha : a ∈ line v) (hb : b ∈ line v) : Q (a + b) = Q a + Q b := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.line, OAI.UniqueGamesTheorem.Quadratic.Q
def OAI.UniqueGamesTheorem.Quadratic.U line 154
Source documentation
The block space U_A, as an actual binary submodule. Membership uses y + Q a because subtraction equals addition in characteristic two.
```
def U (v : Vec F) : Submodule (ZMod 2) (Vec F × Vec F) where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.mem_U line 175
theorem OAI.UniqueGamesTheorem.Quadratic.pair_mem_U line 178
theorem OAI.UniqueGamesTheorem.Quadratic.mem_U_iff_exists line 185