OAI/Computability/UniqueGames/PCP/FoldedEquationLemmas.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Actual equations for clause contexts having no valid local assignment. The right answer is the constant false bit, represented by two occurrences of one dummy variable. Those occurrences cancel for every assignment. The remaining left answer is folded, so its uniform bias is exactly zero.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.Address line 25

    Source documentation

    Left and right stored tables have disjoint variable names.

    abbrev Address (i₀ : I) (j₀ : J) := HalfCube i₀ ⊕ HalfCube j₀

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube

  2. def OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.storedAssignment line 27
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.rhsCorrection line 32

    Source documentation

    Cancellation of the two copies of g j₀ leaves this explicit RHS.

    def rhsCorrection (π : J → I) (i₀ : I) (j₀ : J)
    (f : Cube I) (μ : Cube J) : Bool := f i₀ ^^ f (π j₀) ^^ μ j₀

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.correction_eq line 35
  5. def OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation line 43

    Source documentation

    One sampled test becomes exactly one three-occurrence equation.

    def equation (π : J → I) (i₀ : I) (j₀ : J)
    (f : Cube I) (g μ : Cube J) : Equation (Address i₀ j₀) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.Address

  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.xor_corrections line 50
  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation_satisfied line 57

    Source documentation

    Exact Boolean semantics, with the three stored bits read from one assignment. There is no distinct-address assumption.

    theorem equation_satisfied (π : J → I) (i₀ : I) (j₀ : J)
    (tableA : HalfCube i₀ → Bool) (tableB : HalfCube j₀ → Bool)
    (f : Cube I) (g μ : Cube J) :
    satisfied (equation π i₀ j₀ f g μ) (storedAssignment tableA tableB) =
      !(foldedAnswer i₀ tableA f ^^ foldedAnswer j₀ tableB g ^^
        foldedAnswer j₀ tableB (thirdQuery π f g μ)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.storedAssignment, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.thirdQuery

  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 68
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation_indicator line 77
  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 89

    Source documentation

    Repeated variable occurrences retain XOR multiplicity and cancel in pairs.

    theorem satisfied_repeated_right {Name : Type} (e : Equation Name)
    (assignment : Name → Bool) (h : e.second = e.third) :
    satisfied e assignment = (assignment e.first == e.rhs) := by
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equation_repeated_right line 96
  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 105
  13. def OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation line 113

    Source documentation

    Conditioned storage uses only satisfying-assignment coordinates, so identical restricted canonical inputs are the same variable, even for distinct raw queries.

    def conditionedEquation (valid : J → Bool) (π : J → I)
    (i₀ : I) (j₀ : {j : J // valid j = true})
    (f : Cube I) (g μ : Cube J) : Equation (Address i₀ j₀) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.Address

  14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 118
  15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 123
  16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 134
  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 144
  18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 156
  19. def OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equationAcceptance line 172

    Source documentation

    Actual weighted acceptance of the emitted equation family.

    def equationAcceptance (ε : ℝ) (π : J → I) (i₀ : I) (j₀ : J)
    (tableA : HalfCube i₀ → Bool) (tableB : HalfCube j₀ → Bool) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube

  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 178
  21. def OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 185
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 192
  23. def OAI.UniqueGamesTheorem.Foundations.Hastad.mapEquation line 222

    Source documentation

    Rename the three occurrences without merging or dropping any occurrence.

    def mapEquation {Name Name' : Type} (rename : Name → Name')
    (e : Equation Name) : Equation Name' where
…
  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.satisfied_mapEquation line 229
  25. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address line 238

    Source documentation

    A left half-table address or the one dummy address.

    abbrev Address (i₀ : I) := HalfCube i₀ ⊕ Unit

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube

  26. def OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.storedAssignment line 240
  27. def OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation line 244

    Source documentation

    The dummy appears twice. Its assigned bit cancels in the equation.

    def equation (i₀ : I) (f : Cube I) : Equation (Address i₀) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address

  28. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_second_eq_third line 250
  29. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_satisfied line 254

    Source documentation

    Exact semantics for every assignment, including an arbitrary dummy bit.

    theorem equation_satisfied (i₀ : I) (assignment : Address i₀ → Bool) (f : Cube I) :
    satisfied (equation i₀ f) assignment =
      !(foldedAnswer i₀ (fun h => assignment (.inl h)) f) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer

  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 262
  31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_flip_first line 268

    Source documentation

    Flipping the query preserves all three addresses and reverses the RHS.

    theorem equation_flip_first (i₀ : I) (f : Cube I) :
    (equation i₀ (cubeFlip f)).first = (equation i₀ f).first := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation, OAI.UniqueGamesTheorem.Foundations.Hastad.cubeFlip

  32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_flip_rhs line 273
  33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 276
  34. def OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.pairedEquations line 283

    Source documentation

    The two opposite queries give an explicit balanced list of equations.

    def pairedEquations (i₀ : I) (f : Cube I) : List (Equation (Address i₀)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address

  35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.pairedEquations_length line 286
  36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 289
  37. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 293

    Source documentation

    Exactly one actual equation in the pair accepts every fixed proof.

    theorem pairedEquations_acceptedCount (i₀ : I) (assignment : Address i₀ → Bool)
    (f : Cube I) :
    (pairedEquations i₀ f).countP (fun e => satisfied e assignment) = 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.pairedEquations

  38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 299
  39. def OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equationAcceptance line 309
  40. def OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equationBias line 312
  41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 315
  42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equation_indicator line 320
  43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 328

    Source documentation

    Uniform queries accept with probability exactly one half. No right folding anchor, valid right assignment, or placeholder response is assumed.

    theorem equationAcceptance_eq_half (i₀ : I) (assignment : Address i₀ → Bool) :
    equationAcceptance i₀ assignment = 1 / 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equationAcceptance

  44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 336

    Source documentation

    The signed acceptance of the actual emitted equations has zero bias.

    theorem equationBias_eq_zero (i₀ : I) (assignment : Address i₀ → Bool) :
    equationBias i₀ assignment = 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.Address, OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.equationBias

  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 347
  46. abbrev OAI.UniqueGamesTheorem.Outer.Clone100Counting.Index line 366
  47. abbrev OAI.UniqueGamesTheorem.Outer.Clone100Counting.Triple line 367
  48. def OAI.UniqueGamesTheorem.Outer.Clone100Counting.sign line 369
  49. def OAI.UniqueGamesTheorem.Outer.Clone100Counting.bias line 371
  50. def OAI.UniqueGamesTheorem.Outer.Clone100Counting.majorityBit line 374

    Source documentation

    A deterministic majority, resolving a zero bias to false.

    def majorityBit (f : Index → Bool) : Bool := decide (bias f < 0)

    Mentions: OAI.UniqueGamesTheorem.Outer.Clone100Counting.Index, OAI.UniqueGamesTheorem.Outer.Clone100Counting.bias

  51. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.majority_aligned_nonneg line 376
  52. def OAI.UniqueGamesTheorem.Outer.Clone100Counting.parityIndicator line 383
  53. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.parityIndicator_nonneg line 386
  54. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.parityIndicator_le_one line 391
  55. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.parityIndicator_eq line 396
  56. def OAI.UniqueGamesTheorem.Outer.Clone100Counting.unconditionedScore line 402
  57. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.independent_product_sum line 405
  58. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.unconditionedScore_eq line 414
  59. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.unconditionedScore_le_one line 434
  60. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.signed_product_of_failure line 442
  61. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.unconditionedScore_le_half_of_failure line 451

    Source documentation

    An equation violated by the majority assignment is satisfied by independent clone labels with probability at most one half. This also allows repeated original variable names: independence belongs to the sampled clone indices.

    theorem unconditionedScore_le_half_of_failure (p q r : Index → Bool) (rhs : Bool)
    (h : (xor (xor (majorityBit p) (majorityBit q)) (majorityBit r) == rhs) = false) :
    unconditionedScore p q r rhs ≤ 1 / 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Outer.Clone100Counting.Index, OAI.UniqueGamesTheorem.Outer.Clone100Counting.majorityBit, OAI.UniqueGamesTheorem.Outer.Clone100Counting.unconditionedScore

  62. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.unconditionedScore_le line 462
  63. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.condition_970200_le line 485

    Source documentation

    Conditioning a bounded function onto 970200 of one million outcomes changes its upper expectation by at most 3/100. The exact loss is 298/10000. Only finite sums and the actual accepted sample cardinality are needed.

    theorem condition_970200_le {T : Type*} [Fintype T]
    (good : T → Prop) [DecidablePred good]
    (_hT : Fintype.card T = 1000000)
    (hgood : Fintype.card {t : T // good t} = 970200)
    (f : T → ℚ) (hf0 : ∀ t, 0 ≤ f t) (hf1 : ∀ t, f t ≤ 1) :
    (∑ t : {t : T // good t}, f t.val) / 970200 ≤
      (∑ t : T, f t) / 1000000 + 3 / 100 := by
…
  64. def OAI.UniqueGamesTheorem.Outer.Clone100Counting.conditionedScore line 504
  65. theorem OAI.UniqueGamesTheorem.Outer.Clone100Counting.conditionedScore_le line 509