OAI/Computability/MaxCut/Encoding/TableKeysCompleteness.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Completeness of the v2 single-orbit matrix game. The generic finite-average calculation is shared with the proved actual completeness calculation. Its reuse is justified below by pointwise equality of restored answers under diagonal labels; the output vertices themselves are never doubled.

No gadget existence, dispersion hypothesis, inverse theorem, or legacy soundness theorem is a premise. The bound includes the exact fair-bit factor 1 / 2, and is a statement about the actual finite edge occurrence list.

  1. def OAI.MaxCutGames.Decoder.TableKeysCompleteness.diagonalLabeling line 29

    Source documentation

    Use a single label function on both auxiliary sides, solely to share the already proved finite-average calculation. This does not change the v2 game.

    def diagonalLabeling (S : Source) (k s d : Nat)
    (labeling : Fin (vertexCount S k s d) → Fin (2^s)) :
    Fin (ActualGame.vertexCount S k s d) → Fin (2^s) :=
…
  2. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.diagonal_unfolded line 34
  3. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.acceptanceProbability_eq_diagonal line 43

    Source documentation

    Pointwise-identical matrix tests have exactly the same acceptance average.

    theorem acceptanceProbability_eq_diagonal (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (labeling : Fin (vertexCount S k s d) → Fin (2^s)) :
    acceptanceProbability S k g labeling =
      ActualGame.acceptanceProbability S k g (diagonalLabeling S k s d labeling) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysCompleteness.diagonalLabeling

  4. def OAI.MaxCutGames.Decoder.TableKeysCompleteness.honestLabeling line 50
  5. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.diagonal_honestLabeling line 54
  6. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.honest_unfolded line 62

    Source documentation

    The removed affine intercept is recovered by gadget equivariance.

    theorem honest_unfolded (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.«variables» → Bool) (q : Query S k s d) :
    unfolded S k s d (honestLabeling S k g A) q =
      g.f (ActualCompleteness.evaluate (ActualGame.names S) (fun n => ofBit (A n))
        (canonical S k s d q)) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysCompleteness.honestLabeling

  7. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.honest_unfolded_valid line 72

    Source documentation

    On a satisfied tuple, every sampled table evaluates the same homogeneous answer with first coordinate one.

    theorem honest_unfolded_valid (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.«variables» → Bool) (q : Query S k s d)
    (hgood : ∀ j, S.satisfied A (q.1 j) = true) :
    unfolded S k s d (honestLabeling S k g A) q =
      g.f (q.2 (ActualCompleteness.sourcePoint S k A q.1)) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysCompleteness.honestLabeling

  8. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.honest_acceptance_bound line 80
  9. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.honest_acceptance_of_bounds line 87
  10. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.honest_satisfied_fraction_bound line 97

    Source documentation

    Completeness is measured on the generated single-orbit edge occurrences.

    theorem honest_satisfied_fraction_bound (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.«variables» → Bool) :
    1 - (k : ℚ) * S.failure A - g.stabilityError / 2 ≤
      (countSatisfied (honestLabeling S k g A)
        (outputInstance S k g).constraints : ℚ) /
        (outputInstance S k g).constraints.length := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysCompleteness.honestLabeling

  11. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.completeAt line 106
  12. theorem OAI.MaxCutGames.Decoder.TableKeysCompleteness.completeAt_withEnumeration line 120
  13. abbrev OAI.MaxCutGames.Reduction.CanonicalEncoding.Ambient line 143
  14. abbrev OAI.MaxCutGames.Reduction.CanonicalEncoding.Record line 144
  15. abbrev OAI.MaxCutGames.Reduction.CanonicalEncoding.Body line 145
  16. def OAI.MaxCutGames.Reduction.CanonicalEncoding.vectorWord line 147
  17. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.vectorWord_lt line 150
  18. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.vectorWord_injective line 153
  19. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.vectorWord_eq_iff line 159
  20. def OAI.MaxCutGames.Reduction.CanonicalEncoding.recordWords line 164

    Source documentation

    Words: tag, name, occurrence, followed by three split coefficient pairs. Padding is zero. A single record uses only the first coefficient pair.

    def recordWords {n m s d : Nat} : Record n m s d → List Nat
  | .blank => [0, 0, 0, 0, 0, 0, 0, 0, 0]
  | .single name coefficient =>
      [1, name.val, 0, vectorWord coefficient.1, vectorWord coefficient.2, 0, 0, 0, 0]
  | .full occurrence coefficients =>
      [2, 0, occurrence.val,
        vectorWord (coefficients 0).1, vectorWord (coefficients 0).2,
        vectorWord (coefficients 1).1, vectorWord (coefficients 1).2,
        vectorWord (coefficients 2).1, vectorWord (coefficients 2).2]

    Mentions: OAI.MaxCutGames.Reduction.CanonicalEncoding.Record, OAI.MaxCutGames.Reduction.CanonicalEncoding.vectorWord

  21. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordWords_length line 174
  22. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordWords_injective line 178
  23. def OAI.MaxCutGames.Reduction.CanonicalEncoding.recordsWords line 213
  24. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordsWords_nil line 216
  25. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordsWords_cons line 219
  26. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordsWords_length line 223
  27. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordsWords_take_head line 229
  28. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordsWords_injective line 236
  29. def OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyWords line 264
  30. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyWords_length line 267
  31. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyWords_injective line 271
  32. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyWords_eq_iff line 279
  33. def OAI.MaxCutGames.Reduction.CanonicalEncoding.wordBound line 282
  34. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.recordWords_bounded line 284
  35. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyWords_bounded line 309
  36. def OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyBits line 320
  37. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyBits_injective line 323
  38. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyBits_eq_iff line 328
  39. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyBits_length_le line 331
  40. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.imageVertices_bodyWords line 337

    Source documentation

    Serializing before deduplication preserves the exact retained vertex order.

    theorem imageVertices_bodyWords {Q : Type*} {n m k s d : Nat}
    [DecidableEq (Body n m k s d)] (queries : List Q) (body : Q → Body n m k s d) :
    Encoding.imageVertices queries (fun q => bodyWords (body q)) =
      (Encoding.imageVertices queries body).map bodyWords := by
…

    Mentions: OAI.MaxCutGames.Reduction.CanonicalEncoding.Body, OAI.MaxCutGames.Reduction.Encoding.imageVertices, OAI.MaxCutGames.Reduction.CanonicalEncoding.bodyWords

  41. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.imageVertices_bodyBits line 345
  42. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.idxOf_map_injective line 353
  43. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.imageIndex_map_val line 367

    Source documentation

    Injective serialization leaves the actual numeric vertex index unchanged, not just the vertex set or its cardinality.

    theorem imageIndex_map_val {Q A B : Type*} [DecidableEq A] [DecidableEq B]
    (queries : List Q) (body : Q → A) (f : A → B) (hf : Function.Injective f)
    (q : Q) (hq : q ∈ queries) :
    (Encoding.imageIndex queries (fun q => f (body q)) q hq).val =
      (Encoding.imageIndex queries body q hq).val := by
…

    Mentions: OAI.MaxCutGames.Reduction.Encoding.imageIndex

  44. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.imageIndex_bodyWords_val line 381
  45. theorem OAI.MaxCutGames.Reduction.CanonicalEncoding.imageIndex_bodyBits_val line 388