OAI/Computability/UniqueGames/PCP/SourceAddressArithmeticLemmas.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.variable_rank line 17
2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.clause_rank line 21
3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.left_address line 25
4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.right_address line 30
5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.dummy_address line 36
6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.left_address_radix line 43
7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.right_address_radix line 50
8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressArithmetic.nBits_eq_dummy_succ line 58
9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.formulaBits_length line 74
10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 82
11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 87
12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 92
13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.bitCountFormula line 98

    Source documentation

    The two padded long-code tables and one global dummy bit.

    def bitCountFormula (n m u : ℕ) : ℕ :=
    …

14. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.bitCoefficient line 102

    Source documentation

    Depends on the fixed repetition count alone.

    def bitCoefficient (u : ℕ) : ℕ := 2 ^ (2 ^ u) + 2 ^ (8 ^ u) + 1

15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.testCoefficient line 106

    Source documentation

    The slot tuples, two queries, and noise tapes per clause tuple. The empty-context branch uses the global dummy and adds no random tape.

    def testCoefficient (u D : ℕ) : ℕ :=
    …

16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 110

    Source documentation

    The total encoding also handles an empty formula with one dummy equation.

    def occurrenceCoefficient (u D : ℕ) : ℕ := testCoefficient u D + 1

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.testCoefficient

17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.one_le_input_power line 112
18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 118
19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 133
20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 143
21. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.sourceSizeBound line 152
22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.sourceBits_length_le line 155
23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.sourcePolynomial line 166

    Source documentation

    One explicit output-length polynomial for each fixed u,D.

    noncomputable def sourcePolynomial (u D : ℕ) : Polynomial ℕ :=
    …

24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 171
25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.card_testTape line 179

    Source documentation

    Exact cardinality of the actual fixed query/noise tape.

    theorem card_testTape (u D : ℕ) :
        Fintype.card (SourceTape.TestTape (I u) (J u) D) =
          2 ^ (2 ^ u) * (D ^ (8 ^ u) * 2 ^ (8 ^ u)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape

26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 185

    Source documentation

    The executable radix enumeration has the same fixed size.

    theorem testTapeEncoding_size (u D : ℕ) :
        (SourceOccurrences.testTapeEncoding u D).size =
          2 ^ (2 ^ u) * (D ^ (8 ^ u) * 2 ^ (8 ^ u)) := rfl

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.testTapeEncoding

27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.card_sourceIndex line 190

    Source documentation

    Cardinality of the actual complete random-tape population.

    theorem card_sourceIndex (F : Formula) (u D : ℕ) :
        Fintype.card (SourceIndex F u D) =
          (F.clauses.length ^ u * 3 ^ u) *
            (2 ^ (2 ^ u) * (D ^ (8 ^ u) * 2 ^ (8 ^ u))) := by
    …

28. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.nBits_le_input line 198

    Source documentation

    Bound on the actual variable count, including padded addresses and dummy.

    theorem nBits_le_input (F : Formula) (u : ℕ) :
        nBits F u ≤ bitCoefficient u * (Complexity.formulaBits F).length ^ u := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.bitCoefficient, OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

29. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 204

    Source documentation

    Exact list size retains every repeated sampled context and equation.

    theorem rawSourceList_length_eq (F : Formula) (u D : ℕ) :
        (rawSourceList F u D).length = testCoefficient u D * F.clauses.length ^ u := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.testCoefficient

30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 210
31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 218

    Source documentation

    Bound on the total actual list, also covering the empty-formula branch.

    theorem sourceList_length_le_input (F : Formula) (u D : ℕ) :
        (sourceList F u D).length ≤
          occurrenceCoefficient u D * (Complexity.formulaBits F).length ^ u := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.occurrenceCoefficient, OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 228
33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 237

    Source documentation

    Fixed parameters supply one polynomial uniformly for all actual inputs.

    theorem fixed_parameters_source_size (u D : ℕ) (hD : 0 < D) :
        ∃ p : Polynomial ℕ, ∀ F : Formula,
          (SourceEncoding.inputBits (sourceInput F u D hD)).length ≤
            p.eval (Complexity.formulaBits F).length :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_pair line 253
35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_mk line 261
36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_prod line 279

    Source documentation

    Increasing product rank enumerates the first factor outside and the second factor inside, including when either factor is empty.

    theorem enumerate_prod (a : Encoding α) (b : Encoding β) :
        (a.prod b).enumerate =
          a.enumerate.flatMap (fun x => b.enumerate.map (fun y => (x, y))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.enumerate

37. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceOccurrences.Encoding.map_enumerate_prod line 294
38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEnumeration.testTapeEncoding_enumerate line 307

    Source documentation

    The exact tape order is left query, noise assignment, right query.

    theorem testTapeEncoding_enumerate (u D : ℕ) :
        (testTapeEncoding u D).enumerate =
          ((iEncoding u).function Encoding.bool).enumerate.flatMap (fun f =>
            ((jEncoding u).function (Encoding.fin D)).enumerate.flatMap (fun z =>
              ((jEncoding u).function Encoding.bool).enumerate.map (fun g => (f, z, g)))) := by
    …

39. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_enumerate line 315
40. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_map line 326
41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEnumeration.rawSourceList_eq_nestedLoops line 339

    Source documentation

    The concrete equation list is exactly a nest of finite emitting loops.

    theorem rawSourceList_eq_nestedLoops (F : Formula) (u D : ℕ) :
        rawSourceList F u D =
          (clauseEncoding F u).enumerate.flatMap (fun c =>
            (slotContextEncoding u).enumerate.flatMap (fun s =>
              ((iEncoding u).function Encoding.bool).enumerate.flatMap (fun f =>
                ((jEncoding u).function (Encoding.fin D)).enumerate.flatMap (fun z =>
                  ((jEncoding u).function Encoding.bool).enumerate.map
                    (fun g => contextEquation F u D c (sampledVariables F c s) (f, z, g)))))) := by
    …

42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEnumeration.sourceList_eq_nestedLoops line 349
43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEnumeration.rawSourceList_flatMap line 362

    Source documentation

    An output-word encoder can be concatenated directly in the same order. This is an algebraic serialization identity, not a machine realization.

    theorem rawSourceList_flatMap {α : Type} (F : Formula) (u D : ℕ)
        (emit : UniqueGamesTheorem.Reduction.CloneGap.Equation (Fin (nBits F u)) → List α) :
        (rawSourceList F u D).flatMap emit =
          (clauseEncoding F u).enumerate.flatMap (fun c =>
            (slotContextEncoding u).enumerate.flatMap (fun s =>
              ((iEncoding u).function Encoding.bool).enumerate.flatMap (fun f =>
                ((jEncoding u).function (Encoding.fin D)).enumerate.flatMap (fun z =>
                  ((jEncoding u).function Encoding.bool).enumerate.flatMap
                    (fun g => emit (contextEquation F u D c (sampledVariables F c s) (f, z, g))))))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation