OrientationVectors.lean`

98 declarations, 0 contain sorry, 0 declared as axioms

Fresh orientations of nonzero perturbations

This is the nonzero-symbol uniformity step in the latent-noise recurrence. The perturbation is fixed before the orientation, and zero is excluded from both sample spaces explicitly.

theorem OAI.MaxCutGames.Gadget.OrientationVectors.exists_equiv_map_nonzero line 25
Source documentation
Extend the isomorphism taking one specified nonzero vector to another.
```
theorem exists_equiv_map_nonzero (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ e : V ≃ₗ[K] V, e x = y := by
…
```
theorem OAI.MaxCutGames.Gadget.OrientationVectors.equiv_apply_ne_zero line 35
instance OAI.MaxCutGames.Gadget.OrientationVectors.nonzeroAction line 42
theorem OAI.MaxCutGames.Gadget.OrientationVectors.nonzero_transitive line 47

theorem OAI.MaxCutGames.Gadget.OrientationVectors.mean_oriented_nonzero line 54

Source documentation

A uniform ambient automorphism sends a fixed nonzero symbol uniformly onto all nonzero symbols.

theorem mean_oriented_nonzero [Fintype (V ≃ₗ[K] V)]
    [Fintype {x : V // x ≠ 0}] (x : {v : V // v ≠ 0})
    (f : {v : V // v ≠ 0} → ℚ) :
    (∑ a : V ≃ₗ[K] V, f (a • x)) / Fintype.card (V ≃ₗ[K] V) =
      (∑ y : {v : V // v ≠ 0}, f y) / Fintype.card {v : V // v ≠ 0} :=
…

theorem OAI.MaxCutGames.Gadget.OrientationVectors.mean_iso_nonzero line 63

Source documentation

The exact law used after fixing a child line and its nonzero output difference: averaging over all J : B ≃ₗ[K] U is uniform on U \ {0}.

theorem mean_iso_nonzero {B U : Type*} [AddCommGroup B] [Module K B]
    [AddCommGroup U] [Module K U] (J₀ : B ≃ₗ[K] U)
    [Fintype (B ≃ₗ[K] U)] [Fintype (U ≃ₗ[K] U)]
    [Fintype {u : U // u ≠ 0}] (b : B) (hb : b ≠ 0)
    (f : {u : U // u ≠ 0} → ℚ) :
    (∑ J : B ≃ₗ[K] U, f ⟨J b, equiv_apply_ne_zero J hb⟩) /
        Fintype.card (B ≃ₗ[K] U) =
      (∑ u : {u : U // u ≠ 0}, f u) / Fintype.card {u : U // u ≠ 0} := by
…

Mentions: OAI.MaxCutGames.Gadget.OrientationVectors.equiv_apply_ne_zero

abbrev OAI.MaxCutGames.Quadratic.Vec line 90
def OAI.MaxCutGames.Quadratic.Q line 95
Source documentation
The three-coordinate quadratic block from equation (2.4).
```
def Q (x : Vec F) : Vec F := ![x 1 * x 2, x 0 * x 2, x 0 * x 1]
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.D line 99
Source documentation
Its polar cross-terms. In characteristic two these equal Q (x + a) + Q x + Q a.
```
def D (x a : Vec F) : Vec F :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.dot line 104
Source documentation
Field dot product, with all three coordinates displayed.
```
def dot (v y : Vec F) : F := v 0 * y 0 + v 1 * y 1 + v 2 * y 2
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.Q_zero line 106
theorem OAI.MaxCutGames.Quadratic.Q_add line 110
theorem OAI.MaxCutGames.Quadratic.D_zero_left line 114
theorem OAI.MaxCutGames.Quadratic.D_zero_right line 118
theorem OAI.MaxCutGames.Quadratic.D_comm line 122
theorem OAI.MaxCutGames.Quadratic.D_add_left line 126
theorem OAI.MaxCutGames.Quadratic.D_add_right line 130
theorem OAI.MaxCutGames.Quadratic.D_smul_left line 133
theorem OAI.MaxCutGames.Quadratic.D_smul_right line 137
theorem OAI.MaxCutGames.Quadratic.dot_zero_right line 140
theorem OAI.MaxCutGames.Quadratic.dot_zero_left line 141
theorem OAI.MaxCutGames.Quadratic.dot_add_right line 143
theorem OAI.MaxCutGames.Quadratic.dot_smul_right line 147
theorem OAI.MaxCutGames.Quadratic.dot_smul_left line 151
def OAI.MaxCutGames.Quadratic.line line 156
Source documentation
The field line generated by v.
```
def line (v : Vec F) : Submodule F (Vec F) := Submodule.span F {v}
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.hyperplane line 159
Source documentation
The field hyperplane perpendicular to the generator of the line.
```
def hyperplane (v : Vec F) : Submodule F (Vec F) where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.mem_hyperplane line 169
theorem OAI.MaxCutGames.Quadratic.mem_line_iff line 171
theorem OAI.MaxCutGames.Quadratic.vec_add_self line 176
theorem OAI.MaxCutGames.Quadratic.D_eq_polar line 180
theorem OAI.MaxCutGames.Quadratic.cross_self_zero_inline_Block line 186
theorem OAI.MaxCutGames.Quadratic.D_smul_smul_zero line 193
Source documentation
The polar expression vanishes on any pair of vectors in the same field line.
```
theorem D_smul_smul_zero (v : Vec F) (t s : F) : D (t • v) (s • v) = 0 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.D
theorem OAI.MaxCutGames.Quadratic.dot_D_smul line 198
Source documentation
Every cross-term arising from a shift along Fv is perpendicular to v.
```
theorem dot_D_smul (v x : Vec F) (t : F) : dot v (D x (t • v)) = 0 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.dot, OAI.MaxCutGames.Quadratic.D
theorem OAI.MaxCutGames.Quadratic.D_mem_hyperplane line 207
theorem OAI.MaxCutGames.Quadratic.D_eq_zero_of_mem_line line 212
theorem OAI.MaxCutGames.Quadratic.Q_add_of_mem_line line 219
Source documentation
The restriction of the quadratic map to one field line is additive.
```
theorem Q_add_of_mem_line (v a b : Vec F)
    (ha : a ∈ line v) (hb : b ∈ line v) : Q (a + b) = Q a + Q b := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.line, OAI.MaxCutGames.Quadratic.Q
def OAI.MaxCutGames.Quadratic.U line 227
Source documentation
The block space U_A, as an actual binary submodule. Membership uses y + Q a because subtraction equals addition in characteristic two.
```
def U (v : Vec F) : Submodule (ZMod 2) (Vec F × Vec F) where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.mem_U line 248
theorem OAI.MaxCutGames.Quadratic.pair_mem_U line 251
theorem OAI.MaxCutGames.Quadratic.mem_U_iff_exists line 258
abbrev OAI.MaxCutGames.Quadratic.FieldLine line 279
Source documentation
Actual one-dimensional field directions, with proportional nonzero vectors identified.
```
abbrev FieldLine (F : Type*) [Field F] := Projectivization F (Vec F)
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.lineGenerator line 284
Source documentation
A chosen nonzero generator, only used with generator-independent data.
```
noncomputable def lineGenerator (A : FieldLine F) : Vec F := A.rep
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.lineGenerator_ne_zero line 286
theorem OAI.MaxCutGames.Quadratic.line_lineGenerator line 289
theorem OAI.MaxCutGames.Quadratic.fieldLine_finrank line 292
theorem OAI.MaxCutGames.Quadratic.card_FieldLine line 298
Source documentation
The denominator of the block erasure probability is exactly q²+q+1.
```
theorem card_FieldLine : Nat.card (FieldLine F) = Nat.card F ^ 2 + Nat.card F + 1 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine
theorem OAI.MaxCutGames.Quadratic.card_fieldLine_submodules line 305
Source documentation
The same count on one-dimensional submodules, rather than representatives.
```
theorem card_fieldLine_submodules :
    Nat.card {A : Submodule F (Vec F) // Module.finrank F A = 1} =
      Nat.card F ^ 2 + Nat.card F + 1 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.card_FieldLine_pos line 311
theorem OAI.MaxCutGames.Quadratic.reciprocal_card_FieldLine line 316
Source documentation
Written over rationals, as needed for the finite rational noise law.
```
theorem reciprocal_card_FieldLine :
    (Nat.card (FieldLine F) : ℚ)⁻¹ =
      ((Nat.card F : ℚ) ^ 2 + Nat.card F + 1)⁻¹ := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine
abbrev OAI.MaxCutGames.Quadratic.lineBinary line 330
abbrev OAI.MaxCutGames.Quadratic.hyperplaneBinary line 333
theorem OAI.MaxCutGames.Quadratic.Q_cancel_inline_BlockDimension line 337
def OAI.MaxCutGames.Quadratic.blockParametrization line 345
Source documentation
The parametrization (a,w) ↦ (a,Q(a)+w) is a binary-linear bijection. It is not asserted to be field-linear: squaring along a field line is only binary-linear.
```
def blockParametrization (v : Vec F) :
    (lineBinary v × hyperplaneBinary v) ≃ₗ[ZMod 2] U v where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.lineBinary, OAI.MaxCutGames.Quadratic.hyperplaneBinary, OAI.MaxCutGames.Quadratic.U
def OAI.MaxCutGames.Quadratic.dotLinear line 387
Source documentation
The dot-product functional over the large field.
```
def dotLinear (v : Vec F) : Vec F →ₗ[F] F where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.dotLinear_apply line 393
theorem OAI.MaxCutGames.Quadratic.dotLinear_ker line 396
theorem OAI.MaxCutGames.Quadratic.dotLinear_surjective line 399
theorem OAI.MaxCutGames.Quadratic.finrank_hyperplane line 418
theorem OAI.MaxCutGames.Quadratic.finrank_line line 427
theorem OAI.MaxCutGames.Quadratic.finrank_lineBinary line 434
theorem OAI.MaxCutGames.Quadratic.finrank_hyperplaneBinary line 440
theorem OAI.MaxCutGames.Quadratic.finrank_U line 448
Source documentation
If the field has binary dimension d, every nonzero-generator block has binary dimension 3d, the dimension of its input/output alphabet.
```
theorem finrank_U (v : Vec F) (hv : v ≠ 0) :
    Module.finrank (ZMod 2) (U v) = 3 * Module.finrank (ZMod 2) F := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
theorem OAI.MaxCutGames.Quadratic.finrank_U_eq_finrank_vec line 454
abbrev OAI.MaxCutGames.Quadratic.BlockOrientation line 466
Source documentation
An orientation identifies the common binary alphabet with a line's block.
```
abbrev BlockOrientation (A : FieldLine F) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine
instance OAI.MaxCutGames.Quadratic.fieldLineFintype line 469
instance OAI.MaxCutGames.Quadratic.finiteBlockOrientation line 471
instance OAI.MaxCutGames.Quadratic.blockOrientationFintype line 474
def OAI.MaxCutGames.Quadratic.chosenBlockOrientation line 478
Source documentation
Existence uses the proved dimension of the actual quadratic block.
```
noncomputable def chosenBlockOrientation (A : FieldLine F) : BlockOrientation A :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation
def OAI.MaxCutGames.Quadratic.blockOrientationEquiv line 484
Source documentation
Composing with one fixed orientation identifies all orientations with automorphisms of the common binary alphabet.
```
noncomputable def blockOrientationEquiv (A : FieldLine F) :
    BlockOrientation A ≃ (Vec F ≃ₗ[ZMod 2] Vec F) where
…
```
Mentions: OAI.MaxCutGames.Quadratic.FieldLine, OAI.MaxCutGames.Quadratic.BlockOrientation, OAI.MaxCutGames.Quadratic.Vec
theorem OAI.MaxCutGames.Quadratic.card_blockOrientation line 497
theorem OAI.MaxCutGames.Quadratic.card_blockOrientation_eq line 501
theorem OAI.MaxCutGames.Quadratic.card_blockOrientation_pos line 505
abbrev OAI.MaxCutGames.Quadratic.BlockOrientationIndex line 510
def OAI.MaxCutGames.Quadratic.blockOrientationIndexEquiv line 513
theorem OAI.MaxCutGames.Quadratic.card_blockOrientationIndex line 524
def OAI.MaxCutGames.Quadratic.blockObservable line 544
Source documentation
The block's nonlinear observable.
```
def blockObservable (p : Vec F × Vec F) : Vec F := p.2 + Q p.1
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.Q
theorem OAI.MaxCutGames.Quadratic.blockObservable_difference line 547
theorem OAI.MaxCutGames.Quadratic.blockObservable_difference_parametrized line 558
def OAI.MaxCutGames.Quadratic.hyperplaneNoiseShift line 566
Source documentation
Translation by the polar term permutes the vertical hyperplane.
```
def hyperplaneNoiseShift (v x a : Vec F) (ha : a ∈ line v) :
    hyperplane v ≃ hyperplane v where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.line, OAI.MaxCutGames.Quadratic.hyperplane
def OAI.MaxCutGames.Quadratic.noiseParameterShift line 582
Source documentation
The polar shear preserves the first coordinate and is its own inverse.
```
def noiseParameterShift (v x : Vec F) :
    (lineBinary v × hyperplaneBinary v) ≃ (lineBinary v × hyperplaneBinary v) where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.lineBinary, OAI.MaxCutGames.Quadratic.hyperplaneBinary
def OAI.MaxCutGames.Quadratic.blockNoiseCoordinates line 601
Source documentation
Coordinates in which the nonlinear output difference is just the second coordinate, for every fixed input x.
```
def blockNoiseCoordinates (v x : Vec F) : U v ≃ (lineBinary v × hyperplaneBinary v) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U, OAI.MaxCutGames.Quadratic.lineBinary, OAI.MaxCutGames.Quadratic.hyperplaneBinary
theorem OAI.MaxCutGames.Quadratic.blockObservable_difference_eq_noiseCoordinate line 604
theorem OAI.MaxCutGames.Quadratic.vec_add_eq_zero_iff_inline_BlockNoise line 611
theorem OAI.MaxCutGames.Quadratic.blockObservable_changes_iff line 619
theorem OAI.MaxCutGames.Quadratic.blockObservable_change_ne_zero line 630
def OAI.MaxCutGames.Quadratic.changedCoordinatesEquiv line 638
Source documentation
Changed perturbations correspond exactly to an arbitrary line coordinate and a nonzero hyperplane coordinate. In particular this is uniform in p.
```
def changedCoordinatesEquiv (v : Vec F) (p : Vec F × Vec F) :
    {u : U v // blockObservable (p + (u : Vec F × Vec F)) ≠ blockObservable p} ≃
      (lineBinary v × {w : hyperplaneBinary v // w ≠ 0}) :=
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U, OAI.MaxCutGames.Quadratic.blockObservable, OAI.MaxCutGames.Quadratic.lineBinary, OAI.MaxCutGames.Quadratic.hyperplaneBinary
theorem OAI.MaxCutGames.Quadratic.natCard_ne_zero_inline_BlockNoise line 651
theorem OAI.MaxCutGames.Quadratic.natCard_line line 658
theorem OAI.MaxCutGames.Quadratic.natCard_hyperplane line 662
theorem OAI.MaxCutGames.Quadratic.natCard_U line 666
theorem OAI.MaxCutGames.Quadratic.natCard_block_changes line 676
Source documentation
Exact numerator for the uniform nonzero-perturbation change probability. Zero never changes the observable, so no exclusion correction is needed.
```
theorem natCard_block_changes (v : Vec F) (hv : v ≠ 0) (p : Vec F × Vec F) :
    Nat.card {u : U v // blockObservable (p + (u : Vec F × Vec F)) ≠ blockObservable p} =
      Nat.card F * (Nat.card F ^ 2 - 1) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U, OAI.MaxCutGames.Quadratic.blockObservable
theorem OAI.MaxCutGames.Quadratic.natCard_nonzero_U line 684
Source documentation
Exact denominator when the perturbation is conditioned to be nonzero.
```
theorem natCard_nonzero_U (v : Vec F) (hv : v ≠ 0) :
    Nat.card {u : U v // u ≠ 0} = Nat.card F ^ 3 - 1 := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
theorem OAI.MaxCutGames.Quadratic.block_change_ratio line 689
Source documentation
The count ratio simplifies to the one-level survival factor 1-θ.
```
theorem block_change_ratio (q : ℚ) (hq : 1 < q) :
    q * (q ^ 2 - 1) / (q ^ 3 - 1) = 1 - 1 / (q ^ 2 + q + 1) := by
…
```
abbrev OAI.MaxCutGames.Quadratic.NonzeroBlock line 711
Source documentation
The uniform noise space after conditioning the perturbation to be nonzero.
```
abbrev NonzeroBlock (v : Vec F) := {u : U v // u ≠ 0}
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.U
def OAI.MaxCutGames.Quadratic.nonzeroBlockChangeProbability line 714
Source documentation
Exact uniform expectation of the nonlinear-change indicator.
```
def nonzeroBlockChangeProbability (v : Vec F) (p : Vec F × Vec F) : ℚ := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec
def OAI.MaxCutGames.Quadratic.conditionedChangedEquiv line 721
Source documentation
The zero perturbation is never a changed perturbation, so conditioning does not remove any element from the change event.
```
def conditionedChangedEquiv (v : Vec F) (p : Vec F × Vec F) :
    {u : NonzeroBlock v //
      blockObservable (p + (u.val : Vec F × Vec F)) ≠ blockObservable p} ≃
    {u : U v // blockObservable (p + (u : Vec F × Vec F)) ≠ blockObservable p} where
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.NonzeroBlock, OAI.MaxCutGames.Quadratic.blockObservable, OAI.MaxCutGames.Quadratic.U
theorem OAI.MaxCutGames.Quadratic.nonzeroBlockChangeProbability_eq_count line 730
theorem OAI.MaxCutGames.Quadratic.nonzeroBlockChangeProbability_eq line 748
Source documentation
The one-level change probability is exactly 1-θ, for every fixed input. Here θ = 1/(q²+q+1) and q is the actual finite-field cardinality.
```
theorem nonzeroBlockChangeProbability_eq (v : Vec F) (hv : v ≠ 0)
    (p : Vec F × Vec F) :
    nonzeroBlockChangeProbability v p =
      1 - 1 / ((Nat.card F : ℚ) ^ 2 + (Nat.card F : ℚ) + 1) := by
…
```
Mentions: OAI.MaxCutGames.Quadratic.Vec, OAI.MaxCutGames.Quadratic.nonzeroBlockChangeProbability