OAI/Computability/UniqueGames/Gadgets/QuotientLemmas.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Conditional uniformity by translation averaging

For uniform finite input, an equivariant output is uniform even conditional on any shift-invariant observable. The observable need not have a finite range. The proof averages translations directly and therefore never divides by a conditioning probability. In particular it applies to the output difference at a fixed perturbation, and to an independent finite noise choice.

  1. def OAI.UniqueGamesTheorem.Gadget.Quotient.shiftKernel line 22

    Source documentation

    The logical kernel viewed as a submodule of the ambient input space.

    def shiftKernel (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) : Submodule 𝕜 P :=
…
  2. abbrev OAI.UniqueGamesTheorem.Gadget.Quotient.Space line 25
  3. def OAI.UniqueGamesTheorem.Gadget.Quotient.projection line 27
  4. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.projection_surjective line 30
  5. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.mem_shiftKernel line 33
  6. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.projection_eq_zero line 36
  7. def OAI.UniqueGamesTheorem.Gadget.Quotient.quotientShift line 48

    Source documentation

    Inclusion of the quotient shift space into the ambient quotient.

    def quotientShift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) :
    (R ⧸ LinearMap.ker lam) →ₗ[𝕜] Space R lam :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Space

  8. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.quotientShift_mk line 54
  9. def OAI.UniqueGamesTheorem.Gadget.Quotient.logicalShift line 58

    Source documentation

    The logical alphabet is realized as actual linear shifts of the quotient.

    noncomputable def logicalShift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) : B →ₗ[𝕜] Space R lam :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Space

  10. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.logicalShift_lambda line 62
  11. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.logicalShift_injective line 67
  12. def OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant line 80

    Source documentation

    Equivariance under every allowed shift; no linearity of C is assumed.

    def Equivariant (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) (C : P → B) : Prop :=
…
  13. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.difference_shift line 84

    Source documentation

    An output difference is unchanged by every logical shift.

    theorem difference_shift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (C : P → B) (hC : Equivariant R lam C) (u a : P) (h : R) :
    C (u + (h : P) + a) - C (u + (h : P)) = C (u + a) - C u := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  14. def OAI.UniqueGamesTheorem.Gadget.Quotient.conditionedShiftEquiv line 93

    Source documentation

    Translating by a logical shift bijects output fibers even after conditioning on an arbitrary shift-invariant event.

    def conditionedShiftEquiv (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (C : P → B) (hC : Equivariant R lam C) (D : P → Prop)
    (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u) (b : B) (h : R) :
    {u : P // C u = b ∧ D u} ≃ {u : P // C u = b + lam h ∧ D u} where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  15. def OAI.UniqueGamesTheorem.Gadget.Quotient.conditionedFiberEquiv line 109

    Source documentation

    Surjectivity makes all output fibers equally large inside an invariant event, without assuming that this event has positive probability.

    noncomputable def conditionedFiberEquiv (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (D : P → Prop) (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u)
    (b c : B) : {u : P // C u = b ∧ D u} ≃ {u : P // C u = c ∧ D u} := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  16. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.conditioned_fiber_card line 119
  17. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.output_fiber_card line 126
  18. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.difference_fiber_card line 134

    Source documentation

    Fixing the additive perturbation and the observed difference leaves the initial output uniform: the joint fibers have equal cardinality for all outputs.

    theorem difference_fiber_card (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (a : P) (d b c : B) :
    Nat.card {u : P // C u = b ∧ C (u + a) - C u = d} =
      Nat.card {u : P // C u = c ∧ C (u + a) - C u = d} := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  19. def OAI.UniqueGamesTheorem.Gadget.Quotient.conditionedSigmaEquiv line 144

    Source documentation

    Splitting an invariant event into its output fibers.

    def conditionedSigmaEquiv (C : P → B) (D : P → Prop) :
    {u : P // D u} ≃ Σ b : B, {u : P // C u = b ∧ D u} where
…
  20. def OAI.UniqueGamesTheorem.Gadget.Quotient.conditionedProductEquiv line 152

    Source documentation

    An invariant event factors as an independent logical output and one fiber.

    noncomputable def conditionedProductEquiv (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (D : P → Prop) (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u) (b : B) :
    {u : P // D u} ≃ B × {u : P // C u = b ∧ D u} :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  21. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.conditionedProductEquiv_fst line 160
  22. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.conditioned_card_factorization line 167

    Source documentation

    Exact counting factorization underlying the conditional uniform law.

    theorem conditioned_card_factorization [Finite P] [Finite B]
    (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (D : P → Prop) (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u) (b : B) :
    Nat.card {u : P // D u} = Nat.card B * Nat.card {u : P // C u = b ∧ D u} := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  23. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.difference_card_factorization line 175
  24. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.output_constant_on_fibers line 185
  25. def OAI.UniqueGamesTheorem.Gadget.Quotient.output line 193
  26. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.output_projection line 198
  27. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.output_equivariant line 202
  28. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.change_iff line 212

    Source documentation

    Noise pushforward preserves the change event pointwise, before averaging.

    theorem change_iff (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (C : P → B) (hC : Equivariant R lam C) (u a : P) :
    (output R lam C hC (projection R lam u + projection R lam a) ≠
      output R lam C hC (projection R lam u)) ↔ C (u + a) ≠ C u := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant, OAI.UniqueGamesTheorem.Gadget.Quotient.output, OAI.UniqueGamesTheorem.Gadget.Quotient.projection

  29. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.character_pullback_shift line 219

    Source documentation

    Pulling a quotient character back recovers its prescribed logical value.

    theorem character_pullback_shift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (g : Space R lam →ₗ[𝕜] 𝕜) (h : R) :
    (g.comp (projection R lam)) (h : P) =
      (g.comp (logicalShift R lam hlam)) (lam h) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Space, OAI.UniqueGamesTheorem.Gadget.Quotient.projection, OAI.UniqueGamesTheorem.Gadget.Quotient.logicalShift

  30. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.detection_iff line 227

    Source documentation

    Pullback preserves the detection event of an already selected family of quotient characters, including a section of the logical restriction map.

    theorem detection_iff {I : Type*} (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (family : I → Space R lam →ₗ[𝕜] 𝕜) (a : P) :
    (∃ i, family i (projection R lam a) ≠ 0) ↔
      ∃ i, (family i).comp (projection R lam) a ≠ 0 := Iff.rfl

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Space, OAI.UniqueGamesTheorem.Gadget.Quotient.projection

  31. def OAI.UniqueGamesTheorem.Gadget.Quotient.fiberMap line 233

    Source documentation

    Translation by the logical kernel parametrizes a quotient fiber.

    def fiberMap (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) (a : P) :
    shiftKernel R lam → {u : P // projection R lam u = projection R lam a} :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.shiftKernel, OAI.UniqueGamesTheorem.Gadget.Quotient.projection

  32. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.fiberMap_bijective line 240
  33. theorem OAI.UniqueGamesTheorem.Gadget.Quotient.fiber_card line 254

    Source documentation

    Every fiber has the same cardinality, justifying uniform-input pushforward.

    theorem fiber_card (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) (x : Space R lam) :
    Nat.card {u : P // projection R lam u = x} = Nat.card (shiftKernel R lam) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Space, OAI.UniqueGamesTheorem.Gadget.Quotient.projection, OAI.UniqueGamesTheorem.Gadget.Quotient.shiftKernel

  34. theorem OAI.UniqueGamesTheorem.Gadget.ConditionalOutput.expect_output_translate line 281
  35. theorem OAI.UniqueGamesTheorem.Gadget.ConditionalOutput.expect_uniform_output line 293

    Source documentation

    Exact replacement of the initial output by an independent uniform symbol, jointly with every shift-invariant observable.

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

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  36. theorem OAI.UniqueGamesTheorem.Gadget.ConditionalOutput.expect_uniform_output_difference line 318

    Source documentation

    The output difference is a permissible observable, for every fixed perturbation, including zero and perturbations never sampled by a noise law.

    theorem expect_uniform_output_difference (R : Submodule k P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : Quotient.Equivariant R lam C) (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
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  37. theorem OAI.UniqueGamesTheorem.Gadget.ConditionalOutput.expect_uniform_output_noise line 329

    Source documentation

    A finite independent noise choice may be retained in the test function; conditioning on its value does not affect conditional output uniformity.

    theorem expect_uniform_output_noise {N : Type*} [Fintype N]
    (R : Submodule k P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : Quotient.Equivariant R lam C) (noise : N → P) (f : N → B → B → M) :
    (𝔼 n, 𝔼 u, f n (C u) (C (u + noise n) - C u)) =
      𝔼 n, 𝔼 u, 𝔼 b : B, f n b (C (u + noise n) - C u) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Quotient.Equivariant

  38. structure OAI.UniqueGamesTheorem.Gadget.Stage line 348

    Source documentation

    An equivariant finite stage, including its concrete finite noise sampler.

    structure Stage (k : Type u) (B : Type v) [CommRing k]
    [AddCommGroup B] [Module k B] where
…
  39. def OAI.UniqueGamesTheorem.Gadget.Stage.base line 378

    Source documentation

    The height-zero input, shift and uniform noise alphabet.

    def base : Stage k B where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  40. def OAI.UniqueGamesTheorem.Gadget.Stage.next line 394

    Source documentation

    One complete recursive level, with actual single-coordinate leaf noise.

    noncomputable def next (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B)
    (s : Stage k B) : Stage k B where
…

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

  41. def OAI.UniqueGamesTheorem.Gadget.Stage.iterate line 411

    Source documentation

    The finite stage at any natural height, using the same alphabet and block family at every level. Surjectivity and equivariance have been proved by the constructor, and hence are available at every height without extra hypotheses.

    noncomputable def iterate (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B) : ℕ → Stage k B
  | 0 => base
  | n + 1 => next J hJ Q (iterate J hJ Q n)

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.Stage.base, OAI.UniqueGamesTheorem.Gadget.Stage.next

  42. theorem OAI.UniqueGamesTheorem.Gadget.Stage.iterate_zero line 416
  43. theorem OAI.UniqueGamesTheorem.Gadget.Stage.iterate_succ line 420
  44. structure OAI.UniqueGamesTheorem.Gadget.Lift line 443

    Source documentation

    A linear lift of a logical character subspace to the actual stage input.

    structure Lift (s : Stage k B) (S : Submodule k (B →ₗ[k] k)) where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  45. def OAI.UniqueGamesTheorem.Gadget.Lift.restrict line 448

    Source documentation

    Restricting a lift preserves its prescribed logical characters.

    def Lift.restrict {s : Stage k B} {S T : Submodule k (B →ₗ[k] k)}
    (L : Lift s T) (hST : S ≤ T) : Lift s S where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.Lift

  46. def OAI.UniqueGamesTheorem.Gadget.singleInput line 457

    Source documentation

    Linear insertion into one physical input coordinate.

    def singleInput (i : I) (P : Type v) [AddCommGroup P] [Module k P] :
    P →ₗ[k] (I → P) where
…
  47. def OAI.UniqueGamesTheorem.Gadget.childCharacter line 465

    Source documentation

    The logical map of a child, obtained from the common parent first-coordinate map and the prescribed logical character.

    def childCharacter (J : I → B →ₗ[k] X × B)
    {S : Submodule k (B →ₗ[k] k)} (γ : S →ₗ[k] (X →ₗ[k] k)) (i : I) :
    S →ₗ[k] (B →ₗ[k] k) where
…
  48. theorem OAI.UniqueGamesTheorem.Gadget.exists_common_child_character line 473
  49. def OAI.UniqueGamesTheorem.Gadget.descendantFamily line 490

    Source documentation

    The descendant family using a section of the actual image.

    def descendantFamily {s : Stage k B} {S : Submodule k (B →ₗ[k] k)}
    (ψ : S →ₗ[k] ((I → s.Input) →ₗ[k] k)) (i : I)
    (φ : S →ₗ[k] (B →ₗ[k] k))
    (sectionMap : LinearMap.range φ →ₗ[k] S) :
    LinearMap.range φ →ₗ[k] (s.Input →ₗ[k] k) where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  50. theorem OAI.UniqueGamesTheorem.Gadget.exists_descendant_lift line 501

    Source documentation

    Every child image carries a genuine child lift. The section is constructed by ordinary linear algebra and is chosen without any later path or leaf symbol.

    theorem exists_descendant_lift
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (Q : X → B) (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
    (L : Lift (Stage.next J hJ Q s) S)
    (γ : S →ₗ[k] (X →ₗ[k] k))
    (hγ : ∀ i z h, L.family z (Pi.single i (s.embed h)) =
      childCharacter J γ i z (s.logical h)) (i : I) :
    ∃ (L' : Lift s (LinearMap.range (childCharacter J γ i)))
      (sectionMap : LinearMap.range (childCharacter J γ i) →ₗ[k] S),
      (∀ z, childCharacter J γ i (sectionMap z) = z.val) ∧
      (∀ z p, L'.family z p = L.family (sectionMap z) (Pi.single i p)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.next, OAI.UniqueGamesTheorem.Gadget.childCharacter

  51. theorem OAI.UniqueGamesTheorem.Gadget.descendant_detection_implies_parent line 530

    Source documentation

    Pointwise containment of child detection in parent detection. Repeating this implication along a path preserves the original family at the root.

    theorem descendant_detection_implies_parent
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (Q : X → B) (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
    (L : Lift (Stage.next J hJ Q s) S)
    {S' : Submodule k (B →ₗ[k] k)} (L' : Lift s S')
    (sectionMap : S' →ₗ[k] S) (i : I)
    (hfamily : ∀ z p, L'.family z p = L.family (sectionMap z) (Pi.single i p))
    (n : s.Noise) (hdetect : ∃ z, L'.family z (s.noise n) ≠ 0) :
    ∃ z, L.family z ((Stage.next J hJ Q s).noise (i, n)) ≠ 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.next

  52. def OAI.UniqueGamesTheorem.Gadget.Descent.commonGamma line 556
  53. theorem OAI.UniqueGamesTheorem.Gadget.Descent.commonGamma_spec line 561
  54. def OAI.UniqueGamesTheorem.Gadget.Descent.childDomain line 567
  55. def OAI.UniqueGamesTheorem.Gadget.Descent.childLift line 571
  56. def OAI.UniqueGamesTheorem.Gadget.Descent.childSection line 577
  57. theorem OAI.UniqueGamesTheorem.Gadget.Descent.childSection_rightInverse line 584
  58. theorem OAI.UniqueGamesTheorem.Gadget.Descent.childLift_spec line 593
  59. theorem OAI.UniqueGamesTheorem.Gadget.Descent.child_detection line 602
  60. theorem OAI.UniqueGamesTheorem.Gadget.Descent.child_rank_le line 610
  61. def OAI.UniqueGamesTheorem.Gadget.Descent.leafRank line 617

    Source documentation

    Terminal logical rank along the actual recursively sampled path. The final uniform symbol is ignored by this rank function.

    noncomputable def leafRank
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J)) (Q : X → B) :
    (n : ℕ) → (S : Submodule k (B →ₗ[k] k)) →
    Lift (Stage.iterate J hJ Q n) S → (Stage.iterate J hJ Q n).Noise → ℕ
  | 0, S, _, _ => Module.finrank k S
  | n + 1, S, L, t => leafRank J hJ Q n
      (childDomain J hJ Q (Stage.iterate J hJ Q n) S L t.1)
      (childLift J hJ Q (Stage.iterate J hJ Q n) S L t.1) t.2

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.iterate, OAI.UniqueGamesTheorem.Gadget.Descent.childDomain, OAI.UniqueGamesTheorem.Gadget.Descent.childLift

  62. theorem OAI.UniqueGamesTheorem.Gadget.Descent.leafRank_le line 626
  63. instance OAI.UniqueGamesTheorem.Gadget.DescentProbability.noiseFintype line 658
  64. def OAI.UniqueGamesTheorem.Gadget.DescentProbability.terminalPotential line 664
  65. theorem OAI.UniqueGamesTheorem.Gadget.DescentProbability.terminalPotential_zero line 669
  66. theorem OAI.UniqueGamesTheorem.Gadget.DescentProbability.terminalPotential_succ line 677
  67. theorem OAI.UniqueGamesTheorem.Gadget.DescentProbability.expected_terminal_loss line 693

    Source documentation

    The only geometric inputs are the outgoing harmonic loss estimate for every lift and the fresh-orientation bound for every child image. The lift may depend on every previous orientation; the proof never declares it independent.

    theorem expected_terminal_loss
    (bad : Submodule k (B →ₗ[k] k) → Prop) [DecidablePred bad]
    (r₀ : ℕ) (C θ ε : ℚ) (hC : 0 ≤ C) (hθ : 0 ≤ θ) (hsmall : C * ε ≤ 1)
    (hstep : ∀ (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
      (L : Lift (Stage.next J hJ Q s) S), Module.finrank k S ≤ r₀ →
      average (fun i => harmonic (Module.finrank k S) -
        harmonic (Module.finrank k (childDomain J hJ Q s S L i))) ≤
          3 * θ + C * θ * if bad S then 1 else 0)
    (hfresh : ∀ (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
      (L : Lift (Stage.next J hJ Q s) S), Module.finrank k S ≤ r₀ →
      probability (fun i => bad (childDomain J hJ Q s S L i)) ≤ ε)
    (n : ℕ) (S : Submodule k (B →ₗ[k] k)) (L : Lift (Stage.iterate J hJ Q n) S)
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.next, OAI.UniqueGamesTheorem.Gadget.Stage.iterate

  68. def OAI.UniqueGamesTheorem.Gadget.LeafDetection.survivalProbability line 754
  69. def OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability line 759
  70. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability_nonneg line 766
  71. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability_restrict_le line 775

    Source documentation

    Restricting the logical domain can only remove detecting characters.

    theorem detectionProbability_restrict_le (n : ℕ)
    (S T : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2)) (hST : S ≤ T)
    (L : Lift (Stage.iterate J hJ Q n) T) :
    detectionProbability J hJ Q n S (L.restrict hST) ≤
      detectionProbability J hJ Q n T L := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.iterate, OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability

  72. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability_zero_of_rank_pos line 786
  73. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.survivalProbability_zero line 811
  74. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.survivalProbability_succ line 821
  75. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.average_child_detection_le line 836
  76. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.half_survival_le_detection line 857

    Source documentation

    Detection by the root lift is at least one half the actual terminal-rank survival probability, on precisely the recursively generated noise sample.

    theorem half_survival_le_detection (n : ℕ)
    (S : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2))
    (L : Lift (Stage.iterate J hJ Q n) S) :
    (1 / 2 : ℚ) * survivalProbability J hJ Q n S L ≤
      detectionProbability J hJ Q n S L := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.iterate, OAI.UniqueGamesTheorem.Gadget.LeafDetection.survivalProbability, OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability

  77. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.quarter_detection_of_terminal_potential line 882

    Source documentation

    Actual quarter detection follows from retaining half the initial harmonic potential; all leaf-to-root event containments are already proved.

    theorem quarter_detection_of_terminal_potential (n : ℕ)
    (S : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2))
    (L : Lift (Stage.iterate J hJ Q n) S)
    (hrank : 0 < Module.finrank (ZMod 2) S)
    (hpotential : harmonic (Module.finrank (ZMod 2) S) / 2 ≤
      terminalPotential J hJ Q n S L) :
    (1 / 4 : ℚ) ≤ detectionProbability J hJ Q n S L := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.iterate, OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability

  78. theorem OAI.UniqueGamesTheorem.Gadget.LeafDetection.quarter_detection_of_restricted_terminal_potential line 897

    Source documentation

    The fixed generic top subspace may be chosen inside a full logical family; the resulting quarter bound still concerns the original lift.

    theorem quarter_detection_of_restricted_terminal_potential (n : ℕ)
    (S T : Submodule (ZMod 2) (B →ₗ[ZMod 2] ZMod 2)) (hST : S ≤ T)
    (L : Lift (Stage.iterate J hJ Q n) T)
    (hrank : 0 < Module.finrank (ZMod 2) S)
    (hpotential : harmonic (Module.finrank (ZMod 2) S) / 2 ≤
      terminalPotential J hJ Q n S (L.restrict hST)) :
    (1 / 4 : ℚ) ≤ detectionProbability J hJ Q n T L :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.Stage.iterate, OAI.UniqueGamesTheorem.Gadget.LeafDetection.detectionProbability