OrientedBlockKernel.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Gadget.OrientedBlockKernel.orientedBlockLinear line 19
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.UniqueGamesTheorem.Gadget.OrientedBlockKernel.orientedBlockChange line 24
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.UniqueGamesTheorem.Gadget.OrientedBlockKernel.mean_orientations_change line 33
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.UniqueGamesTheorem.Gadget.OrientedBlockKernel.orientedBlockChange
theorem OAI.UniqueGamesTheorem.Gadget.OrientedBlockKernel.mean_block_pairs line 53
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.UniqueGamesTheorem.Gadget.OrientedBlockKernel.mean_oriented_block_change line 73
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.UniqueGamesTheorem.Gadget.OrientedBlockKernel.orientedBlockChange
theorem OAI.UniqueGamesTheorem.Gadget.OrientedBlockKernel.mean_oriented_block_kernel line 85
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.UniqueGamesTheorem.Gadget.OrientedBlockKernel.orientedBlockChange