BlockKernelLemmas.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Character kernels on quadratic blocks

The character with horizontal coefficient g and vertical coefficient z annihilates the block attached to Fz precisely when the alignment equation holds. The predicate below is annihilation of the actual binary submodule, rather than an abstract replacement for that condition.

theorem OAI.UniqueGamesTheorem.Quadratic.dot_Q_smul line 27
Source documentation
A field-valued identity before applying the binary trace.
```
theorem dot_Q_smul (z : Vec F) (t : F) :
    dot z (Q (t • z)) = t ^ 2 * (z 0 * z 1 * z 2) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.Q
def OAI.UniqueGamesTheorem.Quadratic.blockCharacter line 39
Source documentation
The binary character with separate horizontal and vertical coefficients.
```
noncomputable def blockCharacter (g z : Vec F) (p : Vec F × Vec F) : ZMod 2 :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.BlockAnnihilates line 43
Source documentation
Literal annihilation of every vector in the block attached to v.
```
def BlockAnnihilates (g z v : Vec F) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.blockCharacter_on_quadratic line 47
theorem OAI.UniqueGamesTheorem.Quadratic.blockAnnihilates_self_iff line 53
Source documentation
The exact quadratic-block kernel criterion on the line of the character.
```
theorem blockAnnihilates_self_iff (g z : Vec F) :
    BlockAnnihilates g z z ↔ dot g z = squareRoot (z 0 * z 1 * z 2) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.BlockAnnihilates, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.squareRoot
theorem OAI.UniqueGamesTheorem.Quadratic.U_smul_ne_zero line 73
Source documentation
The binary block is independent of the nonzero generator of its field line.
```
theorem U_smul_ne_zero (v : Vec F) {t : F} (ht : t ≠ 0) : U (t • v) = U v := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U
theorem OAI.UniqueGamesTheorem.Quadratic.U_eq_of_nonzero_mem_line line 80
theorem OAI.UniqueGamesTheorem.Quadratic.mem_line_of_blockAnnihilates line 90
Source documentation
A character in a block's kernel has its vertical coefficient on that line.
```
theorem mem_line_of_blockAnnihilates {g z v : Vec F} (hv : v ≠ 0)
    (h : BlockAnnihilates g z v) : z ∈ line v := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.BlockAnnihilates, OAI.UniqueGamesTheorem.Quadratic.line
theorem OAI.UniqueGamesTheorem.Quadratic.blockAnnihilates_iff line 100
Source documentation
Full nonzero-character criterion, including the field-line condition.
```
theorem blockAnnihilates_iff {g z v : Vec F} (hv : v ≠ 0) (hz : z ≠ 0) :
    BlockAnnihilates g z v ↔
      z ∈ line v ∧ dot g z = squareRoot (z 0 * z 1 * z 2) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.BlockAnnihilates, OAI.UniqueGamesTheorem.Quadratic.line, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.squareRoot
def OAI.UniqueGamesTheorem.Quadratic.blockEmbedding line 129
def OAI.UniqueGamesTheorem.Quadratic.blockAggregate line 133
theorem OAI.UniqueGamesTheorem.Quadratic.blockAggregate_single line 136
theorem OAI.UniqueGamesTheorem.Quadratic.fieldLine_block_le_range_aggregate line 149
theorem OAI.UniqueGamesTheorem.Quadratic.blockAggregate_surjective line 164
Source documentation
All blocks occur in the actual pair-indexed aggregate. Their already proved span is the entire horizontal/vertical space, so the aggregate is surjective, as required by the recursive shift construction.
```
theorem blockAggregate_surjective : Function.Surjective (blockAggregate (F := F)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.blockAggregate
theorem OAI.UniqueGamesTheorem.Quadratic.aggregate_blockEmbedding_surjective line 180