TraceDual.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Trace coordinates for families of binary characters

The trace pairing identifies the binary dual of F³ with F³ itself. Its inverse is linear, so a common-parent family of binary functionals produces one binary-linear lift g, as required by the all-lifts genericity theorem.

theorem OAI.UniqueGamesTheorem.Quadratic.dot_add_first line 24
Also declared: OAI/Computability/UniqueGames/Quadratic/BlockRestriction.lean:24 (same declaration text).
def OAI.UniqueGamesTheorem.Quadratic.traceDotForm line 30
Source documentation
The trace dot product, as an actual binary bilinear form.
```
def traceDotForm : LinearMap.BilinForm (ZMod 2) (Vec F) where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.traceDotForm_apply line 59
theorem OAI.UniqueGamesTheorem.Quadratic.traceDotForm_nondegenerate line 63
Source documentation
Nondegeneracy holds coordinate by coordinate over the finite field.
```
theorem traceDotForm_nondegenerate :
    (traceDotForm (F := F)).Nondegenerate := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.traceDotForm
def OAI.UniqueGamesTheorem.Quadratic.traceDualEquiv line 84
Source documentation
The exact binary trace-pairing identification.
```
def traceDualEquiv : Vec F ≃ₗ[ZMod 2] (Vec F →ₗ[ZMod 2] ZMod 2) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.traceDualEquiv_apply line 87
theorem OAI.UniqueGamesTheorem.Quadratic.traceDualEquiv_symm_apply line 90
def OAI.UniqueGamesTheorem.Quadratic.representTraceFamily line 99
Source documentation
Taking trace coordinates preserves linear dependence on the family index.
```
def representTraceFamily (γ : W →ₗ[ZMod 2] (Vec F →ₗ[ZMod 2] ZMod 2)) :
    W →ₗ[ZMod 2] Vec F :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.representTraceFamily_spec line 103