OAI/Computability/MaxCut/PCP/Occurrences.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

Executable radix numbering of padded global long-code tables and an ordered equation occurrence list. The code enumerates random tapes, not distinct equations: coinciding equations and repeated variable occurrences are retained.

  1. structure OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding line 20

    Source documentation

    A concrete, reversible finite encoding. Constructors below specify the actual arithmetic; no arbitrary Fintype.equivFin is used.

    structure Encoding (α : Type) where
…
  2. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.fin line 26
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.bool line 27
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.unit line 28
  5. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.prod line 31

    Source documentation

    The second component is the low-order block coordinate.

    def prod {α β : Type} (a : Encoding α) (b : Encoding β) : Encoding (α × β) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding

  6. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.sum line 35

    Source documentation

    The right summand follows the whole left block.

    def sum {α β : Type} (a : Encoding α) (b : Encoding β) : Encoding (α ⊕ β) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding

  7. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.function line 39

    Source documentation

    Function coordinate zero is the least significant radix digit.

    def function {α β : Type} (a : Encoding α) (b : Encoding β) : Encoding (α → β) where
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding

  8. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 47
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 49
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 52
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 56
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 59
  13. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.GlobalKey line 67

    Source documentation

    Distinct table vertices and the three side tags never share storage. Unused ambient query positions are harmless explicit padding.

    abbrev GlobalKey (V C I J : Type) := (V × Cube I) ⊕ ((C × Cube J) ⊕ Unit)

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube

  14. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.globalEncoding line 69
  15. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 75
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendRestricted line 81

    Source documentation

    Extending by false gives a unique padded address to a restricted query.

    def extendRestricted {J : Type} (valid : J → Bool)
    (f : Cube {j : J // valid j = true}) : Cube J :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube

  17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 85
  18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 89
  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 96
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 102
  21. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 109

    Source documentation

    The global index map is an explicit equivalence, including all padding.

    def assignmentOfKey {V C I J : Type}
    (v : Encoding V) (c : Encoding C) (i : Encoding I) (j : Encoding J)
    (bits : GlobalKey V C I J → Bool) : Fin (globalEncoding v c i j).size → Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.GlobalKey, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.globalEncoding

  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 114
  23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 120
  24. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.localAddress line 132
  25. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.localAddress_injective line 139
  26. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 164
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 173
  28. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.findValid line 203

    Source documentation

    A terminating first-valid search on the explicitly ordered ambient list.

    def findValid {J : Type} (valid : J → Bool) : List J → Option {j : J // valid j = true}
  | [] => none
  | j :: rest => if h : valid j = true then some ⟨j, h⟩ else findValid valid rest
  29. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 207
  30. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.firstValid line 216
  31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 219
  32. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.occurrenceList line 225

    Source documentation

    Mapping the ordered enumeration preserves all sampled occurrences.

    def occurrenceList {Tape Name : Type} (tape : Encoding Tape)
    (emit : Tape → Equation Name) : List (Equation Name) := tape.enumerate.map emit

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding

  33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 228
  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum_inline_SourceOccurrences line 232
  35. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.countP_enumerate line 238
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 247

    Source documentation

    Exact satisfaction fraction of the actual ordered equation list equals the uniform random-tape expectation, even when equations or addresses repeat.

    theorem occurrenceList_acceptance {Tape Name : Type} [Fintype Tape]
    (tape : Encoding Tape) (emit : Tape → Equation Name) (bits : Name → Bool) :
    ((occurrenceList tape emit).countP (fun e => satisfied e bits) : ℝ) /
        (occurrenceList tape emit).length =
      𝔼 x, if satisfied (emit x) bits then (1 : ℝ) else 0 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.occurrenceList

  37. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 260
  38. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.slotEncoding line 262
  39. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.iEncoding line 270
  40. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.jEncoding line 271
  41. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.variableEncoding line 272
  42. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.clauseEncoding line 274
  43. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 276
  44. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.proofEncoding line 279
  45. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.nBits line 283
  46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.nBits_eq line 285
  47. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.dummyIndex line 289
  48. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.leftAnchor line 292
  49. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rightAnchor line 294
  50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 297
  51. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 303

    Source documentation

    Independent actual half-tables extend to the explicit padded key space. Only the canonically selected right anchor is read at each clause context.

    def halfTableKeyAssignment (F : Target.Formula) (u : ℕ)
    (a : VariableContext F u → HalfCube (leftAnchor u) → Bool)
    (b : ∀ c : ClauseContext F u, ∀ j₀ : {j : J u // validJ F c j = true},
      HalfCube j₀ → Bool) :
    GlobalKey (VariableContext F u) (ClauseContext F u) (I u) (J u) → Bool
  | .inl (v, f) => a v (canonicalInput (leftAnchor u) f)
  | .inr (.inl (c, g)) =>
    match rightAnchor F c with
    | none => false
    | some j₀ => b c j₀ (canonicalInput j₀ (restrictQuery (validJ F c) g))
  | .inr (.inr _) => false

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.leftAnchor, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.GlobalKey, OAI.MaxCutGames.Foundations.Hastad.canonicalInput, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rightAnchor, OAI.MaxCutGames.Foundations.Hastad.restrictQuery

  52. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendHalfTables line 315
  53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 322
  54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 333
  55. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.emptyAddress line 350
  56. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.contextEquation line 357

    Source documentation

    The private query law depends only on the two visible contexts. In particular, the hidden sampled slots are not inputs to pi.

    def contextEquation (F : Target.Formula) (u D : ℕ)
    (c : ClauseContext F u) (v : VariableContext F u)
    (t : SourceTape.TestTape (I u) (J u) D) : Equation (Fin (nBits F u)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.nBits

  57. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.leftResponse line 366
  58. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rightResponse line 370
  59. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 377
  60. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 394
  61. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.SourceIndex line 398
  62. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 401
  63. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceEquation line 404
  64. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rawSourceList line 410

    Source documentation

    The entire finite random-tape population, including repeated visible contexts and all equation multiplicities, in a fixed explicit order.

    def rawSourceList (F : Target.Formula) (u D : ℕ) : List (Equation (Fin (nBits F u))) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.nBits

  65. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 413
  66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 420
  67. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 445

    Source documentation

    A satisfiable totalization for the empty input formula, without changing or diluting the occurrence list of a nonempty formula.

    def emptyFormulaEquation (F : Target.Formula) (u : ℕ) : Equation (Fin (nBits F u)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.nBits

  68. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceList line 448
  69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceList_empty line 451
  70. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 454
  71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 460
  72. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 469
  73. def OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.sourceInput line 480
  74. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 484
  75. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_pair line 497
  76. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_mk line 505
  77. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_prod line 523

    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.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding, OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate

  78. theorem OAI.MaxCutGames.Foundations.Hastad.SourceOccurrences.Encoding.map_enumerate_prod line 538
  79. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEnumeration.testTapeEncoding_enumerate line 551

    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
…
  80. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_enumerate line 559
  81. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_map line 570
  82. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEnumeration.rawSourceList_eq_nestedLoops line 583

    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
…
  83. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEnumeration.sourceList_eq_nestedLoops line 593
  84. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEnumeration.rawSourceList_flatMap line 606

    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 : MaxCutGames.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.MaxCutGames.Reduction.CloneGap.Equation

  85. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.variable_rank line 627
  86. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.clause_rank line 631
  87. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.left_address line 635
  88. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.right_address line 640
  89. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.dummy_address line 646
  90. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.left_address_radix line 653
  91. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.right_address_radix line 660
  92. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressArithmetic.nBits_eq_dummy_succ line 668
  93. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.Position line 679
  94. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.NameProfile line 680
  95. structure OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.Signature line 684

    Source documentation

    All local control data have sizes determined solely by the repetition parameter. Global variable and clause indices are absent.

    structure Signature (u : ℕ) where
…
  96. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureEquiv line 690
  97. instance OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureFintype line 697
  98. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.card_position line 701
  99. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.card_signature line 705

    Source documentation

    A finite control alphabet bound, not a claim about evaluation time.

    theorem card_signature (u : ℕ) :
    Fintype.card (Signature u) =
      2 ^ (3 * u) * ((2 ^ (3 * u)) ^ (3 * u) * 3 ^ u) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.Signature

  100. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.positiveAt line 711
  101. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.occurrenceName line 716
  102. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.contextNameProfile line 722

    Source documentation

    The equality matrix can be supplied by a separate field-comparison procedure after an explicit reindexing of the 3*u positions.

    def contextNameProfile (F : Formula) {u : ℕ} (c : ClauseContext F u) : NameProfile u :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.NameProfile

  103. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext line 725
  104. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext_signs line 731
  105. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext_sameName line 735
  106. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext_selected line 740
  107. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureSatisfies line 744

    Source documentation

    Local clause truth is computed from signs and the three answer bits.

    def signatureSatisfies {u : ℕ} (σ : Signature u) (j : J u) (t : Fin u) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.Signature

  108. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureValid line 749
  109. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureSatisfies_ofContext line 754
  110. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signature_validJ line 761

    Source documentation

    Exact equality with the actual contextual validity predicate, for every answer tuple, including repeated «variables» within or across clauses.

    theorem signature_validJ (F : Formula) {u : ℕ} (c : ClauseContext F u)
    (s : SlotContext u) (j : J u) :
    signatureValid (ofContext F c s) j = validJ F c j := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureValid, OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext

  111. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot line 786

    Source documentation

    The first slot matching the visible selected name, computed using only the equality matrix. The selected slot guarantees visible support.

    def signatureCanonicalSlot {u : ℕ} (σ : Signature u) (t : Fin u) : Slot :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.Signature

  112. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureProjection line 790
  113. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot_ofContext line 793
  114. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signature_pi line 810

    Source documentation

    The actual canonical projection factors through the finite signature on every label, without a validity hypothesis.

    theorem signature_pi (F : Formula) {u : ℕ} (c : ClauseContext F u)
    (s : SlotContext u) (j : J u) :
    signatureProjection (ofContext F c s) j = pi F c (sampledVariables F c s) j := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureProjection, OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext

  115. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signature_projection_selected line 818

    Source documentation

    On valid labels, canonical projection also agrees with the actual selected occurrence answers.

    theorem signature_projection_selected (F : Formula) {u : ℕ}
    (c : ClauseContext F u) (s : SlotContext u) (j : J u)
    (hj : signatureValid (ofContext F c s) j = true) :
    signatureProjection (ofContext F c s) j = fun t => answerAt (j t) (s t) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureValid, OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext, OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.signatureProjection

  116. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.validJ_eq_of_signature_eq line 829

    Source documentation

    The same finite signature gives the same validity decision even across formulas having different global index types.

    theorem validJ_eq_of_signature_eq (F G : Formula) {u : ℕ}
    (c : ClauseContext F u) (d : ClauseContext G u) (s s' : SlotContext u)
    (h : ofContext F c s = ofContext G d s') (j : J u) :
    validJ F c j = validJ G d j := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.ofContext

  117. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalSignature.pi_eq_of_signature_eq line 835