BlockNoise.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Exact nonlinear change count for a quadratic block

For every fixed input, a shear of the line/hyperplane parametrization makes the output difference the hyperplane coordinate. This proves the uniform change count before any recursion or random orientation is introduced.

def OAI.UniqueGamesTheorem.Quadratic.blockObservable line 24
Source documentation
The block's nonlinear observable.
```
def blockObservable (p : Vec F × Vec F) : Vec F := p.2 + Q p.1
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.Q
theorem OAI.UniqueGamesTheorem.Quadratic.blockObservable_difference line 27
theorem OAI.UniqueGamesTheorem.Quadratic.blockObservable_difference_parametrized line 38
def OAI.UniqueGamesTheorem.Quadratic.hyperplaneNoiseShift line 46
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.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.line, OAI.UniqueGamesTheorem.Quadratic.hyperplane
def OAI.UniqueGamesTheorem.Quadratic.noiseParameterShift line 62
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.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.lineBinary, OAI.UniqueGamesTheorem.Quadratic.hyperplaneBinary
def OAI.UniqueGamesTheorem.Quadratic.blockNoiseCoordinates line 81
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.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U, OAI.UniqueGamesTheorem.Quadratic.lineBinary, OAI.UniqueGamesTheorem.Quadratic.hyperplaneBinary
theorem OAI.UniqueGamesTheorem.Quadratic.blockObservable_difference_eq_noiseCoordinate line 84
theorem OAI.UniqueGamesTheorem.Quadratic.vec_add_eq_zero_iff line 91
theorem OAI.UniqueGamesTheorem.Quadratic.blockObservable_changes_iff line 99
theorem OAI.UniqueGamesTheorem.Quadratic.blockObservable_change_ne_zero line 110
def OAI.UniqueGamesTheorem.Quadratic.changedCoordinatesEquiv line 118
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.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U, OAI.UniqueGamesTheorem.Quadratic.blockObservable, OAI.UniqueGamesTheorem.Quadratic.lineBinary, OAI.UniqueGamesTheorem.Quadratic.hyperplaneBinary
theorem OAI.UniqueGamesTheorem.Quadratic.natCard_ne_zero line 131
theorem OAI.UniqueGamesTheorem.Quadratic.natCard_line line 138
theorem OAI.UniqueGamesTheorem.Quadratic.natCard_hyperplane line 142
theorem OAI.UniqueGamesTheorem.Quadratic.natCard_U line 146
theorem OAI.UniqueGamesTheorem.Quadratic.natCard_block_changes line 156
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.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U, OAI.UniqueGamesTheorem.Quadratic.blockObservable
theorem OAI.UniqueGamesTheorem.Quadratic.natCard_nonzero_U line 164
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.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U
theorem OAI.UniqueGamesTheorem.Quadratic.block_change_ratio line 169
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
…
```