OAI/Computability/UniqueGames/Inverse/RowErasureMatrixLemmas.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Visible selection of a row-erasure witness. The selected description depends only on the fixed table function, the row map, and the observed row value. The full sampled matrix enters only the later event testing its membership in the already selected slice. Classical choice fixes one witness once and for all; proof irrelevance makes the choice independent of the goodness proof.

  1. def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.rowAdvice line 18
  2. def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family line 21
  3. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family_agreement line 35
  4. abbrev OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.Samples line 47
  5. def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.left line 49
  6. def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.right line 51
  7. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.expect_prod line 54
  8. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.left_uniform line 63
  9. def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.stepEquiv line 71

    Source documentation

    Translation of the sampled matrix is a permutation while the two sampled factors remain fixed; this also covers either factor being zero.

    def stepEquiv (ell m : ℕ) : Samples ell m ≃ Samples ell m where
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.Samples

  10. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.right_uniform line 83
  11. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.acceptance_eq line 90
  12. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.described_inverse line 109

    Source documentation

    Zero-padding turns the actual bounded-slice inverse conclusion into the description-based inverse conclusion used by the erasure proof.

    theorem described_inverse {ell m r : ℕ} (α η : ℝ)
    (inverse : ∀ f : Mat ell m → Vector ell,
      η ≤ Shortcode.equalityAcceptance f → HasAffineSlice f α r) :
    ∀ f : Mat ell m → Vector ell,
      η ≤ RowErasure.equalityAcceptance (left (ell := ell) (m := m)) right f →
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.RowErasure.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.left, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.right

  13. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.advice_mass_ge_of_inverse_and_erasure line 129

    Source documentation

    Concrete fixed-context advice lower bound. All full matrix and row-map samples are uniform. The still-required mathematical premises are visible: the actual shortcode inverse and a simultaneous small-replacement witness.

    theorem advice_mass_ge_of_inverse_and_erasure {ell m r : ℕ}
    (f : Mat ell m → Vector ell) (η α : ℝ) (hη : 0 < η) (hα : 0 < α)
    (haccept : 4 * η ≤ Shortcode.equalityAcceptance f)
    (inverse : ∀ g : Mat ell m → Vector ell,
      η ≤ Shortcode.equalityAcceptance g → HasAffineSlice g α r)
    (erasure : ∃ replacement : Mat ell m → Vector ell,
      ∀ d : Description ell m r, ((family ell m r).points d).Nonempty →
        (family ell m r).randomizedAgreement
          ((family ell m r).erasedUnion f α) replacement d < α / 4) :
    η / (2 ^ (ell * r) : ℝ) ≤ adviceMass ((family ell m r).goodAt f α) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  14. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.exists_replacement_of_budget line 164

    Source documentation

    One replacement table simultaneously defeats every padded slice/target. The budget depends only on dimensions and α, not on the labeling or erased set.

    theorem exists_replacement_of_budget {ell m r : ℕ}
    (B : Mat ell m → Prop) (α : ℝ) (hα : 0 < α) (hαone : α ≤ 1)
    (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8)
    (hbudget : (2 : ℝ) ^ ((2 * r + 1) * (ell + m)) *
      Real.exp (-(α ^ 2 * (2 : ℝ) ^ ((ell - r) * (m - r))) / 32) < 1) :
    ∃ replacement : Mat ell m → Vector ell,
      ∀ d : Description ell m r, ((family ell m r).points d).Nonempty →
        (family ell m r).randomizedAgreement B replacement d < α / 4 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  15. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.advice_mass_ge_of_inverse_and_budget line 193

    Source documentation

    The random-erasure obligation is discharged here by proved finite product concentration and concrete slice counts. The inverse hypothesis is still the genuine new-route mathematical input.

    theorem advice_mass_ge_of_inverse_and_budget {ell m r : ℕ}
    (f : Mat ell m → Vector ell) (η α : ℝ) (hη : 0 < η)
    (hα : 0 < α) (hαone : α ≤ 1)
    (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8)
    (haccept : 4 * η ≤ Shortcode.equalityAcceptance f)
    (inverse : ∀ g : Mat ell m → Vector ell,
      η ≤ Shortcode.equalityAcceptance g → HasAffineSlice g α r)
    (hbudget : (2 : ℝ) ^ ((2 * r + 1) * (ell + m)) *
      Real.exp (-(α ^ 2 * (2 : ℝ) ^ ((ell - r) * (m - r))) / 32) < 1) :
    η / (2 ^ (ell * r) : ℝ) ≤ adviceMass ((family ell m r).goodAt f α) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  16. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.exists_erasure_threshold line 225

    Source documentation

    A single dimension threshold supplies replacements for every erased set. There is no inverse-theorem premise in this concentration/counting statement.

    theorem exists_erasure_threshold (α : ℝ) (hα : 0 < α) (hαone : α ≤ 1)
    (ell r : ℕ) (hr : r < ell) (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m →
      ∀ B : Mat ell m → Prop,
        ∃ replacement : Mat ell m → Vector ell,
          ∀ d : Description ell m r, ((family ell m r).points d).Nonempty →
            (family ell m r).randomizedAgreement B replacement d < α / 4 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  17. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.exists_fixed_context_advice_threshold line 240

    Source documentation

    For sufficiently many columns, every accepted function has a positive measure of good row advice, assuming the genuine bounded-slice inverse.

    theorem exists_fixed_context_advice_threshold (η α : ℝ)
    (hη : 0 < η) (hα : 0 < α) (hαone : α ≤ 1)
    (ell r : ℕ) (hr : r < ell) (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m →
      (∀ g : Mat ell m → Vector ell,
        η ≤ Shortcode.equalityAcceptance g → HasAffineSlice g α r) →
      ∀ f : Mat ell m → Vector ell,
        4 * η ≤ Shortcode.equalityAcceptance f →
          η / (2 ^ (ell * r) : ℝ) ≤ adviceMass ((family ell m r).goodAt f α) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  18. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.exists_contextual_advice_threshold line 255
  19. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.chosenDescription line 302
  20. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.chosenDescription_spec line 307
  21. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.chosenDescription_congr line 316
  22. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedDescription line 327

    Source documentation

    A total visible selector. Bad advice has no selected witness.

    def SliceFamily.selectedDescription (F : SliceFamily X Y A S D)
    (f : X → Y) (α : ℝ) (a : A) (s : S) : Option D := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily

  23. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedDescription_of_good line 333
  24. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.good_of_selectedDescription line 339
  25. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedDescription_spec line 348
  26. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedDescription_congr line 359
  27. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedEvent line 369

    Source documentation

    Good visible advice and the selected column restrictions on the hidden matrix. The selector receives only its observed row value.

    def SliceFamily.selectedEvent (F : SliceFamily X Y A S D)
    (f : X → Y) (α : ℝ) (a : A) (x : X) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily

  28. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedMatch line 373
  29. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedEvent_iff_of_advice line 378
  30. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedMatch_iff_of_advice line 391
  31. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedEvent_good line 406
  32. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedMatch_event line 412
  33. def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.withTarget line 436

    Source documentation

    Replace the affine target while retaining all row and column data.

    def Description.withTarget {ell m r : ℕ} (d : Description ell m r)
    (z : Vector m) (u : Vector ell) : Description ell m r :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description

  34. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.withTarget_toSlice line 440
  35. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.withTarget_coefficient line 444
  36. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.withTarget_intercept line 448
  37. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.exists_normalizedChosenDescription line 467

    Source documentation

    Normalization of the already chosen description. The sampled matrix is absent from the selector's inputs; pointwise target equality holds afterward for every matrix in the selected slice.

    theorem exists_normalizedChosenDescription
    (f : Mat ell m → Vector ell) (α : ℝ) (A : RowMap ell r) (S : Mat r m)
    (hgood : (family ell m r).GoodAdvice f α A S)
    (e : Vector m →ₗ[F2] F2)
    (hfold : ∀ (h : Vector ell) M,
      f (M + rankOne h (functionalRow e)) = f M + h)
    (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (ell - r) < α / 8) :
    let d₀ := (family ell m r).chosenDescription f α A S hgood
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  38. def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.normalizedChosenDescription line 508

    Source documentation

    A fixed normalized witness determined by the visible table and row advice. All remaining inputs are the fixed normalization functional and proofs.

    def normalizedChosenDescription
    (f : Mat ell m → Vector ell) (α : ℝ) (A : RowMap ell r) (S : Mat r m)
    (hgood : (family ell m r).GoodAdvice f α A S)
    (e : Vector m →ₗ[F2] F2)
    (hfold : ∀ (h : Vector ell) M,
      f (M + rankOne h (functionalRow e)) = f M + h)
    (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (ell - r) < α / 8) :
    Description ell m r :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family

  39. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.normalizedChosenDescription_spec line 518
  40. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.fiber line 560
  41. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.event line 563
  42. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.matchEvent line 567
  43. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.expect_le_expect_of_fiber_sum_le line 573

    Source documentation

    Arbitrary real summands can be compared fiber by fiber. No uniformity of the induced observation distribution is asserted or required.

    theorem expect_le_expect_of_fiber_sum_le (observe : X → S) (f g : X → ℝ)
    (hle : ∀ s, (∑ x ∈ fiber observe s, f x) ≤ ∑ x ∈ fiber observe s, g x) :
    Finset.univ.expect f ≤ Finset.univ.expect g := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.fiber

  44. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.sum_event_mul_fiber line 585

    Source documentation

    On good visible data, the selected event sums exactly over the selected points, including for arbitrary real weights on the hidden sample.

    theorem sum_event_mul_fiber (observe : X → S) (good : S → Prop)
    (chosen : S → Finset X)
    (support : ∀ s x, x ∈ chosen s → observe x = s)
    (s : S) (hgood : good s) (w : X → ℝ) :
    (∑ x ∈ fiber observe s, indicator (event observe good chosen x) * w x) =
      ∑ x ∈ chosen s, w x := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.fiber, OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator, OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.event

  45. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.sum_event_fiber line 610
  46. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.sum_match_fiber line 619
  47. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.mass_event_ge line 639

    Source documentation

    A lower fraction inside every good fiber gives the same lower fraction of the actual good-advice mass. Empty fibers and empty sample spaces are valid.

    theorem mass_event_ge (observe : X → S) (good : S → Prop)
    (chosen : S → Finset X)
    (support : ∀ s x, x ∈ chosen s → observe x = s)
    (c : ℝ)
    (hsize : ∀ s, good s →
      c * ((fiber observe s).card : ℝ) ≤ ((chosen s).card : ℝ)) :
    c * uniformMass (fun x => good (observe x)) ≤
      uniformMass (event observe good chosen) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.fiber, OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass, OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.event

  48. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.mass_match_ge line 678

    Source documentation

    A matching fraction in every selected good fiber survives averaging over the hidden sample space, without any equiprobability assumption on fibers.

    theorem mass_match_ge (observe : X → S) (good : S → Prop)
    (chosen : S → Finset X)
    (support : ∀ s x, x ∈ chosen s → observe x = s)
    (hit : S → X → Prop) (β : ℝ)
    (hmatch : ∀ s, good s →
      β * ((chosen s).card : ℝ) ≤ ∑ x ∈ chosen s, indicator (hit s x)) :
    β * uniformMass (event observe good chosen) ≤
      uniformMass (matchEvent observe good chosen hit) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator, OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass, OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.event, OAI.UniqueGamesTheorem.Inverse.RowErasure.SelectionPartition.matchEvent

  49. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.difference_row_zero line 727
  50. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.difference_range_le line 740
  51. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.difference_vanishes_columns line 747
  52. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionEmbedding_surjective line 760

    Source documentation

    Every actual slice point differs from the base by a unique quotient map.

    theorem directionEmbedding_surjective (S : Slice ell m)
    (M₀ : Mat ell m) (h₀ : S.Contains M₀) :
    Function.Surjective (S.directionEmbedding M₀ h₀) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat

  53. def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionEquiv line 782

    Source documentation

    The concrete simultaneous slice is exactly an affine copy of Hom(domain / columnSpan, commonRowKernel).

    def directionEquiv (S : Slice ell m) (M₀ : Mat ell m) (h₀ : S.Contains M₀) :
    S.Directions ≃ S.points :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat

  54. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionEquiv_val line 787
  55. instance OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionsFintype line 791
  56. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.card_points_eq_directions line 799
  57. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.points_expect_eq_directions line 805

    Source documentation

    Uniform quotient parameters give precisely the uniform measure on the actual finite slice, including all its inhomogeneous row/column equations.

    theorem points_expect_eq_directions (S : Slice ell m) (M₀ : Mat ell m)
    (h₀ : S.Contains M₀) (f : Mat ell m → ℝ) :
    S.points.expect f = 𝔼 N : S.Directions, f (M₀ + S.directionMatrix N) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat

  58. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionMatrix_evaluate line 813
  59. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.direction_affine_target line 821

    Source documentation

    The decoder's affine offset is the original intercept plus the base matrix evaluated at the target; it is not silently replaced by zero.

    theorem direction_affine_target (S : Slice ell m) (M₀ : Mat ell m)
    (N : S.Directions) (z : Vector m) (u : Vector ell) :
    evaluate (M₀ + S.directionMatrix N) z + u =
      (N (S.columnSpan.mkQ z) : Vector ell) + (evaluate M₀ z + u) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.evaluate

  60. theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.affineAgreement_eq_directions line 832