OrientedBlockKernel.lean`

57 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.

def OAI.MaxCutGames.Gadget.OrientedBlockKernel.orientedBlockLinear line 20
Source documentation
The actual binary-linear embedding belonging to an oriented child.
```
def orientedBlockLinear (i : BlockOrientationIndex F) :
    Vec F →ₗ[ZMod 2] Vec F × Vec F :=
…
```
def OAI.MaxCutGames.Gadget.OrientedBlockKernel.orientedBlockChange line 25
Source documentation
The nonlinear-change indicator for the actual oriented quadratic block.
```
def orientedBlockChange (i : BlockOrientationIndex F) (p : Vec F × Vec F)
    (d : Vec F) : ℚ := by
…
```
theorem OAI.MaxCutGames.Gadget.OrientedBlockKernel.mean_orientations_change line 34
Source documentation
For one fixed field line, random orientation sends a fixed nonzero logical difference uniformly onto that line's nonzero block perturbations.
```
theorem mean_orientations_change (A : FieldLine F) (p : Vec F × Vec F)
    (d : Vec F) (hd : d ≠ 0) :
    (𝔼 J : BlockOrientation A, orientedBlockChange ⟨A, J⟩ p d) =
      1 - 1 / ((Nat.card F : ℚ) ^ 2 + (Nat.card F : ℚ) + 1) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.OrientedBlockKernel.orientedBlockChange
theorem OAI.MaxCutGames.Gadget.OrientedBlockKernel.mean_block_pairs line 54
Source documentation
Equal orientation-fiber sizes make the pair-index average exactly an independent uniform line followed by a uniform orientation of that line.
```
theorem mean_block_pairs (f : BlockOrientationIndex F → ℚ) :
    (𝔼 i : BlockOrientationIndex F, f i) =
      𝔼 A : FieldLine F, 𝔼 J : BlockOrientation A, f ⟨A, J⟩ := by
…
```
theorem OAI.MaxCutGames.Gadget.OrientedBlockKernel.mean_oriented_block_change line 74
Source documentation
Pointwise in the initial aggregate: the actual oriented-child average has the exact one-level nonlinear survival rate.
```
theorem mean_oriented_block_change (p : Vec F × Vec F) (d : Vec F) (hd : d ≠ 0) :
    (𝔼 i : BlockOrientationIndex F, orientedBlockChange i p d) =
      1 - 1 / ((Nat.card F : ℚ) ^ 2 + (Nat.card F : ℚ) + 1) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.OrientedBlockKernel.orientedBlockChange
theorem OAI.MaxCutGames.Gadget.OrientedBlockKernel.mean_oriented_block_kernel line 86
Source documentation
The averaged block kernel required by the parent-noise recurrence, now proved for the concrete quadratic construction.
```
theorem mean_oriented_block_kernel (d : Vec F) (hd : d ≠ 0) :
    (𝔼 i : BlockOrientationIndex F, 𝔼 p : Vec F × Vec F,
      orientedBlockChange i p d) =
      1 - 1 / ((Nat.card F : ℚ) ^ 2 + (Nat.card F : ℚ) + 1) := by
…
```
Mentions: OAI.MaxCutGames.Gadget.OrientedBlockKernel.orientedBlockChange
theorem OAI.MaxCutGames.Quadratic.squareMap_injective line 104
def OAI.MaxCutGames.Quadratic.squareRoot line 113
Source documentation
The unique square root, obtained by bijectivity of the finite square map.
```
noncomputable def squareRoot (c : F) : F :=
…
```
theorem OAI.MaxCutGames.Quadratic.squareRoot_sq line 116
theorem OAI.MaxCutGames.Quadratic.squareRoot_of_sq line 119
theorem OAI.MaxCutGames.Quadratic.squareRoot_unique line 123
abbrev OAI.MaxCutGames.Quadratic.traceBinary line 135
Source documentation
The field trace to the binary prime field.
```
noncomputable abbrev traceBinary : F →ₗ[ZMod 2] ZMod 2 := Algebra.trace (ZMod 2) F
…
```
theorem OAI.MaxCutGames.Quadratic.trace_square line 138
theorem OAI.MaxCutGames.Quadratic.trace_square_mul line 145
Source documentation
Moving a square from the first factor through the trace.
```
theorem trace_square_mul (t c : F) :
    traceBinary (t ^ 2 * c) = traceBinary (t * squareRoot c) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.traceBinary, OAI.MaxCutGames.Quadratic.squareRoot
theorem OAI.MaxCutGames.Quadratic.trace_mul_vanish_iff line 154
Source documentation
The trace pairing detects every nonzero field element.
```
theorem trace_mul_vanish_iff (a : F) :
    (∀ t : F, traceBinary (t * a) = 0) ↔ a = 0 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.traceBinary
theorem OAI.MaxCutGames.Quadratic.trace_quadratic_vanish_iff line 164
theorem OAI.MaxCutGames.Quadratic.dot_add_first_inline_TraceDual line 187
def OAI.MaxCutGames.Quadratic.traceDotForm line 193
Source documentation
The trace dot product, as an actual binary bilinear form.
```
def traceDotForm : LinearMap.BilinForm (ZMod 2) (Vec F) where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.traceDotForm_apply line 222
theorem OAI.MaxCutGames.Quadratic.traceDotForm_nondegenerate line 227
Source documentation
Nondegeneracy holds coordinate by coordinate over the finite field.
```
theorem traceDotForm_nondegenerate :
    (traceDotForm (F := F)).Nondegenerate := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.traceDotForm
def OAI.MaxCutGames.Quadratic.traceDualEquiv line 248
Source documentation
The exact binary trace-pairing identification.
```
def traceDualEquiv : Vec F ≃ₗ[ZMod 2] (Vec F →ₗ[ZMod 2] ZMod 2) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.traceDualEquiv_apply line 252
theorem OAI.MaxCutGames.Quadratic.traceDualEquiv_symm_apply line 256
def OAI.MaxCutGames.Quadratic.representTraceFamily line 265
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.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.representTraceFamily_spec line 270
theorem OAI.MaxCutGames.Quadratic.dot_sub_right_inline_BlockTrace line 290
theorem OAI.MaxCutGames.Quadratic.dot_single_inline_BlockTrace line 295
theorem OAI.MaxCutGames.Quadratic.annihilator_hyperplane_iff_mem_line line 301
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.hyperplane, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.line
theorem OAI.MaxCutGames.Quadratic.trace_annihilator_hyperplane_iff_mem_line line 332
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.hyperplane, OAI.MaxCutGames.Quadratic.traceBinary, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.line
theorem OAI.MaxCutGames.Quadratic.trace_annihilator_hyperplane line 346
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.hyperplane, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.line
theorem OAI.MaxCutGames.Quadratic.dot_Q_smul line 369
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.Q
def OAI.MaxCutGames.Quadratic.blockCharacter line 381
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.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.BlockAnnihilates line 385
Source documentation
Literal annihilation of every vector in the block attached to v.
```
def BlockAnnihilates (g z v : Vec F) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.blockCharacter_on_quadratic line 389
theorem OAI.MaxCutGames.Quadratic.blockAnnihilates_self_iff line 395
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.BlockAnnihilates, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.squareRoot
theorem OAI.MaxCutGames.Quadratic.U_smul_ne_zero line 415
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
theorem OAI.MaxCutGames.Quadratic.U_eq_of_nonzero_mem_line line 422
theorem OAI.MaxCutGames.Quadratic.mem_line_of_blockAnnihilates line 432
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.BlockAnnihilates, OAI.MaxCutGames.Quadratic.line
theorem OAI.MaxCutGames.Quadratic.blockAnnihilates_iff line 442
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.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.BlockAnnihilates, OAI.MaxCutGames.Quadratic.line, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.squareRoot
def OAI.MaxCutGames.Quadratic.alignmentMatrix line 469
Source documentation
The |n| * |ι| alignment columns for a fixed parametrization and input set. The input set is represented by any map point : E → V; no injectivity is needed for the exact algebraic equivalence.
```
def alignmentMatrix (b : Basis ι R V) (point : E → V) (z : V → n → F) :
    Matrix E (n × ι) F :=
…
```
theorem OAI.MaxCutGames.Quadratic.dot_lift_eq_alignment_mulVec line 476
Source documentation
Basis values of a linear lift give the coefficients of the alignment column combination. The identity holds for every lift, without selecting one in advance of the parametrization.
```
theorem dot_lift_eq_alignment_mulVec (b : Basis ι R V)
    (point : E → V) (z : V → n → F) (g : V →ₗ[R] (n → F)) (e : E) :
    (∑ i, z (point e) i * g (point e) i) =
      (alignmentMatrix b point z *ᵥ (fun ij => g (b ij.2) ij.1)) e := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.alignmentMatrix
theorem OAI.MaxCutGames.Quadratic.exists_lift_alignment_iff_mem_range line 499
Source documentation
Existence of any linear lift aligning on the chosen inputs is one column-membership event. In particular there is no field-size-dependent union bound over the possible lifts.
```
theorem exists_lift_alignment_iff_mem_range (b : Basis ι R V)
    (point : E → V) (z : V → n → F) (c : E → F) :
    (∃ g : V →ₗ[R] (n → F), ∀ e,
      (∑ i, z (point e) i * g (point e) i) = c e) ↔
      c ∈ LinearMap.range (alignmentMatrix b point z).mulVecLin := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.alignmentMatrix
theorem OAI.MaxCutGames.Quadratic.finrank_alignment_range_le line 524
Source documentation
The column-space dimension is at most the number of free basis values. For three field coordinates and a binary basis of size r, this is 3r.
```
theorem finrank_alignment_range_le (b : Basis ι R V)
    (point : E → V) (z : V → n → F) [Fintype E] :
    Module.finrank F (LinearMap.range (alignmentMatrix b point z).mulVecLin) ≤
      Fintype.card n * Fintype.card ι := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.alignmentMatrix
def OAI.MaxCutGames.Quadratic.alignmentEvent line 546
Source documentation
Nonzero inputs aligned by a specified linear lift.
```
def alignmentEvent (z : V → n → F) (g : V →ₗ[R] (n → F)) (c : V → F) :
    Finset V := by
…
```

theorem OAI.MaxCutGames.Quadratic.all_lifts_bound_iff_subsets line 553

Source documentation

Exact finite bad-set reduction. Its right hand side quantifies only over input sets, while column membership already accounts for every linear lift.

theorem all_lifts_bound_iff_subsets (b : Basis ι R V) (z : V → n → F)
    (c : V → F) (k : ℕ) :
    (∀ g : V →ₗ[R] (n → F), (alignmentEvent z g c).card ≤ k) ↔
      ∀ E : Finset V, 0 ∉ E → E.card = k + 1 →
        (fun e : E => c e) ∉
          LinearMap.range (alignmentMatrix b (fun e : E => (e : V)) z).mulVecLin := by
…

Mentions: OAI.MaxCutGames.Quadratic.alignmentEvent, OAI.MaxCutGames.Quadratic.alignmentMatrix

theorem OAI.MaxCutGames.Quadratic.all_lifts_bound_of_card_le line 586
def OAI.MaxCutGames.Quadratic.alignmentRightHandSide line 601
Source documentation
The cubic square-root right hand side of the alignment equation.
```
def alignmentRightHandSide (z : Fin 3 → F) : F := squareRoot (z 0 * z 1 * z 2)
```
Mentions: OAI.MaxCutGames.Quadratic.squareRoot
def OAI.MaxCutGames.Quadratic.IsGeneric line 605
Source documentation
The complete genericity predicate. The universal linear map quantifier occurs inside the property of the selected subspace.
```
def IsGeneric (S : Submodule (ZMod 2) (Fin 3 → F)) : Prop := by
…
```
theorem OAI.MaxCutGames.Quadratic.finrank_le_one_of_nonzero_unique line 633
Source documentation
A vector space with at most one nonzero vector has dimension at most one. The statement is deliberately independent of any characteristic assumption.
```
theorem finrank_le_one_of_nonzero_unique
    (h : ∀ v w : V, v ≠ 0 → w ≠ 0 → v = w) :
    Module.finrank R V ≤ 1 := by
…
```
theorem OAI.MaxCutGames.Quadratic.finrank_ker_le_one_of_nonzero_unique line 653
Source documentation
Nonproportionality of a generic character space makes every child kernel at most one-dimensional once the field-line kernel criterion is applied.
```
theorem finrank_ker_le_one_of_nonzero_unique (f : V →ₗ[R] W)
    (h : ∀ v w : V, v ≠ 0 → w ≠ 0 → f v = 0 → f w = 0 → v = w) :
    Module.finrank R f.ker ≤ 1 := by
…
```

theorem OAI.MaxCutGames.Quadratic.finrank_source_le_range_add_one line 670

Source documentation

Consequently the image rank can lose at most one dimension.

theorem finrank_source_le_range_add_one [FiniteDimensional R V]
    (f : V →ₗ[R] W)
    (h : ∀ v w : V, v ≠ 0 → w ≠ 0 → f v = 0 → f w = 0 → v = w) :
    Module.finrank R V ≤ Module.finrank R f.range + 1 := by
…

def OAI.MaxCutGames.Quadratic.lossIndices line 681
Source documentation
The actual finite event of a child map having a nonzero kernel.
```
def lossIndices (f : I → V →ₗ[R] W) : Finset I := by
…
```
def OAI.MaxCutGames.Quadratic.alignedCharacters line 685
theorem OAI.MaxCutGames.Quadratic.lossIndices_subset_image line 689

theorem OAI.MaxCutGames.Quadratic.card_lossIndices_le_card_aligned line 701

Source documentation

The cardinality bound does not union over lifts or orientations.

theorem card_lossIndices_le_card_aligned (f : I → V →ₗ[R] W)
    (aligned : V → Prop) (lineOf : V → I)
    (hkernel : ∀ i v, v ≠ 0 → f i v = 0 → aligned v ∧ lineOf v = i) :
    (lossIndices f).card ≤ (alignedCharacters aligned).card := by
…

Mentions: OAI.MaxCutGames.Quadratic.lossIndices, OAI.MaxCutGames.Quadratic.alignedCharacters

theorem OAI.MaxCutGames.Quadratic.card_lossIndices_le line 709
theorem OAI.MaxCutGames.Quadratic.card_lossIndices_le_nonzero line 716