OrientedRestrictionLemmas.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Orientation-independent character kernels

Changing the binary parametrization of a block only pulls its dual back along a linear equivalence. This leaves the logical kernel unchanged and places all child maps in one fixed dual space for the finite counting argument.

def OAI.UniqueGamesTheorem.Quadratic.orientedBlockRestriction line 26
Source documentation
The actual child restriction after a choice of block orientation.
```
def orientedBlockRestriction (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (v : Vec F) (J : B ≃ₗ[ZMod 2] U v) :
    S →ₗ[ZMod 2] (B →ₗ[ZMod 2] ZMod 2) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U
theorem OAI.UniqueGamesTheorem.Quadratic.orientedBlockRestriction_apply line 32
theorem OAI.UniqueGamesTheorem.Quadratic.orientedBlockRestriction_eq_zero_iff line 38
theorem OAI.UniqueGamesTheorem.Quadratic.ker_orientedBlockRestriction line 52
Source documentation
The kernel depends on the field line and common-parent lift, not on J.
```
theorem ker_orientedBlockRestriction
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    (v : Vec F) (J : B ≃ₗ[ZMod 2] U v) :
    (orientedBlockRestriction S g v J).ker = (blockRestriction S g v).ker := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U, OAI.UniqueGamesTheorem.Quadratic.orientedBlockRestriction, OAI.UniqueGamesTheorem.Quadratic.blockRestriction
theorem OAI.UniqueGamesTheorem.Quadratic.ker_orientedBlockRestriction_independent line 60
theorem OAI.UniqueGamesTheorem.Quadratic.mem_ker_orientedBlockRestriction_iff line 67
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_ker_orientedBlockRestriction_le_one line 77
def OAI.UniqueGamesTheorem.Quadratic.characterFieldLine line 112
Source documentation
A total projective-line map; the default is irrelevant on nonzero characters.
```
def characterFieldLine (A₀ : FieldLine F) (z : Vec F) : FieldLine F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.characterFieldLine_eq_of_mem line 117
def OAI.UniqueGamesTheorem.Quadratic.fieldLineRestrictions line 126
Source documentation
All maps have the same binary dual codomain, despite their different blocks.
```
def fieldLineRestrictions (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J : ∀ A : FieldLine F, BlockOrientation A) :
    FieldLine F → S →ₗ[ZMod 2] (Vec F →ₗ[ZMod 2] ZMod 2) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation
theorem OAI.UniqueGamesTheorem.Quadratic.alignedCharacters_eq_alignmentEvent line 132
Source documentation
The alignment event written with the displayed three-coordinate dot product.
```
theorem alignedCharacters_eq_alignmentEvent
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F) :
    alignedCharacters (fun z : S =>
      dot (g z) z = squareRoot (z.val 0 * z.val 1 * z.val 2)) =
      alignmentEvent (fun z : S => (z : Vec F)) g
        (fun z : S => alignmentRightHandSide (z : Vec F)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.alignedCharacters, OAI.UniqueGamesTheorem.Quadratic.dot, OAI.UniqueGamesTheorem.Quadratic.squareRoot, OAI.UniqueGamesTheorem.Quadratic.alignmentEvent, OAI.UniqueGamesTheorem.Quadratic.alignmentRightHandSide
theorem OAI.UniqueGamesTheorem.Quadratic.card_loss_fieldLineRestrictions_le line 145
Source documentation
The exact line-loss count, valid for every choice of orientations and every binary-linear lift, including one chosen adaptively from earlier information.
```
theorem card_loss_fieldLineRestrictions_le
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    (J : ∀ A : FieldLine F, BlockOrientation A) (hS : IsGeneric S)
    (A₀ : FieldLine F) :
    (lossIndices (fieldLineRestrictions S g J)).card ≤
      3 * Module.finrank (ZMod 2) S := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.lossIndices, OAI.UniqueGamesTheorem.Quadratic.fieldLineRestrictions
theorem OAI.UniqueGamesTheorem.Quadratic.card_loss_fieldLineRestrictions_le_three_rank line 164
Source documentation
The fallback line is only used to totalize the counting map.
```
theorem card_loss_fieldLineRestrictions_le_three_rank
    (S : Submodule (ZMod 2) (Vec F)) (g : S →ₗ[ZMod 2] Vec F)
    (J : ∀ A : FieldLine F, BlockOrientation A) (hS : IsGeneric S) :
    (lossIndices (fieldLineRestrictions S g J)).card ≤
      3 * Module.finrank (ZMod 2) S := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.lossIndices, OAI.UniqueGamesTheorem.Quadratic.fieldLineRestrictions