OAI/Computability/UniqueGames/Gadgets/ConcatenationLemmas.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Gadget.aggregate line 41

   Source documentation

   Sum of the oriented block inclusions on the child logical symbols.

   def aggregate (J : I → B →ₗ[k] X × B) : (I → B) →ₗ[k] X × B where
   …

2. def OAI.UniqueGamesTheorem.Gadget.shiftAggregate line 47

   Source documentation

   The same aggregate, evaluated on actual child shifts.

   def shiftAggregate (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B) :
       (I → R) →ₗ[k] X × B where
   …

3. def OAI.UniqueGamesTheorem.Gadget.parentShifts line 55

   Source documentation

   The parent shift space: precisely the child shifts with zero first aggregate coordinate.

   def parentShifts (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B) :
       Submodule k (I → R) :=
   …

4. def OAI.UniqueGamesTheorem.Gadget.parentLogical line 60

   Source documentation

   Parent logical translation, the second aggregate coordinate.

   def parentLogical (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B) :
       parentShifts J lam →ₗ[k] B :=
   …

   Mentions: OAI.UniqueGamesTheorem.Gadget.parentShifts

5. def OAI.UniqueGamesTheorem.Gadget.parentEmbed line 66

   Source documentation

   Embedding parent shifts in the actual product of child input spaces.

   def parentEmbed (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B)
       (e : R →ₗ[k] P) : parentShifts J lam →ₗ[k] (I → P) where
   …

   Mentions: OAI.UniqueGamesTheorem.Gadget.parentShifts

6. theorem OAI.UniqueGamesTheorem.Gadget.parentEmbed_injective line 72
7. theorem OAI.UniqueGamesTheorem.Gadget.shiftAggregate_surjective line 80
8. theorem OAI.UniqueGamesTheorem.Gadget.parentLogical_surjective line 92
9. def OAI.UniqueGamesTheorem.Gadget.parentOutput line 104
10. theorem OAI.UniqueGamesTheorem.Gadget.aggregate_output_shift line 110

    Source documentation

    Child equivariance gives the actual aggregate translation formula.

    theorem aggregate_output_shift (J : I → B →ₗ[k] X × B)
        (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (C : P → B)
        (hC : ∀ u h, C (u + e h) = C u + lam h)
        (u : I → P) (h : I → R) :
        aggregate J (fun i => C (u i + e (h i))) =
          aggregate J (fun i => C (u i)) + shiftAggregate J lam h := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.shiftAggregate

11. theorem OAI.UniqueGamesTheorem.Gadget.parentOutput_equivariant line 121

    Source documentation

    Parent equivariance is derived for the kernel-defined shift space.

    theorem parentOutput_equivariant (J : I → B →ₗ[k] X × B)
        (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (C : P → B) (Q : X → B)
        (hC : ∀ u h, C (u + e h) = C u + lam h)
        (u : I → P) (h : parentShifts J lam) :
        parentOutput J C Q (u + parentEmbed J lam e h) =
          parentOutput J C Q u + parentLogical J lam h := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.parentShifts, OAI.UniqueGamesTheorem.Gadget.parentOutput, OAI.UniqueGamesTheorem.Gadget.parentEmbed, OAI.UniqueGamesTheorem.Gadget.parentLogical

12. theorem OAI.UniqueGamesTheorem.Gadget.output_difference_shift line 144

    Source documentation

    The output difference at a fixed perturbation is invariant under logical shifts. This is the conditioning input for the exact nonlinear noise law.

    theorem output_difference_shift
        (C : P → B) (e : R → P) (lam : R → B)
        (hC : ∀ u h, C (u + e h) = C u + lam h) (u a : P) (h : R) :
        C (u + e h + a) - C (u + e h) = C (u + a) - C u := by
    …

13. theorem OAI.UniqueGamesTheorem.Gadget.EmbeddedConditional.expect_uniform_output_embedded line 172

    Source documentation

    Exact conditional uniformity for an embedded carrier of logical shifts. No injectivity of the embedding is needed for this averaging statement.

    theorem expect_uniform_output_embedded (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
        (hlam : Function.Surjective lam) (C : P → B)
        (hC : ∀ u h, C (u + e h) = C u + lam h)
        (D : P → Z) (hD : ∀ u h, D (u + e h) = D u)
        (f : B → Z → M) :
        (𝔼 u, f (C u) (D u)) = 𝔼 u, 𝔼 b : B, f b (D u) := by
    …

14. theorem OAI.UniqueGamesTheorem.Gadget.EmbeddedConditional.expect_equivariant_output line 197

    Source documentation

    Unconditional uniformity is the constant-observable instance.

    theorem expect_equivariant_output (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
        (hlam : Function.Surjective lam) (C : P → B)
        (hC : ∀ u h, C (u + e h) = C u + lam h) (f : B → M) :
        (𝔼 u, f (C u)) = 𝔼 b : B, f b := by
    …

15. theorem OAI.UniqueGamesTheorem.Gadget.EmbeddedConditional.expect_linear_surjective line 206

    Source documentation

    Surjective linear maps send uniform finite input to uniform output.

    theorem expect_linear_surjective (f : P →ₗ[k] B) (hf : Function.Surjective f)
        (test : B → M) : (𝔼 u, test (f u)) = 𝔼 b : B, test b := by
    …

16. theorem OAI.UniqueGamesTheorem.Gadget.EmbeddedConditional.expect_uniform_difference_embedded line 213

    Source documentation

    Fixed-perturbation conditional uniformity without a range conversion.

    theorem expect_uniform_difference_embedded (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
        (hlam : Function.Surjective lam) (C : P → B)
        (hC : ∀ u h, C (u + e h) = C u + lam h) (a : P) (f : B → B → M) :
        (𝔼 u, f (C u) (C (u + a) - C u)) =
          𝔼 u, 𝔼 b : B, f b (C (u + a) - C u) := by
    …

17. def OAI.UniqueGamesTheorem.Gadget.Enlargement.probability line 238

    Source documentation

    Uniform finite probability, kept rational because the gadget noise is a pushforward of finite uniform choices.

    def probability {Ω : Type*} [Fintype Ω] (p : Ω → Prop) : ℚ :=
    …

18. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.probability_exists_le_sum line 242

    Source documentation

    A union bound without independence assumptions.

    theorem probability_exists_le_sum {Ω I : Type*} [Fintype Ω] [Fintype I]
        (p : I → Ω → Prop) :
        probability (fun x => ∃ i, p i x) ≤ ∑ i, probability (p i) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

19. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.probability_preimage_of_fibers line 258

    Source documentation

    Equal-size fibers determine the exact probability of every target event.

    theorem probability_preimage_of_fibers {Ω T : Type*} [Fintype Ω] [Fintype T]
        [Nonempty Ω] [Nonempty T] (f : Ω → T)
        (hf : ∀ x y : T, Nat.card {a : Ω // f a = x} = Nat.card {a : Ω // f a = y})
        (p : T → Prop) : probability (fun a => p (f a)) = probability p := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

20. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.exists_equiv_map_nonzero line 295

    Source documentation

    Automorphisms act transitively on the nonzero vectors. This follows by extending an isomorphism between the two one-dimensional spans.

    theorem exists_equiv_map_nonzero {F V : Type*} [Field F]
        [AddCommGroup V] [Module F V] (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
        ∃ e : V ≃ₗ[F] V, e x = y := by
    …

21. abbrev OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection line 306
22. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.linearInjection_nonempty_of_finrank_le line 310
23. def OAI.UniqueGamesTheorem.Gadget.Enlargement.postcompose line 320

    Source documentation

    Postcomposition permutes all linear injections, including their uniform finite distribution.

    def postcompose {F B K : Type*} [Field F] [AddCommGroup B] [Module F B]
        [AddCommGroup K] [Module F K] (e : K ≃ₗ[F] K) :
        LinearInjection F B K ≃ LinearInjection F B K where
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection

24. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.injection_eval_ne_zero line 334
25. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.exists_injection_hitting_nonzero line 345

    Source documentation

    Every nonzero target vector is hit by an injection at any prescribed nonzero base vector. This is the surjectivity ingredient of the product-shift map used before taking the quotient.

    theorem exists_injection_hitting_nonzero {F B K : Type*} [Field F]
        [AddCommGroup B] [Module F B] [FiniteDimensional F B]
        [AddCommGroup K] [Module F K] [FiniteDimensional F K]
        (h : Module.finrank F B ≤ Module.finrank F K)
        (b : B) (hb : b ≠ 0) (x : K) (hx : x ≠ 0) :
        ∃ L : LinearInjection F B K, L.1 b = x := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection

26. def OAI.UniqueGamesTheorem.Gadget.Enlargement.productShift line 357

    Source documentation

    The product-shift map before the final quotient.

    def productShift {F B K : Type*} [Field F] [AddCommGroup B] [Module F B]
        [AddCommGroup K] [Module F K] [Fintype (LinearInjection F B K)] :
        (LinearInjection F B K → B) →ₗ[F] K where
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection

27. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.productShift_surjective line 364
28. def OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput line 380

    Source documentation

    Sum of the injectively relabeled base outputs before quotienting.

    def enlargedOutput {F B K V : Type*} [Field F]
        [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
        [Fintype (LinearInjection F B K)] (C : V → B)
        (x : LinearInjection F B K → V) : K := ∑ L : LinearInjection F B K, L.1 (C (x L))

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection

29. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput_shift line 386

    Source documentation

    Equivariance of the nonlinear sum under the full product of base shifts.

    theorem enlargedOutput_shift {F B K V : Type*} [Field F]
        [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
        [AddCommGroup V] [Module F V] [Fintype (LinearInjection F B K)]
        (C : V → B) (i : B →ₗ[F] V)
        (hC : ∀ x b, C (x + i b) = C x + b)
        (x : LinearInjection F B K → V) (b : LinearInjection F B K → B) :
        enlargedOutput C (fun L => x L + i (b L)) =
          enlargedOutput C x + productShift b := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection, OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput, OAI.UniqueGamesTheorem.Gadget.Enlargement.productShift

30. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput_update line 399

    Source documentation

    Updating only one copy changes the output by its relabeled base-output difference. This identity retains all summands and does not assume they are independent.

    theorem enlargedOutput_update {F B K V : Type*} [Field F]
        [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
        [Fintype (LinearInjection F B K)] (C : V → B)
        (x : LinearInjection F B K → V) (L : LinearInjection F B K) (y : V) :
        enlargedOutput C (Function.update x L y) =
          enlargedOutput C x + L.1 (C y - C (x L)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection, OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput

31. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput_update_ne_iff line 421

    Source documentation

    Injectivity of the selected relabeling makes the enlargement output change exactly when that copy's base output changes.

    theorem enlargedOutput_update_ne_iff {F B K V : Type*} [Field F]
        [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
        [Fintype (LinearInjection F B K)] (C : V → B)
        (x : LinearInjection F B K → V) (L : LinearInjection F B K) (y : V) :
        enlargedOutput C (Function.update x L y) ≠ enlargedOutput C x ↔ C y ≠ C (x L) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection, OAI.UniqueGamesTheorem.Gadget.Enlargement.enlargedOutput

32. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.injection_eval_uniform line 429
33. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.pullback_ne_top_iff line 462

    Source documentation

    Failure of the pullback family to span the full dual has a nonzero vector witness in its common annihilator.

    theorem pullback_ne_top_iff {F B K : Type*} [Field F] [AddCommGroup B]
        [Module F B] [FiniteDimensional F B] [AddCommGroup K] [Module F K]
        (L : B →ₗ[F] K) (S : Submodule F (Module.Dual F K)) :
        S.map L.dualMap ≠ ⊤ ↔ ∃ b : B, b ≠ 0 ∧ L b ∈ S.dualCoannihilator := by
    …

34. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.nonzero_density_le line 498

    Source documentation

    The nonzero part of a codimension-r subspace has density at most 2⁻ʳ among all nonzero ambient vectors. The dimensions are written additively to avoid truncated subtraction.

    theorem nonzero_density_le (d r : ℕ) (h : 0 < d + r) :
        ((2 : ℚ) ^ d - 1) / ((2 : ℚ) ^ (d + r) - 1) ≤ 1 / (2 : ℚ) ^ r := by
    …

35. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.card_nonzero_binary line 507

    Source documentation

    Cardinality of all nonzero vectors in a finite binary vector space.

    theorem card_nonzero_binary (K : Type*) [AddCommGroup K] [Module (ZMod 2) K]
        [Fintype K] :
        Nat.card {x : K // x ≠ 0} = 2 ^ Module.finrank (ZMod 2) K - 1 := by
    …

36. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.probability_nonzero_subspace line 515

    Source documentation

    Exact density of the nonzero part of a binary subspace.

    theorem probability_nonzero_subspace (K : Type*) [AddCommGroup K]
        [Module (ZMod 2) K] [Fintype K] (W : Submodule (ZMod 2) K) :
        probability (fun x : {x : K // x ≠ 0} => x.1 ∈ W) =
          ((2 : ℚ) ^ Module.finrank (ZMod 2) W - 1) /
            ((2 : ℚ) ^ Module.finrank (ZMod 2) K - 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

37. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.probability_annihilator_le line 542

    Source documentation

    The annihilator dimension identity gives precisely the exponent needed by the enlargement, without any loss depending on the ambient dimension.

    theorem probability_annihilator_le (K : Type*) [AddCommGroup K]
        [Module (ZMod 2) K] [Fintype K] [FiniteDimensional (ZMod 2) K]
        (S : Submodule (ZMod 2) (Module.Dual (ZMod 2) K))
        (hK : 0 < Module.finrank (ZMod 2) K) :
        probability (fun x : {x : K // x ≠ 0} => x.1 ∈ S.dualCoannihilator) ≤
          1 / (2 : ℚ) ^ Module.finrank (ZMod 2) S := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

38. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.union_bound_le_quarter line 555

    Source documentation

    The threshold b + 2 is chosen before the ambient dimension.

    theorem union_bound_le_quarter (b r : ℕ) (hr : b + 2 ≤ r) :
        ((2 : ℚ) ^ b - 1) / (2 : ℚ) ^ r ≤ 1 / 4 := by
    …

39. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.pullback_failure_probability_le line 566

    Source documentation

    The enlargement's uniform-injection union bound, including its actual linear-algebraic bad event.

    theorem pullback_failure_probability_le {B K : Type*}
        [AddCommGroup B] [Module (ZMod 2) B] [Fintype B]
        [FiniteDimensional (ZMod 2) B]
        [AddCommGroup K] [Module (ZMod 2) K] [Fintype K]
        [FiniteDimensional (ZMod 2) K]
        [Fintype (LinearInjection (ZMod 2) B K)]
        [Nonempty (LinearInjection (ZMod 2) B K)]
        (S : Submodule (ZMod 2) (Module.Dual (ZMod 2) K))
        (hK : 0 < Module.finrank (ZMod 2) K) :
        probability (fun L : LinearInjection (ZMod 2) B K => S.map L.1.dualMap ≠ ⊤) ≤
          ((2 : ℚ) ^ Module.finrank (ZMod 2) B - 1) /
            (2 : ℚ) ^ Module.finrank (ZMod 2) S := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection, OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

40. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.pullback_failure_probability_le_quarter line 607

    Source documentation

    At least three quarters of the injection copies restrict onto the full base dual when the restriction rank is at least dim B + 2.

    theorem pullback_failure_probability_le_quarter {B K : Type*}
        [AddCommGroup B] [Module (ZMod 2) B] [Fintype B]
        [FiniteDimensional (ZMod 2) B]
        [AddCommGroup K] [Module (ZMod 2) K] [Fintype K]
        [FiniteDimensional (ZMod 2) K]
        [Fintype (LinearInjection (ZMod 2) B K)]
        [Nonempty (LinearInjection (ZMod 2) B K)]
        (S : Submodule (ZMod 2) (Module.Dual (ZMod 2) K))
        (hr : Module.finrank (ZMod 2) B + 2 ≤ Module.finrank (ZMod 2) S) :
        probability (fun L : LinearInjection (ZMod 2) B K => S.map L.1.dualMap ≠ ⊤) ≤
          1 / 4 := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.LinearInjection, OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

41. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.probability_not line 622
42. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.average_detection_lower_bound line 638

    Source documentation

    Averaging a nonnegative detection rate which is at least one quarter on each good copy. This is the last finite probability step of enlargement.

    theorem average_detection_lower_bound {Ω : Type*} [Fintype Ω] [Nonempty Ω]
        (bad : Ω → Prop) (detected : Ω → ℚ)
        (hnonneg : ∀ x, 0 ≤ detected x)
        (hgood : ∀ x, ¬bad x → 1 / 4 ≤ detected x) :
        (1 - probability bad) * (1 / 4) ≤
          (∑ x, detected x) / (Fintype.card Ω : ℚ) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

43. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.detection_constants line 666

    Source documentation

    The enlargement retains 3/16 detection, and hence the advertised 1/8. The hypotheses are the bad-copy probability and the average lower bound from the base gadget; they make no independence assertion.

    theorem detection_constants {bad detected : ℚ} (hbad : bad ≤ 1 / 4)
        (hdetected : (1 - bad) * (1 / 4) ≤ detected) :
        3 / 16 ≤ detected ∧ 1 / 8 ≤ detected := by
    …

44. theorem OAI.UniqueGamesTheorem.Gadget.Enlargement.enlarged_detection line 671
45. def OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic line 705

    Source documentation

    The finite harmonic potential, by its exact rational recurrence.

    def harmonic : ℕ → ℚ
      | 0 => 0
      | r + 1 => harmonic r + (↑(r + 1))⁻¹

46. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_zero line 709
47. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_succ line 711
48. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_eq_sum line 714
49. def OAI.UniqueGamesTheorem.Gadget.Harmonic.average line 721

    Source documentation

    Rational expectation under uniform sampling on a finite space.

    def average (f : Ω → ℚ) : ℚ := Finset.univ.expect f

50. def OAI.UniqueGamesTheorem.Gadget.Harmonic.probability line 724

    Source documentation

    Probability of a decidable event in the finite experiment.

    def probability (p : Ω → Prop) [DecidablePred p] : ℚ :=
    …

51. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.average_mono line 727
52. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.average_nonneg line 731
53. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.average_const line 735
54. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.average_add line 739
55. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.average_sub line 743
56. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.average_mul_left line 747
57. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.probability_nonneg line 751
58. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.probability_le_one line 757
59. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.probability_mono line 766
60. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.probability_not line 775
61. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.probability_eq_half_of_swap line 787

    Source documentation

    A bijection swapping an event with its complement proves exact half probability. At a leaf the bijection is translation by a symbol on which a nonzero binary character is one.

    theorem probability_eq_half_of_swap [Nonempty Ω]
        (p : Ω → Prop) [DecidablePred p] (e : Ω ≃ Ω)
        (hswap : ∀ ω, p (e ω) ↔ ¬ p ω) : probability p = 1 / 2 := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability

62. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.binary_character_detection_probability line 799

    Source documentation

    Every nonzero binary additive character detects precisely half of uniform symbols. The witness may depend on the previously sampled path.

    theorem binary_character_detection_probability [AddGroup Ω]
        (χ : Ω →+ ZMod 2) (v : Ω) (hv : χ v ≠ 0) :
        probability (fun ω => χ ω ≠ 0) = 1 / 2 := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability

63. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.binary_family_detection_ge_half line 818

    Source documentation

    A surviving family contains a nonzero character, so its detection event contains an event of exact half probability.

    theorem binary_family_detection_ge_half [AddGroup Ω]
        (detects : Ω → Prop) [DecidablePred detects]
        (χ : Ω →+ ZMod 2) (v : Ω) (hv : χ v ≠ 0)
        (hcontains : ∀ ω, χ ω ≠ 0 → detects ω) :
        (1 / 2 : ℚ) ≤ probability detects := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability

64. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_nonneg line 826
65. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_mono line 831
66. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_pos line 839
67. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic_sub_predecessor line 844
68. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.generic_drop_identity line 851

    Source documentation

    A generic rank-r space loses either zero or one dimension. Its harmonic drop is exactly the loss indicator times 1/r.

    theorem generic_drop_identity (r : ℕ) (next : Ω → ℕ) (hr : 0 < r)
        (hstep : ∀ ω, next ω = r ∨ next ω = r - 1) :
        average (fun ω => harmonic r - harmonic (next ω)) =
          (r : ℚ)⁻¹ * probability (fun ω => next ω < r) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic, OAI.UniqueGamesTheorem.Gadget.Harmonic.probability

69. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.generic_expected_drop_le line 867

    Source documentation

    The generic loss probability 3rθ becomes the rank-independent harmonic loss bound 3θ.

    theorem generic_expected_drop_le (r : ℕ) (next : Ω → ℕ) (θ : ℚ)
        (hr : 0 < r) (hstep : ∀ ω, next ω = r ∨ next ω = r - 1)
        (hloss : probability (fun ω => next ω < r) ≤ 3 * r * θ) :
        average (fun ω => harmonic r - harmonic (next ω)) ≤ 3 * θ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability, OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic

70. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.arbitrary_expected_drop_le line 881

    Source documentation

    Without genericity, charge the entire harmonic potential only on paths where some rank is lost.

    theorem arbitrary_expected_drop_le (r : ℕ) (next : Ω → ℕ) (p : ℚ)
        (hstep : ∀ ω, next ω ≤ r)
        (hloss : probability (fun ω => next ω < r) ≤ p) :
        average (fun ω => harmonic r - harmonic (next ω)) ≤ harmonic r * p := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability, OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic

71. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.expected_drop_le_four_theta line 902

    Source documentation

    Averaging a conditional rank-loss estimate uses only a bound on the bad space's probability, even when the selected lift depends on that space.

    theorem expected_drop_le_four_theta [Nonempty Ω]
        (drop : Ω → ℚ) (bad : Ω → Prop) [DecidablePred bad] (C θ ε : ℚ)
        (hC : 0 ≤ C) (hθ : 0 ≤ θ)
        (hconditional : ∀ ω, drop ω ≤ 3 * θ + C * θ * if bad ω then 1 else 0)
        (hbad : probability bad ≤ ε) (hsmall : C * ε ≤ 1) :
        average drop ≤ 4 * θ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability, OAI.UniqueGamesTheorem.Gadget.Harmonic.average

72. def OAI.UniqueGamesTheorem.Gadget.Harmonic.badRankCoefficient line 919
73. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.badRankCoefficient_nonneg line 921
74. def OAI.UniqueGamesTheorem.Gadget.Harmonic.depth line 924
75. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.depth_budget line 926
76. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.expected_total_drop_le line 936

    Source documentation

    Expected harmonic losses telescope. The ranks may be arbitrary functions of the full path; this assertion introduces no independence premise.

    theorem expected_total_drop_le [Nonempty Ω] (rank : ℕ → Ω → ℕ)
        (r₀ s : ℕ) (θ : ℚ) (hinitial : ∀ ω, rank 0 ω = r₀)
        (hstep : ∀ j < s,
          average (fun ω => harmonic (rank j ω) - harmonic (rank (j + 1) ω)) ≤ 4 * θ) :
        harmonic r₀ - average (fun ω => harmonic (rank s ω)) ≤ 4 * s * θ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic

77. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.survival_probability_ge_half_of_potential line 959

    Source documentation

    The potential-to-survival step needs only the final finite experiment, allowing earlier levels to have different path sample spaces.

    theorem survival_probability_ge_half_of_potential (rank : Ω → ℕ) (r₀ : ℕ)
        (hr₀ : 0 < r₀) (hterminal : ∀ ω, rank ω ≤ r₀)
        (hmean : harmonic r₀ / 2 ≤ average (fun ω => harmonic (rank ω))) :
        (1 / 2 : ℚ) ≤ probability (fun ω => 0 < rank ω) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic, OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.probability

78. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.survival_probability_ge_half line 983

    Source documentation

    At depth s with 4sθ ≤ H(r₀)/2, at least half the paths have nonzero terminal rank. The terminal bound follows from rank monotonicity in the actual gadget, and is kept explicit here.

    theorem survival_probability_ge_half [Nonempty Ω] (rank : ℕ → Ω → ℕ)
        (r₀ s : ℕ) (θ : ℚ) (hr₀ : 0 < r₀)
        (hinitial : ∀ ω, rank 0 ω = r₀)
        (hterminal : ∀ ω, rank s ω ≤ r₀)
        (hstep : ∀ j < s,
          average (fun ω => harmonic (rank j ω) - harmonic (rank (j + 1) ω)) ≤ 4 * θ)
        (hdepth : 4 * s * θ ≤ harmonic r₀ / 2) :
        (1 / 2 : ℚ) ≤ probability (fun ω => 0 < rank s ω) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic, OAI.UniqueGamesTheorem.Gadget.Harmonic.probability

79. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.survival_of_adaptive_step_law line 999

    Source documentation

    Direct assembly of the adaptive calculation. conditionalDrop is the conditional mean after fixing the history; hmean is the finite averaging identity. The only assertion about bad orientations is their probability bound, so a future lift is allowed to depend on the incoming orientation.

    theorem survival_of_adaptive_step_law [Nonempty Ω]
        (rank : ℕ → Ω → ℕ) (bad : ℕ → Ω → Prop)
        [∀ j, DecidablePred (bad j)] (conditionalDrop : ℕ → Ω → ℚ)
        (r₀ : ℕ) (θ ε : ℚ) (hr₀ : 0 < r₀) (hθ : 0 < θ)
        (hinitial : ∀ ω, rank 0 ω = r₀)
        (hterminal : ∀ ω, rank (depth r₀ θ) ω ≤ r₀)
        (hmean : ∀ j < depth r₀ θ,
          average (fun ω => harmonic (rank j ω) - harmonic (rank (j + 1) ω)) =
            average (conditionalDrop j))
        (hconditional : ∀ j < depth r₀ θ, ∀ ω,
          conditionalDrop j ω ≤ 3 * θ + badRankCoefficient r₀ * θ *
            if bad j ω then 1 else 0)
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.depth, OAI.UniqueGamesTheorem.Gadget.Harmonic.average, OAI.UniqueGamesTheorem.Gadget.Harmonic.harmonic, OAI.UniqueGamesTheorem.Gadget.Harmonic.badRankCoefficient

80. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.detection_probability_ge_quarter line 1025

    Source documentation

    A final independent uniform symbol detects a surviving character with probability at least one half. Multiplying this conditional bound by the surviving-path probability gives the required quarter.

    theorem detection_probability_ge_quarter [Nonempty Ω]
        (survives : Ω → Prop) [DecidablePred survives] (conditionalDetection : Ω → ℚ)
        (hsurvival : (1 / 2 : ℚ) ≤ probability survives)
        (hnonneg : ∀ ω, 0 ≤ conditionalDetection ω)
        (hdetect : ∀ ω, survives ω → (1 / 2 : ℚ) ≤ conditionalDetection ω) :
        (1 / 4 : ℚ) ≤ average conditionalDetection := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability, OAI.UniqueGamesTheorem.Gadget.Harmonic.average

81. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.probability_product line 1046

    Source documentation

    Uniform paths and a separately sampled uniform terminal symbol have the product law used in the leaf-noise experiment.

    theorem probability_product {Ξ : Type*} [Fintype Ξ]
        (detects : Ω × Ξ → Prop) [DecidablePred detects] :
        probability detects = average (fun ω => probability (fun ξ => detects (ω, ξ))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability, OAI.UniqueGamesTheorem.Gadget.Harmonic.average

82. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.product_detection_probability_ge_quarter line 1054
83. theorem OAI.UniqueGamesTheorem.Gadget.Harmonic.binary_product_detection_probability_ge_quarter line 1069

    Source documentation

    Terminal family detection with actual binary characters rather than an assumed conditional probability bound. A character can be selected separately on every surviving path.

    theorem binary_product_detection_probability_ge_quarter [Nonempty Ω]
        {Ξ : Type*} [Fintype Ξ] [AddGroup Ξ]
        (survives : Ω → Prop) [DecidablePred survives]
        (detects : Ω × Ξ → Prop) [DecidablePred detects]
        (hsurvival : (1 / 2 : ℚ) ≤ probability survives)
        (hcharacter : ∀ ω, survives ω → ∃ χ : Ξ →+ ZMod 2, ∃ v : Ξ,
          χ v ≠ 0 ∧ ∀ ξ, χ ξ ≠ 0 → detects (ω, ξ)) :
        (1 / 4 : ℚ) ≤ probability detects := by
    …

    Mentions: OAI.UniqueGamesTheorem.Gadget.Harmonic.probability