OAI/Computability/UniqueGames/Decoding/VisiblePoliciesLemmas.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

The actual visible selector used by the stochastic decoder

At fixed labeling, the matrix table depends only on the occurrence question and complement map. Its normalized row/column witness is selected from the observed row map and row value. Transporting this witness through the actual homogeneous coordinates supplies VisiblePolicies.ResponseWitness; the selected target's affine intercept is retained separately, including exact equality on the slice.

  1. structure OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness line 31

    Source documentation

    The part of a normalized affine witness needed by the left sampler.

    structure ResponseWitness (k : ℕ) where
…
  2. def OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.defaultWitness line 36
  3. abbrev OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput line 41
  4. abbrev OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.RightInput line 45
  5. def OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.chosenWitness line 51

    Source documentation

    The witness choice has only the left observation as its variable input.

    def chosenWitness {S : Source}
    (good : LeftInput S k s d R → ResponseWitness k → Prop)
    (q : LeftInput S k s d R) : ResponseWitness k :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness

  6. theorem OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.chosenWitness_spec line 56
  7. def OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.leftPolicy line 63
  8. def OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.pointLaw line 71

    Source documentation

    A fixed valid fallback gives a total policy even on impossible row inputs.

    def pointLaw {X : Type*} [Fintype X] (x : X) : FiniteDistribution X where
…
  9. def OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.rightPolicy line 77

    Source documentation

    The right kernel consumes its own complete visible observation only.

    def rightPolicy (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (J : Finset (Fin k)) (q : RightInput S J s d R) :
    FiniteDistribution (ActualAnswer (TableKeys.visibleTau J)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.RightInput, OAI.UniqueGamesTheorem.Decoder.TableKeys.visibleTau

  10. theorem OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.rightPolicy_on_attainable line 88
  11. theorem OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.leftPolicy_changeHidden line 99
  12. theorem OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.rightPolicy_on_draw line 108
  13. def OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement line 126

    Source documentation

    The literal product of the two observation-local stochastic responses.

    def observedAgreement (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : LeftInput S k s d R → ResponseWitness k → Prop)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) R) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw

  14. theorem OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement_eq_private line 138

    Source documentation

    The private-decoding expression is exactly the actual local-kernel product probability. In particular there is no shared decoder random tape.

    theorem observedAgreement_eq_private (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : LeftInput S k s d R → ResponseWitness k → Prop)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) R) :
    observedAgreement S labeling good draw =
      let w := chosenWitness good (AdviceExperiment.leftObservation (ActualGame.rhs S) draw)
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.chosenWitness, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation

  15. def OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.matrixTable line 191

    Source documentation

    The table at a fixed actual occurrence question and complement map.

    def matrixTable (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (occ : ActualGame.Question S k)
    (T : ActualHomogeneous.E k →ₗ[F2] Vector d)
    (M : Shortcode.Mat s (1 + 2 * k)) : Alphabet s :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount

  16. def OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.fullTable line 200

    Source documentation

    No hidden matrix is an input to this fixed table function.

    def fullTable (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (q : LeftInput S k s d (Vector r)) : Shortcode.Mat s (1 + 2 * k) → Alphabet s :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount

  17. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.matrixTable_fold line 205
  18. def OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice line 227
  19. def OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedDescription line 234

    Source documentation

    The actual normalized description, chosen using only the left observation.

    def normalizedDescription (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q) :
    RowErasureDescriptions.Description s (1 + 2 * k) r :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice

  20. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedDescription_spec line 243
  21. def OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedResponse line 264

    Source documentation

    The response coefficient and columns in the actual homogeneous space.

    def normalizedResponse (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q) :
    ResponseWitness k where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice

  22. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedResponse_dimension line 275
  23. def OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.goodPredicate line 286

    Source documentation

    The generic selector predicate is now the graph of the actual normalized row-advice selector, rather than an unspecified class of candidate witnesses.

    def goodPredicate (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (w : ResponseWitness k) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount

  24. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.chosenWitness_eq_normalizedResponse line 293
  25. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.leftPolicy_eq_candidateLaw line 305

    Source documentation

    The actual left kernel is uniform on the selected normalized affine coset intersected with the first-bit-one answer space.

    theorem leftPolicy_eq_candidateLaw (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q) :
    leftPolicy (goodPredicate S labeling α hα hsmall) q =
      let w := normalizedResponse S labeling α hα hsmall q hgood
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.goodPredicate, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedResponse

  26. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalized_point_row line 317

    Source documentation

    Every point of the selected matrix slice has exactly the observed row value when transported to the actual homogeneous domain.

    theorem normalized_point_row (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q)
    (M : Shortcode.Mat s (1 + 2 * k))
    (hM : M ∈ (RowErasureMatrix.family s (1 + 2 * k) r).points
      (normalizedDescription S labeling α hα hsmall q hgood)) :
    q.rowMap.comp ((mapEquiv k s).symm M) = q.rows := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedDescription

  27. theorem OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalized_target line 335

    Source documentation

    Coordinate transport keeps the actual affine target, including its selected intercept; first-bit normalization never replaces it by a homogeneous target.

    theorem normalized_target (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q)
    (M : Shortcode.Mat s (1 + 2 * k)) :
    (RowErasureMatrix.family s (1 + 2 * k) r).target
        (normalizedDescription S labeling α hα hsmall q hgood) M =
      (mapEquiv k s).symm M (normalizedResponse S labeling α hα hsmall q hgood).coefficient +
        (normalizedDescription S labeling α hα hsmall q hgood).intercept :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedDescription, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.normalizedResponse

  28. instance OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.affineSliceFintype line 382

    Source documentation

    The affine slice is a subtype of a finite linear-map space.

    instance affineSliceFintype {E K L : Type*}
    [AddCommGroup E] [Module F2 E] [AddCommGroup K] [Module F2 K]
    [AddCommGroup L] [Module F2 L] [Fintype (E →ₗ[F2] K)]
    (A : K →ₗ[F2] L) (Q : Submodule F2 E) (Mstar : E →ₗ[F2] K) :
    Fintype (RowErasureSliceQuotient.AffineSlice A Q Mstar) := by
…
  29. theorem OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.selectedEvent_iff_normalized line 393

    Source documentation

    Normalizing the target preserves the actual selected event, point by point.

    theorem selectedEvent_iff_normalized (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q)
    (M : Shortcode.Mat s (1 + 2 * k))
    (hrow : RowErasureMatrix.rowAdvice (LinearMap.toMatrix' q.rowMap) M =
      mapEquiv k r q.rows) :
    (RowErasureMatrix.family s (1 + 2 * k) r).selectedEvent
        (fullTable S labeling q) α (LinearMap.toMatrix' q.rowMap) M ↔
      M ∈ (RowErasureMatrix.family s (1 + 2 * k) r).points
        (normalizedDescription S labeling α hα hsmall q hgood) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount

  30. theorem OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.selectedMatch_iff_normalized line 419

    Source documentation

    The selected target-hit event uses exactly the transported coefficient and its adjusted intercept. This identifies the event used by the mass estimates.

    theorem selectedMatch_iff_normalized (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (q : LeftInput S k s d (Vector r)) (hgood : GoodAdvice S labeling α q)
    (M : Shortcode.Mat s (1 + 2 * k))
    (hrow : RowErasureMatrix.rowAdvice (LinearMap.toMatrix' q.rowMap) M =
      mapEquiv k r q.rows) :
    (RowErasureMatrix.family s (1 + 2 * k) r).selectedMatch
        (fullTable S labeling q) α (LinearMap.toMatrix' q.rowMap) M ↔
      M ∈ (RowErasureMatrix.family s (1 + 2 * k) r).points
          (normalizedDescription S labeling α hα hsmall q hgood) ∧
        fullTable S labeling q M =
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount

  31. theorem OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.rowKernel_reciprocal_le line 459

    Source documentation

    Rank-nullity supplies the small trivial-character probability for every row map, including those with dependent rows.

    theorem rowKernel_reciprocal_le (A : Alphabet s →ₗ[F2] Vector r) :
    1 / (Fintype.card A.ker : ℝ) ≤ 1 / (2 : ℝ) ^ (s - r) := by
…
  32. def OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.transferredAgreement line 469

    Source documentation

    Literal uniform target agreement on the projected affine slice. The slice origin is an analysis witness, independent of the canonical visible row base.

    def transferredAgreement (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (w : ResponseWitness k) (u : Alphabet s)
    (Mstar : RawPartnerTarget.RawPoint draw.singletons →ₗ[F2] Alphabet s) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw

  33. theorem OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.observedAgreement_lower line 484

    Source documentation

    The actual independently sampled local policies obey the decoding lower bound at every datum with a transferred good slice for its selected witness.

    theorem observedAgreement_lower (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (hgood : GoodAdvice S labeling α (AdviceExperiment.leftObservation (ActualGame.rhs S) draw))
    (Mstar : RawPartnerTarget.RawPoint draw.singletons →ₗ[F2] Alphabet s)
    (hstar : draw.rowMap.comp Mstar = draw.rowMap.comp draw.hiddenMatrix)
    (hagreement : α / 4 ≤ transferredAgreement S labeling draw
      (normalizedResponse S labeling α hα hsmall
        (AdviceExperiment.leftObservation (ActualGame.rhs S) draw) hgood)
      (normalizedDescription S labeling α hα hsmall
        (AdviceExperiment.leftObservation (ActualGame.rhs S) draw) hgood).intercept Mstar) :
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation, OAI.UniqueGamesTheorem.Decoder.SelectedDecoding.transferredAgreement

  34. theorem OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.column_agreement_iff line 550

    Source documentation

    Two successive images of a column subspace express the same pointwise agreement as composition with the coordinate change and projection.

    theorem column_agreement_iff (Q : Submodule F2 (Vector (1 + 2 * k)))
    (π : ActualHomogeneous.E k →ₗ[F2] V) (M Mstar : V →ₗ[F2] Alphabet s) :
    (∀ x ∈ Q, M (π ((domainCoordinates k).symm x)) =
      Mstar (π ((domainCoordinates k).symm x))) ↔
      ∀ v ∈ (Q.map (domainCoordinates k).symm.toLinearMap).map π, M v = Mstar v := by
…
  35. theorem OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.contains_padded_iff line 567

    Source documentation

    A simultaneous matrix slice pulls back to the projected column equations once the actual row equation is fixed.

    theorem contains_padded_iff
    (D : RowErasureDescriptions.Description s (1 + 2 * k) r)
    (A : Alphabet s →ₗ[F2] Vector r)
    (hDrow : (RowErasureMatrix.family s (1 + 2 * k) r).rowMap D = LinearMap.toMatrix' A)
    (π : ActualHomogeneous.E k →ₗ[F2] V) (Mstar : V →ₗ[F2] Alphabet s)
    (hstar : mapEquiv k s (Mstar.comp π) ∈ D.toSlice.points)
    (M : V →ₗ[F2] Alphabet s) (hrow : A.comp M = A.comp Mstar) :
    mapEquiv k s (M.comp π) ∈ D.toSlice.points ↔
      ∀ v ∈ (D.toSlice.columnSpan.map (domainCoordinates k).symm.toLinearMap).map π,
        M v = Mstar v := by
…
  36. def OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.paddedSliceEquiv line 605

    Source documentation

    The subtype equivalence leaves the actual matrix untouched.

    def paddedSliceEquiv
    (D : RowErasureDescriptions.Description s (1 + 2 * k) r)
    (A : Alphabet s →ₗ[F2] Vector r)
    (hDrow : (RowErasureMatrix.family s (1 + 2 * k) r).rowMap D = LinearMap.toMatrix' A)
    (π : ActualHomogeneous.E k →ₗ[F2] V) (Mstar : V →ₗ[F2] Alphabet s)
    (hstar : mapEquiv k s (Mstar.comp π) ∈ D.toSlice.points) :
    {M : V →ₗ[F2] Alphabet s // A.comp M = A.comp Mstar ∧
      mapEquiv k s (M.comp π) ∈ D.toSlice.points} ≃
      RowErasureSliceQuotient.AffineSlice A
        ((D.toSlice.columnSpan.map (domainCoordinates k).symm.toLinearMap).map π) Mstar where
…
  37. theorem OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.paddedSlice_expect line 624

    Source documentation

    Uniform expectations agree exactly, because the subtype equivalence preserves the underlying matrix.

    theorem paddedSlice_expect
    (D : RowErasureDescriptions.Description s (1 + 2 * k) r)
    (A : Alphabet s →ₗ[F2] Vector r)
    (hDrow : (RowErasureMatrix.family s (1 + 2 * k) r).rowMap D = LinearMap.toMatrix' A)
    (π : ActualHomogeneous.E k →ₗ[F2] V) (Mstar : V →ₗ[F2] Alphabet s)
    (hstar : mapEquiv k s (Mstar.comp π) ∈ D.toSlice.points)
    [Fintype {M : V →ₗ[F2] Alphabet s // A.comp M = A.comp Mstar ∧
      mapEquiv k s (M.comp π) ∈ D.toSlice.points}]
    [Fintype (RowErasureSliceQuotient.AffineSlice A
      ((D.toSlice.columnSpan.map (domainCoordinates k).symm.toLinearMap).map π) Mstar)]
    (f : (V →ₗ[F2] Alphabet s) → ℝ) :
    (𝔼 M : {M : V →ₗ[F2] Alphabet s // A.comp M = A.comp Mstar ∧
…
  38. theorem OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.fullTable_padded line 646

    Source documentation

    Exact key sharing identifies the selected full table with the projected answer table at every possible hidden matrix in this visible fiber.

    theorem fullTable_padded (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (M : RawPartnerTarget.RawPoint draw.singletons →ₗ[F2] Alphabet s) :
    fullTable S labeling (AdviceExperiment.leftObservation (ActualGame.rhs S) draw)
        (mapEquiv k s (M.comp (AdviceExperiment.projection (ActualGame.rhs S) draw))) =
      TableKeysRestoration.projectedAnswer S k s d labeling draw.singletons
        (RawPrivateTable.supported draw.singletons (ActualGame.names S)
          draw.occurrences draw.positions) (M.prod draw.complement) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.projection, OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer

  39. theorem OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.normalized_contains_iff line 661

    Source documentation

    The concrete normalized witness induces exactly the projected column span used by the private Fourier conditional bound.

    theorem normalized_contains_iff (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (hgood : GoodAdvice S labeling α (AdviceExperiment.leftObservation (ActualGame.rhs S) draw))
    (Mstar : RawPartnerTarget.RawPoint draw.singletons →ₗ[F2] Alphabet s)
    (hstar : mapEquiv k s (Mstar.comp (AdviceExperiment.projection (ActualGame.rhs S) draw)) ∈
      (normalizedDescription S labeling α hα hsmall
        (AdviceExperiment.leftObservation (ActualGame.rhs S) draw) hgood).toSlice.points)
    (M : RawPartnerTarget.RawPoint draw.singletons →ₗ[F2] Alphabet s)
    (hrow : draw.rowMap.comp M = draw.rowMap.comp Mstar) :
    mapEquiv k s (M.comp (AdviceExperiment.projection (ActualGame.rhs S) draw)) ∈
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.projection

  40. theorem OAI.UniqueGamesTheorem.Decoder.ProjectedColumnSlice.normalized_target_padded line 683

    Source documentation

    The actual selected target retains its intercept after projection.

    theorem normalized_target_padded (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (hgood : GoodAdvice S labeling α (AdviceExperiment.leftObservation (ActualGame.rhs S) draw))
    (M : RawPartnerTarget.RawPoint draw.singletons →ₗ[F2] Alphabet s) :
    (RowErasureMatrix.family s (1 + 2 * k) r).target
        (normalizedDescription S labeling α hα hsmall
          (AdviceExperiment.leftObservation (ActualGame.rhs S) draw) hgood)
        (mapEquiv k s (M.comp (AdviceExperiment.projection (ActualGame.rhs S) draw))) =
      M (AdviceExperiment.projection (ActualGame.rhs S) draw
          (normalizedResponse S labeling α hα hsmall
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.projection