OAI/Computability/MaxCut/Encoding/TableKeysGame.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Restore actual orbit labels as a total function of the entire reduced key. The arbitrary value at unrealized orbit bodies is used only to make this function total; every table queried by the verifier and by the sparse experiment is proved to be an actual realization. Folding holds even for the total extension, because the removed intercept is always restored.

  1. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.Question line 13
  2. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.Map line 14
  3. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.Dual line 15
  4. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.Query line 16
  5. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.canonical line 17
  6. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.Vertex line 20

    Source documentation

    One realized key orbit, with no prover-side copy.

    abbrev Vertex (S : Source) (k s d : Nat) := ActualGame.Vertex S k s d
  7. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.vertex line 21
  8. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.offset line 22
  9. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.shiftQuery line 23
  10. def OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount line 25
  11. def OAI.MaxCutGames.Decoder.TableKeysGame.vertexEncoding line 28
  12. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.Outcome line 32

    Source documentation

    All four sampling choices remain separate occurrence indices.

    abbrev Outcome (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d) :=
…
  13. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.leftQuery line 35
  14. abbrev OAI.MaxCutGames.Decoder.TableKeysGame.rightQuery line 37
  15. def OAI.MaxCutGames.Decoder.TableKeysGame.edge line 40
  16. def OAI.MaxCutGames.Decoder.TableKeysGame.outcomes line 47
  17. def OAI.MaxCutGames.Decoder.TableKeysGame.outputInstance line 50
  18. theorem OAI.MaxCutGames.Decoder.TableKeysGame.outputInstance_constraints_length line 62
  19. def OAI.MaxCutGames.Decoder.TableKeysGame.vertexLabel line 67
  20. def OAI.MaxCutGames.Decoder.TableKeysGame.labelingOf line 72
  21. theorem OAI.MaxCutGames.Decoder.TableKeysGame.vertexLabel_labelingOf line 77
  22. def OAI.MaxCutGames.Decoder.TableKeysGame.unfolded line 84

    Source documentation

    Restore the removed alphabet component of the affine intercept.

    noncomputable def unfolded (S : Source) (k s d : Nat)
    (labeling : Fin (vertexCount S k s d) → Fin (2^s))
    (q : Query S k s d) : Alphabet s :=
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysGame.Query

  23. theorem OAI.MaxCutGames.Decoder.TableKeysGame.unfolded_equivariant line 89
  24. theorem OAI.MaxCutGames.Decoder.TableKeysGame.edge_satisfied_iff line 100
  25. def OAI.MaxCutGames.Decoder.TableKeysGame.acceptanceProbability line 114
  26. theorem OAI.MaxCutGames.Decoder.TableKeysGame.acceptanceProbability_eq_test line 118
  27. theorem OAI.MaxCutGames.Decoder.TableKeysGame.countSatisfied_map_inline_TableKeysGame line 130
  28. theorem OAI.MaxCutGames.Decoder.TableKeysGame.countSatisfied_eq_sum line 138
  29. theorem OAI.MaxCutGames.Decoder.TableKeysGame.acceptanceProbability_eq_count line 147

    Source documentation

    The test probability is the satisfied fraction of the actual occurrence list.

    theorem acceptanceProbability_eq_count (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 =
      (countSatisfied labeling (outputInstance S k g).constraints : ℚ) /
        (outputInstance S k g).constraints.length := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysGame.acceptanceProbability, OAI.MaxCutGames.Decoder.TableKeysGame.outputInstance

  30. def OAI.MaxCutGames.Decoder.TableKeysGame.explicitVertexCount line 158

    Source documentation

    Exhaustive numbering of the same single-orbit vertex type.

    def explicitVertexCount (S : Source) (k s d : Nat) : Nat :=
…
  31. def OAI.MaxCutGames.Decoder.TableKeysGame.explicitVertexEncoding line 161
  32. def OAI.MaxCutGames.Decoder.TableKeysGame.semanticToExplicitVertices line 167
  33. theorem OAI.MaxCutGames.Decoder.TableKeysGame.semanticToExplicitVertices_apply line 171
  34. theorem OAI.MaxCutGames.Decoder.TableKeysGame.explicitVertexCount_eq line 177
  35. def OAI.MaxCutGames.Decoder.TableKeysGame.explicitEdge line 181
  36. theorem OAI.MaxCutGames.Decoder.TableKeysGame.explicitEdge_eq_rename line 188
  37. def OAI.MaxCutGames.Decoder.TableKeysGame.outputInstanceWithEnumeration line 196

    Source documentation

    Executable finite output, still allowing loops and parallel occurrences.

    def outputInstanceWithEnumeration (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) : Instance (2^s) where
…
  38. theorem OAI.MaxCutGames.Decoder.TableKeysGame.outputInstanceWithEnumeration_length line 209
  39. theorem OAI.MaxCutGames.Decoder.TableKeysGame.explicitConstraints_perm_renamed line 216
  40. theorem OAI.MaxCutGames.Decoder.TableKeysGame.completeAt_outputInstanceWithEnumeration_iff line 225
  41. theorem OAI.MaxCutGames.Decoder.TableKeysGame.soundAt_outputInstanceWithEnumeration_iff line 233
  42. def OAI.MaxCutGames.Decoder.TableKeysRestoration.extendedLabel line 265
  43. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.extendedLabel_actual line 269
  44. def OAI.MaxCutGames.Decoder.TableKeysRestoration.restoredData line 276

    Source documentation

    Restore the full affine intercept after labeling the orbit body.

    def restoredData (can : Q → Ambient s d × T)
    (label : ActualOrbit.Vertex can → Alphabet s) (D : Ambient s d × T) : Alphabet s :=
…
  45. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.restoredData_actual line 280
  46. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.restoredData_shift line 287
  47. def OAI.MaxCutGames.Decoder.TableKeysRestoration.keyAnswer line 296

    Source documentation

    The actual verifier labeling, viewed as a function of exact affine keys.

    def keyAnswer (S : Source) (k s d : Nat)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (D : TableKeys.Key k (Fin S.«variables») (Fin S.occurrences) (Ambient s d)) : Alphabet s :=
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeys.Key

  48. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.keyAnswer_actual line 302
  49. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.keyAnswer_shift line 309
  50. def OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer line 316
  51. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer_pullback line 326

    Source documentation

    No extra consistency predicate: projected answers equal full-query answers for every table and every compatible hidden extension.

    theorem projectedAnswer_pullback (S : Source) (k s d : Nat)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (occ : Fin k → Fin S.occurrences)
    (slot : Fin k → PartnerProjection.Slot)
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] Ambient s d) :
    projectedAnswer S k s d labeling J
        (RawPrivateTable.supported J (ActualGame.names S) occ slot) Y =
      TableKeysGame.unfolded S k s d labeling
        (occ, Y.comp (RawPrivateTable.projection J (ActualGame.rhs S) occ slot)) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer, OAI.MaxCutGames.Decoder.TableKeysGame.unfolded

  52. theorem OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer_fold line 342

    Source documentation

    The visible table has the exact same affine folding law, with its genuine homogeneous coordinate rather than an assumed or reconstructed first bit.

    theorem projectedAnswer_fold (S : Source) (k s d : Nat)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (O : RawPrivateTable.SupportedV J (ActualGame.names S))
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] Ambient s d) (c : Alphabet s) :
    projectedAnswer S k s d labeling J O
        (Y + (TableKeys.visibleTau J).smulRight (c, (0 : Vector d))) =
      projectedAnswer S k s d labeling J O Y + c := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer, OAI.MaxCutGames.Decoder.TableKeys.visibleTau

  53. theorem OAI.MaxCutGames.Decoder.TableKeysPrivateRow.assemble_prod_shift line 376
  54. def OAI.MaxCutGames.Decoder.TableKeysPrivateRow.rowAnswer line 393

    Source documentation

    The right player's actual private table, formed from visible row advice.

    def rowAnswer (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k))
    (Q : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow

  55. theorem OAI.MaxCutGames.Decoder.TableKeysPrivateRow.rowAnswer_fold line 405

    Source documentation

    Folding on the hidden kernel is a consequence of the exact key action.

    theorem rowAnswer_fold (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (Q : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow

  56. theorem OAI.MaxCutGames.Decoder.TableKeysPrivateRow.rowAnswer_actual line 419

    Source documentation

    At the actual hidden matrix this row table is exactly the projected table used by the verifier, with the same complement and the same complete key.

    theorem rowAnswer_actual (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (Q : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (M : RawPartnerTarget.RawPoint J →ₗ[F2] Alphabet s)
    (T : RawPartnerTarget.RawPoint J →ₗ[F2] Vector d) :
    rowAnswer S labeling J Q A (AdviceFibers.observe A M) T
        (AdviceFibers.hiddenCoordinate A M) =
      TableKeysRestoration.projectedAnswer S k s d labeling J Q (M.prod T) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysPrivateRow.rowAnswer, OAI.MaxCutGames.Decoder.AdviceFibers.observe, OAI.MaxCutGames.Decoder.AdviceFibers.hiddenCoordinate, OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer

  57. def OAI.MaxCutGames.Decoder.TableKeysPrivateRow.targetIntercept line 436

    Source documentation

    This intercept is determined once the visible base and affine witness are fixed; it is not silently erased when decoding from a row fiber.

    def targetIntercept (J : Finset (Fin k)) (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow

  58. theorem OAI.MaxCutGames.Decoder.TableKeysPrivateRow.affine_target_on_row line 441