BlockTrace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The binary trace annihilator of a quadratic-block hyperplane

The trace annihilator of the field hyperplane perpendicular to a nonzero vector is exactly its field line. Scaling test vectors first upgrades binary trace orthogonality to field-valued orthogonality; explicit coordinate test vectors then identify the annihilator. No earlier gadget result is used.

theorem OAI.UniqueGamesTheorem.Quadratic.dot_sub_right line 21
theorem OAI.UniqueGamesTheorem.Quadratic.dot_single line 26
theorem OAI.UniqueGamesTheorem.Quadratic.annihilator_hyperplane_iff_mem_line line 32
Source documentation
The field-valued annihilator of a nonzero vector's perpendicular hyperplane is the line generated by that vector.
```
theorem annihilator_hyperplane_iff_mem_line {v z : Vec F} (hv : v ≠ 0) :
    (∀ y ∈ hyperplane v, dot z y = 0) ↔ z ∈ line v := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.hyperplane, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.line
theorem OAI.UniqueGamesTheorem.Quadratic.trace_annihilator_hyperplane_iff_mem_line line 62
Source documentation
Exact trace-annihilator identity for the field hyperplane. Trace nondegeneracy is provided by the proved finite-field trace pairing theorem.
```
theorem trace_annihilator_hyperplane_iff_mem_line {v z : Vec F} (hv : v ≠ 0) :
    (∀ y ∈ hyperplane v, traceBinary (dot z y) = 0) ↔ z ∈ line v := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.hyperplane, OAI.UniqueGamesTheorem.Quadratic.traceBinary, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.line
theorem OAI.UniqueGamesTheorem.Quadratic.trace_annihilator_hyperplane line 75
Source documentation
The same annihilator identity in set notation, using the actual trace.
```
theorem trace_annihilator_hyperplane (v : Vec F) (hv : v ≠ 0) :
    {z : Vec F | ∀ y ∈ hyperplane v, Algebra.trace (ZMod 2) F (dot z y) = 0} =
      (line v : Set (Vec F)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.hyperplane, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.line