BlockRestriction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual child restriction maps

A common-parent lift g gives a binary linear map from its logical character space into the dual of each quadratic block. Its kernel is literal character annihilation, so the trace calculation and the all-lifts genericity predicate apply directly to this map.

theorem OAI.UniqueGamesTheorem.Quadratic.dot_add_first line 24
Also declared: OAI/Computability/UniqueGames/Quadratic/TraceDual.lean:24 (same declaration text).
def OAI.UniqueGamesTheorem.Quadratic.blockCharacterLinear line 30
Source documentation
The actual trace character as a binary linear functional.
```
def blockCharacterLinear (g z : Vec F) :
    (Vec F × Vec F) →ₗ[ZMod 2] ZMod 2 where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.blockRestriction line 46
Source documentation
Restriction to one block, linear in the logical character z.
```
def blockRestriction (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (v : Vec F) :
    S →ₗ[ZMod 2] ((U v) →ₗ[ZMod 2] ZMod 2) where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U
theorem OAI.UniqueGamesTheorem.Quadratic.blockRestriction_apply line 67
theorem OAI.UniqueGamesTheorem.Quadratic.blockRestriction_eq_zero_iff line 73
Source documentation
Equality to zero is exactly annihilation of the underlying block.
```
theorem blockRestriction_eq_zero_iff (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (v : Vec F) (z : S) :
    blockRestriction S g v z = 0 ↔ BlockAnnihilates (g z) z v := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.blockRestriction, OAI.UniqueGamesTheorem.Quadratic.BlockAnnihilates
theorem OAI.UniqueGamesTheorem.Quadratic.mem_ker_blockRestriction_iff line 84
Source documentation
The exact kernel formula for a nonzero logical character.
```
theorem mem_ker_blockRestriction_iff (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) {v : Vec F} (hv : v ≠ 0)
    {z : S} (hz : z ≠ 0) :
    z ∈ (blockRestriction S g v).ker ↔
      (z : Vec F) ∈ line v ∧
        dot (g z) z = squareRoot (z.val 0 * z.val 1 * z.val 2) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.blockRestriction, OAI.UniqueGamesTheorem.Quadratic.line, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.squareRoot
theorem OAI.UniqueGamesTheorem.Quadratic.blockRestriction_nonzero_kernel_unique line 95
Source documentation
Nonproportionality of a generic space makes every actual block kernel contain at most one nonzero character.
```
theorem blockRestriction_nonzero_kernel_unique
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    {v : Vec F} (hv : v ≠ 0) (hS : IsGeneric S)
    (z w : S) (hz : z ≠ 0) (hw : w ≠ 0)
    (hgz : blockRestriction S g v z = 0)
    (hgw : blockRestriction S g v w = 0) : z = w := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.blockRestriction
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_ker_blockRestriction_le_one line 117
Source documentation
Every actual child restriction map loses at most one binary dimension.
```
theorem finrank_ker_blockRestriction_le_one
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    {v : Vec F} (hv : v ≠ 0) (hS : IsGeneric S) :
    Module.finrank (ZMod 2) (blockRestriction S g v).ker ≤ 1 :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.blockRestriction
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_blockRestriction_source_le_range_add_one line 124