DimensionSelection.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Logical dimension is chosen after the inverse density and row bound, and before the tuple length. All row maps, including deficient-rank maps, satisfy the resulting small trivial-character bound.

theorem OAI.MaxCutGames.Decoder.DimensionSelection.exists_logical_dimension line 14
theorem OAI.MaxCutGames.Decoder.DimensionSelection.kernel_fraction_le line 39
Source documentation
Uniform choice of ell bounds the trivial character fraction for every possible public row map without conditioning on its rank.
```
theorem kernel_fraction_le {ell r : ℕ}
    (A : (Fin ell → ZMod 2) →ₗ[ZMod 2] (Fin r → ZMod 2)) [Fintype A.ker] :
    1 / (Fintype.card A.ker : ℝ) ≤ 1 / (2 : ℝ) ^ (ell - r) := by
…
```
theorem OAI.MaxCutGames.Decoder.DimensionSelection.kernel_fraction_lt line 48
def OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw line 77
Source documentation
The real pushforward of the uniform law on sampler outcomes.
```
def samplerLaw (noise : Noise → V) (v : V) : ℝ := by
…
```
theorem OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw_nonneg line 82
theorem OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw_eq_count line 93
Source documentation
Literal counting formula; multiple sampler outcomes mapping to the same vector retain their multiplicity.
```
theorem samplerLaw_eq_count (noise : Noise → V) (v : V) :
    samplerLaw noise v =
      ((Finset.univ.filter fun n => noise n = v).card : ℝ) / Fintype.card Noise := by
…
```
Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw
theorem OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw_sum line 101
theorem OAI.MaxCutGames.Decoder.NoiseSampler.sample_expect_eq line 112
Source documentation
Exact pushforward expectation, with the uniform normalization explicit.
```
theorem sample_expect_eq (noise : Noise → V) (f : V → ℝ) :
    (𝔼 n, f (noise n)) = ∑ v, samplerLaw noise v * f v := by
…
```
Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw
theorem OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw_normalized line 116
theorem OAI.MaxCutGames.Decoder.NoiseSampler.rat_expect_cast line 121
theorem OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw_eq_rat_count line 126
theorem OAI.MaxCutGames.Decoder.NoiseSampler.sample_kernel_eq_eigenvalue line 140
Source documentation
The actual matrix multiplier is precisely the sampler's kernel event.
```
theorem sample_kernel_eq_eigenvalue (noise : Noise → V) (S : V →ₗ[F2] E) :
    (𝔼 n, if S (noise n) = 0 then (1 : ℝ) else 0) =
      linearNoiseEigenvalue (samplerLaw noise) S := by
…
```
Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw
theorem OAI.MaxCutGames.Decoder.NoiseSampler.detection_add_eigenvalue line 147
Source documentation
Detection plus annihilation is one for the same unconditional sampler.
```
theorem detection_add_eigenvalue [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E) :
    (𝔼 n, if S (noise n) ≠ 0 then (1 : ℝ) else 0) +
      linearNoiseEigenvalue (samplerLaw noise) S = 1 := by
…
```
Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw

theorem OAI.MaxCutGames.Decoder.NoiseSampler.detection_eigenvalue_le line 161

Source documentation

The constant-detection input becomes the 7/8 multiplier bound.

theorem detection_eigenvalue_le [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E)
    (hdetect : (1 : ℝ) / 8 ≤ 𝔼 n, if S (noise n) ≠ 0 then (1 : ℝ) else 0) :
    linearNoiseEigenvalue (samplerLaw noise) S ≤ 7 / 8 := by
…

Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw

theorem OAI.MaxCutGames.Decoder.NoiseSampler.detection_eigenvalue_le_complement line 169

Source documentation

The generic detection level is also retained for future parameter changes.

theorem detection_eigenvalue_le_complement [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E) (d : ℝ)
    (hdetect : d ≤ 𝔼 n, if S (noise n) ≠ 0 then (1 : ℝ) else 0) :
    linearNoiseEigenvalue (samplerLaw noise) S ≤ 1 - d := by
…

Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw

theorem OAI.MaxCutGames.Decoder.NoiseSampler.rational_detection_eigenvalue_le line 177

Source documentation

The gadget may keep its finite probabilities rational throughout.

theorem rational_detection_eigenvalue_le [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E)
    (hdetect : (1 : ℚ) / 8 ≤ 𝔼 n, if S (noise n) ≠ 0 then (1 : ℚ) else 0) :
    linearNoiseEigenvalue (samplerLaw noise) S ≤ 7 / 8 := by
…

Mentions: OAI.MaxCutGames.Decoder.NoiseSampler.samplerLaw