OAI/Computability/MaxCut/Encoding/SelectedPolicies.lean

GitHub source file

48 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. def OAI.MaxCutGames.Decoder.SelectedPolicies.matrixTable line 31

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount

  2. def OAI.MaxCutGames.Decoder.SelectedPolicies.fullTable line 40

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount

  3. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.matrixTable_fold line 45
  4. def OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice line 67
  5. def OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedDescription line 74

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice

  6. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedDescription_spec line 83
  7. def OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedResponse line 104

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice

  8. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedResponse_dimension line 115
  9. def OAI.MaxCutGames.Decoder.SelectedPolicies.goodPredicate line 126

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount

  10. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.chosenWitness_eq_normalizedResponse line 133
  11. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.leftPolicy_eq_candidateLaw line 145

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice, OAI.MaxCutGames.Decoder.SelectedPolicies.goodPredicate, OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedResponse

  12. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.normalized_point_row line 157

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice, OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedDescription

  13. theorem OAI.MaxCutGames.Decoder.SelectedPolicies.normalized_target line 175

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice, OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedDescription, OAI.MaxCutGames.Decoder.SelectedPolicies.normalizedResponse

  14. abbrev OAI.MaxCutGames.Decoder.ActualSeedEvents.Seed line 206
  15. abbrev OAI.MaxCutGames.Decoder.ActualSeedEvents.Datum line 209
  16. def OAI.MaxCutGames.Decoder.ActualSeedEvents.law line 212
  17. def OAI.MaxCutGames.Decoder.ActualSeedEvents.draw line 218
  18. def OAI.MaxCutGames.Decoder.ActualSeedEvents.pad line 221
  19. def OAI.MaxCutGames.Decoder.ActualSeedEvents.slice line 225
  20. def OAI.MaxCutGames.Decoder.ActualSeedEvents.targetHit line 230
  21. theorem OAI.MaxCutGames.Decoder.ActualSeedEvents.pad_eq line 236

    Source documentation

    The padded comparison contains both complete affine component maps.

    theorem pad_eq (S : Source) (k s d r : ℕ) (x : Seed S k s d r) :
    pad S k s d r x =
      (((draw x).occurrences, AdviceExperiment.paddedComplement (ActualGame.rhs S) (draw x)),
        (LinearMap.toMatrix' (draw x).rowMap,
          MatrixCoordinates.mapEquiv k s (AdviceExperiment.paddedMatrix (ActualGame.rhs S) (draw x)))) :=
…

    Mentions: OAI.MaxCutGames.Decoder.ActualSeedEvents.Seed, OAI.MaxCutGames.Decoder.ActualSeedEvents.pad, OAI.MaxCutGames.Decoder.ActualSeedEvents.draw, OAI.MaxCutGames.Decoder.AdviceExperiment.paddedComplement, OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv, OAI.MaxCutGames.Decoder.AdviceExperiment.paddedMatrix

  22. theorem OAI.MaxCutGames.Decoder.ActualSeedEvents.slice_eq_selectedEvent line 243
  23. theorem OAI.MaxCutGames.Decoder.ActualSeedEvents.targetHit_eq_selectedMatch line 254
  24. theorem OAI.MaxCutGames.Decoder.ActualSeedEvents.slice_good line 267

    Source documentation

    Positive selected-slice mass automatically supplies actual good left advice; goodness is not an independent projected experiment assumption.

    theorem slice_good (S : Source) (k s d r : ℕ)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) (α : ℝ)
    (x : Seed S k s d r) (hx : slice S k s d r labeling α x = true) :
    SelectedPolicies.GoodAdvice S labeling α
      (AdviceExperiment.leftObservation (ActualGame.rhs S) (draw x)) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.ActualSeedEvents.Seed, OAI.MaxCutGames.Decoder.ActualSeedEvents.slice, OAI.MaxCutGames.Decoder.SelectedPolicies.GoodAdvice, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation, OAI.MaxCutGames.Decoder.ActualSeedEvents.draw

  25. theorem OAI.MaxCutGames.Decoder.ActualSeedVariation.uniform_pushforward_equiv line 307
  26. theorem OAI.MaxCutGames.Decoder.ActualSeedVariation.totalVariation_pushforward_equiv line 316
  27. theorem OAI.MaxCutGames.Decoder.ActualSeedVariation.ideal_full_uniform line 325

    Source documentation

    Three independent uniform samples are uniform on their full product.

    theorem ideal_full_uniform (S : Source) (k s d r : ℕ) :
    AdviceLaw.withKernel
      ((FiniteDistribution.uniform (ActualGame.Question S k)).product
        (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector r)))
      (fun _ => FiniteDistribution.uniform (ActualGame.Map k s d)) =
        FiniteDistribution.uniform (ActualEvents.FullTableSample S k s d r) := by
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceLaw.withKernel, OAI.MaxCutGames.Decoder.ActualEvents.FullTableSample

  28. theorem OAI.MaxCutGames.Decoder.ActualSeedVariation.ideal_pad_coordinates line 337
  29. theorem OAI.MaxCutGames.Decoder.ActualSeedVariation.actual_totalVariation_le_slope line 346
  30. instance OAI.MaxCutGames.Decoder.SelectedDecoding.affineSliceFintype line 397

    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
…
  31. theorem OAI.MaxCutGames.Decoder.SelectedDecoding.selectedEvent_iff_normalized line 408

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount

  32. theorem OAI.MaxCutGames.Decoder.SelectedDecoding.selectedMatch_iff_normalized line 434

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount

  33. theorem OAI.MaxCutGames.Decoder.SelectedDecoding.rowKernel_reciprocal_le line 474

    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
…
  34. def OAI.MaxCutGames.Decoder.SelectedDecoding.transferredAgreement line 484

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw

  35. theorem OAI.MaxCutGames.Decoder.SelectedDecoding.observedAgreement_lower line 499

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation, OAI.MaxCutGames.Decoder.SelectedDecoding.transferredAgreement

  36. theorem OAI.MaxCutGames.Decoder.ProjectedColumnSlice.column_agreement_iff line 560

    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
…
  37. theorem OAI.MaxCutGames.Decoder.ProjectedColumnSlice.contains_padded_iff line 577

    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
…
  38. def OAI.MaxCutGames.Decoder.ProjectedColumnSlice.paddedSliceEquiv line 615

    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
…
  39. theorem OAI.MaxCutGames.Decoder.ProjectedColumnSlice.paddedSlice_expect line 634

    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 ∧
…
  40. theorem OAI.MaxCutGames.Decoder.ProjectedColumnSlice.fullTable_padded line 656

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation, OAI.MaxCutGames.Decoder.AdviceExperiment.projection, OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer

  41. theorem OAI.MaxCutGames.Decoder.ProjectedColumnSlice.normalized_contains_iff line 670

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation, OAI.MaxCutGames.Decoder.AdviceExperiment.projection

  42. theorem OAI.MaxCutGames.Decoder.ProjectedColumnSlice.normalized_target_padded line 692

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation, OAI.MaxCutGames.Decoder.AdviceExperiment.projection

  43. theorem OAI.MaxCutGames.Decoder.UniformConditioning.sum_over_event line 726
  44. theorem OAI.MaxCutGames.Decoder.UniformConditioning.probability_as_subtype_sum line 731
  45. theorem OAI.MaxCutGames.Decoder.UniformConditioning.probability_and_as_subtype_sum line 735
  46. theorem OAI.MaxCutGames.Decoder.UniformConditioning.probability_of_constant_weight line 747
  47. theorem OAI.MaxCutGames.Decoder.UniformConditioning.condition_probability_uniform line 761

    Source documentation

    Every remaining point receives equal conditional weight. Positivity of the conditioning event justifies cancellation; no unconditional uniform law on the original ambient experiment is required.

    theorem condition_probability_uniform (μ : FiniteDistribution Ω)
    (given event : Ω → Bool) (positive : 0 < μ.probability given)
    (c : ℝ) (hconstant : ∀ x, given x = true → μ.weight x = c) :
    (μ.condition given positive).probability event =
      𝔼 x : {x : Ω // given x = true}, if event x.val then (1 : ℝ) else 0 := by
…
  48. theorem OAI.MaxCutGames.Decoder.UniformConditioning.condition_probability_equiv line 789

    Source documentation

    A proved bijection with the actual affine matrix slice identifies the conditional target probability with that slice's complete uniform average.

    theorem condition_probability_equiv {Y : Type*} [Fintype Y]
    (μ : FiniteDistribution Ω) (given event : Ω → Bool)
    (positive : 0 < μ.probability given) (c : ℝ)
    (hconstant : ∀ x, given x = true → μ.weight x = c)
    (e : {x : Ω // given x = true} ≃ Y) (target : Y → Bool)
    (hevent : ∀ x, event x.val = target (e x)) :
    (μ.condition given positive).probability event =
      𝔼 y : Y, if target y then (1 : ℝ) else 0 := by
…