OAI/Computability/MaxCut/PCP/Folding.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Hastad.cubeFlip line 18
2. theorem OAI.MaxCutGames.Foundations.Hastad.cubeFlip_cubeFlip line 21
3. theorem OAI.MaxCutGames.Foundations.Hastad.bitSign_not line 25
4. theorem OAI.MaxCutGames.Foundations.Hastad.sum_cubeFlip line 28
5. theorem OAI.MaxCutGames.Foundations.Hastad.coefficient_zero_of_odd line 40
6. theorem OAI.MaxCutGames.Foundations.Hastad.coefficient_sign_zero_of_folded line 49
7. def OAI.MaxCutGames.Foundations.Hastad.representative line 56
8. theorem OAI.MaxCutGames.Foundations.Hastad.representative_at line 60
9. theorem OAI.MaxCutGames.Foundations.Hastad.representative_flip line 65
10. abbrev OAI.MaxCutGames.Foundations.Hastad.HalfCube line 69
11. def OAI.MaxCutGames.Foundations.Hastad.canonicalInput line 71
12. theorem OAI.MaxCutGames.Foundations.Hastad.canonicalInput_flip line 75
13. def OAI.MaxCutGames.Foundations.Hastad.foldedAnswer line 81

    Source documentation

    One stored bit and one explicit sign correction for every queried table.

    def foldedAnswer (i₀ : I) (table : HalfCube i₀ → Bool) (f : Cube I) : Bool :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.Cube

14. theorem OAI.MaxCutGames.Foundations.Hastad.foldedAnswer_flip line 85
15. theorem OAI.MaxCutGames.Foundations.Hastad.foldedAnswer_zero_coefficient line 93
16. theorem OAI.MaxCutGames.Foundations.Hastad.foldedAnswer_dictator line 98
17. def OAI.MaxCutGames.Foundations.Hastad.coordinateMask line 103
18. def OAI.MaxCutGames.Foundations.Hastad.cubeToggle line 105
19. theorem OAI.MaxCutGames.Foundations.Hastad.cubeToggle_twice line 109
20. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_coordinateMask line 115
21. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_cubeToggle line 125
22. theorem OAI.MaxCutGames.Foundations.Hastad.sum_cubeToggle line 130
23. def OAI.MaxCutGames.Foundations.Hastad.restrictQuery line 143
24. theorem OAI.MaxCutGames.Foundations.Hastad.restrictQuery_cubeToggle line 147
25. theorem OAI.MaxCutGames.Foundations.Hastad.conditioned_coefficient_zero_invalid line 158
26. theorem OAI.MaxCutGames.Foundations.Hastad.conditioned_coefficient_support line 170

    Source documentation

    Every coordinate returned from a nonzero conditioned Fourier mask is an actual valid local assignment, proved from the concrete restriction map.

    theorem conditioned_coefficient_support (valid : I → Bool)
        (B : Cube {i : I // valid i = true} → ℝ) (s : Cube I)
        (hne : coefficient (fun f => B (restrictQuery valid f)) s ≠ 0) :
        ∀ i ∈ support s, valid i = true := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.coefficient, OAI.MaxCutGames.Foundations.Hastad.restrictQuery, OAI.MaxCutGames.Foundations.Hastad.support

27. def OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer line 180
28. theorem OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer_flip line 185
29. theorem OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 192
30. theorem OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer_dictator line 199
31. def OAI.MaxCutGames.Reduction.CloneGap.cart line 211
32. theorem OAI.MaxCutGames.Reduction.CloneGap.count_const line 214
33. theorem OAI.MaxCutGames.Reduction.CloneGap.count_cart line 218
34. theorem OAI.MaxCutGames.Reduction.CloneGap.length_cart line 229
35. theorem OAI.MaxCutGames.Reduction.CloneGap.count_cart_left line 234
36. theorem OAI.MaxCutGames.Reduction.CloneGap.count_cart_right line 238
37. theorem OAI.MaxCutGames.Reduction.CloneGap.count_cart_le line 242
38. theorem OAI.MaxCutGames.Reduction.CloneGap.count_union_le line 255
39. theorem OAI.MaxCutGames.Reduction.CloneGap.count_remove line 263
40. abbrev OAI.MaxCutGames.Reduction.CloneGap.Index line 271
41. def OAI.MaxCutGames.Reduction.CloneGap.indices line 272
42. def OAI.MaxCutGames.Reduction.CloneGap.triples line 273
43. def OAI.MaxCutGames.Reduction.CloneGap.collision line 274
44. def OAI.MaxCutGames.Reduction.CloneGap.distinctTriples line 276
45. theorem OAI.MaxCutGames.Reduction.CloneGap.length_indices line 278
46. theorem OAI.MaxCutGames.Reduction.CloneGap.length_triples line 279
47. theorem OAI.MaxCutGames.Reduction.CloneGap.count_index_eq_le line 282
48. theorem OAI.MaxCutGames.Reduction.CloneGap.count_collision_le line 292
49. theorem OAI.MaxCutGames.Reduction.CloneGap.majority_exists line 321
50. def OAI.MaxCutGames.Reduction.CloneGap.allAgree line 335
51. theorem OAI.MaxCutGames.Reduction.CloneGap.count_agree_distinct line 338
52. structure OAI.MaxCutGames.Reduction.CloneGap.Equation line 355
53. def OAI.MaxCutGames.Reduction.CloneGap.satisfied line 363
54. def OAI.MaxCutGames.Reduction.CloneGap.clone line 366
55. theorem OAI.MaxCutGames.Reduction.CloneGap.lift_preserves line 369
56. theorem OAI.MaxCutGames.Reduction.CloneGap.clone_names_distinct line 372
57. theorem OAI.MaxCutGames.Reduction.CloneGap.agree_failure line 383
58. theorem OAI.MaxCutGames.Reduction.CloneGap.failed_occurrence_clones line 393
59. def OAI.MaxCutGames.Reduction.CloneGap.majorityBit line 409
60. theorem OAI.MaxCutGames.Reduction.CloneGap.majorityBit_count line 411
61. def OAI.MaxCutGames.Reduction.CloneGap.cloneList line 423
62. theorem OAI.MaxCutGames.Reduction.CloneGap.length_cloneList line 426
63. theorem OAI.MaxCutGames.Reduction.CloneGap.cloneList_failure_lower line 435
64. theorem OAI.MaxCutGames.Reduction.CloneGap.clone_gap line 454
65. theorem OAI.MaxCutGames.Reduction.CloneGap.clone_completeness_count line 473
66. abbrev OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.Address line 499

    Source documentation

    Left and right stored tables have disjoint variable names.

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

    Mentions: OAI.MaxCutGames.Foundations.Hastad.HalfCube

67. def OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.storedAssignment line 501
68. def OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.rhsCorrection line 506

    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.MaxCutGames.Foundations.Hastad.Cube

69. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.correction_eq line 510
70. def OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation line 518

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.Address

71. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.xor_corrections line 525
72. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation_satisfied line 533

    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.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.storedAssignment, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer, OAI.MaxCutGames.Foundations.Hastad.thirdQuery

73. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 545
74. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation_indicator line 555
75. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 567

    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
    …

76. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equation_repeated_right line 575
77. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 585
78. def OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation line 593

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.Address

79. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 599
80. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 605
81. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 617
82. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 628
83. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 641
84. def OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equationAcceptance line 655

    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.MaxCutGames.Foundations.Hastad.HalfCube

85. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 661
86. def OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 668
87. theorem OAI.MaxCutGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 675
88. def OAI.MaxCutGames.Foundations.Hastad.mapEquation line 701

    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
    …

89. theorem OAI.MaxCutGames.Foundations.Hastad.satisfied_mapEquation line 708
90. abbrev OAI.MaxCutGames.Foundations.Hastad.EmptyContext.Address line 717

    Source documentation

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

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

    Mentions: OAI.MaxCutGames.Foundations.Hastad.HalfCube

91. def OAI.MaxCutGames.Foundations.Hastad.EmptyContext.storedAssignment line 719
92. def OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation line 723

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.Address

93. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_second_eq_third line 730
94. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_satisfied line 735

    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.MaxCutGames.Foundations.Hastad.EmptyContext.Address, OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer

95. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 744
96. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_flip_first line 751

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation, OAI.MaxCutGames.Foundations.Hastad.cubeFlip

97. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_flip_rhs line 757
98. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 761
99. def OAI.MaxCutGames.Foundations.Hastad.EmptyContext.pairedEquations line 768

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.Address

100. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.pairedEquations_length line 772
101. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 776
102. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 781

     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.MaxCutGames.Foundations.Hastad.EmptyContext.Address, OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.pairedEquations

103. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 788
104. def OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equationAcceptance line 796
105. def OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equationBias line 799
106. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 802
107. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equation_indicator line 807
108. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 815

     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.MaxCutGames.Foundations.Hastad.EmptyContext.Address, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equationAcceptance

109. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 823

     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.MaxCutGames.Foundations.Hastad.EmptyContext.Address, OAI.MaxCutGames.Foundations.Hastad.EmptyContext.equationBias

110. theorem OAI.MaxCutGames.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 834