OAI/Computability/MaxCut/Games/RowErasure.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

InversePrinciple concerns an arbitrary table function, full uniform factor sampling, and an affine intercept.

  1. def OAI.MaxCutGames.Inverse.RowErasure.indicator line 14
  2. theorem OAI.MaxCutGames.Inverse.RowErasure.indicator_true line 18
  3. theorem OAI.MaxCutGames.Inverse.RowErasure.indicator_false line 19
  4. theorem OAI.MaxCutGames.Inverse.RowErasure.indicator_nonneg line 21
  5. theorem OAI.MaxCutGames.Inverse.RowErasure.indicator_le_one line 26
  6. def OAI.MaxCutGames.Inverse.RowErasure.uniformMass line 31
  7. theorem OAI.MaxCutGames.Inverse.RowErasure.uniformMass_nonneg line 34
  8. theorem OAI.MaxCutGames.Inverse.RowErasure.uniformMass_le_one line 38
  9. def OAI.MaxCutGames.Inverse.RowErasure.replaceOn line 43

    Source documentation

    One independent replacement value per matrix entry, not per row fiber.

    def replaceOn {X Y : Type*} (B : X → Prop) (f replacement : X → Y) : X → Y := by
…
  10. theorem OAI.MaxCutGames.Inverse.RowErasure.replaceOn_of_not_mem line 47
  11. theorem OAI.MaxCutGames.Inverse.RowErasure.replaceOn_of_mem line 52
  12. def OAI.MaxCutGames.Inverse.RowErasure.equalityAcceptance line 57
  13. theorem OAI.MaxCutGames.Inverse.RowErasure.acceptance_le_modified_add_two_mass line 64

    Source documentation

    Deterministic acceptance loss under editing a set of entries. Both endpoint marginals must equal the matrix-uniform law; no independence of endpoints is required. This applies to every choice of replacement values.

    theorem acceptance_le_modified_add_two_mass
    {X Y E : Type*} [Fintype X] [Fintype E]
    (left right : E → X) (B : X → Prop) (f g : X → Y)
    (unchanged : ∀ x, ¬ B x → f x = g x)
    (left_uniform : uniformMass (fun e => B (left e)) = uniformMass B)
    (right_uniform : uniformMass (fun e => B (right e)) = uniformMass B) :
    equalityAcceptance left right f ≤
      equalityAcceptance left right g + 2 * uniformMass B := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.uniformMass, OAI.MaxCutGames.Inverse.RowErasure.equalityAcceptance

  14. theorem OAI.MaxCutGames.Inverse.RowErasure.acceptance_ge_original_sub_two_mass line 99
  15. def OAI.MaxCutGames.Inverse.RowErasure.goodUnion line 114

    Source documentation

    A matrix belongs to the erased union exactly when at least one row map provides good advice there.

    def goodUnion {A X : Type*} (good : A → X → Prop) (x : X) : Prop :=
…
  16. def OAI.MaxCutGames.Inverse.RowErasure.adviceMass line 118

    Source documentation

    Sample a uniform matrix, then an independent uniform row map.

    def adviceMass {A X : Type*} [Fintype A] [Fintype X]
    (good : A → X → Prop) : ℝ :=
…
  17. theorem OAI.MaxCutGames.Inverse.RowErasure.adviceMass_nonneg line 122
  18. theorem OAI.MaxCutGames.Inverse.RowErasure.union_mass_le_card_mul_adviceMass line 128

    Source documentation

    Each matrix in the union has at least one successful row-map atom. No disjointness between good fibers is needed.

    theorem union_mass_le_card_mul_adviceMass
    {A X : Type*} [Fintype A] [Fintype X] (good : A → X → Prop) :
    uniformMass (goodUnion good) ≤ (Fintype.card A : ℝ) * adviceMass good := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.uniformMass, OAI.MaxCutGames.Inverse.RowErasure.goodUnion, OAI.MaxCutGames.Inverse.RowErasure.adviceMass

  19. theorem OAI.MaxCutGames.Inverse.RowErasure.adviceMass_ge_union_div_card line 147
  20. theorem OAI.MaxCutGames.Inverse.RowErasure.adviceMass_ge_of_union_mass line 155
  21. structure OAI.MaxCutGames.Inverse.RowErasure.SliceFamily line 168

    Source documentation

    Each description includes its row map, row value, column equations and affine target. points_row is the necessary relationship to actual row advice.

    structure SliceFamily (X Y A S D : Type*) where
…
  22. def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.agreement line 176
  23. def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.GoodAdvice line 179
  24. def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.goodAt line 184
  25. def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.erasedUnion line 188
  26. def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.randomizedAgreement line 194

    Source documentation

    Only randomized entries count; an unchanged entry contributes zero, even when its old label already matches the target.

    def SliceFamily.randomizedAgreement (F : SliceFamily X Y A S D)
    (B : X → Prop) (replacement : X → Y) (d : D) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily

  27. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.mem_erasedUnion_of_good_row line 198
  28. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.original_agreement_lt_of_not_good line 207
  29. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.modified_agreement_le_original_add_randomized line 215
  30. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.modified_agreement_eq_randomized_of_good line 237
  31. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.modified_agreement_lt line 253

    Source documentation

    If the random replacement bound holds, every permitted nonempty slice has modified agreement strictly below α. The proof splits on goodness of the whole row fiber, not on goodness of the individual column slice.

    theorem SliceFamily.modified_agreement_lt
    (F : SliceFamily X Y A S D) (f replacement : X → Y)
    (α : ℝ) (hα : 0 < α)
    (randomized_small : ∀ d, (F.points d).Nonempty →
      F.randomizedAgreement (F.erasedUnion f α) replacement d < α / 4)
    (d : D) (hne : (F.points d).Nonempty) :
    F.agreement (replaceOn (F.erasedUnion f α) f replacement) d < α := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily, OAI.MaxCutGames.Inverse.RowErasure.replaceOn

  32. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.union_mass_ge_of_inverse_and_erasure line 274

    Source documentation

    Conditional erasure contradiction. The two deep inputs remain explicit: the inverse theorem for arbitrary (possibly unfolded) functions, and existence of a replacement table uniformly small on every slice/target description.

    theorem SliceFamily.union_mass_ge_of_inverse_and_erasure
    {E : Type*} [Fintype X] [Fintype E]
    (F : SliceFamily X Y A S D) (left right : E → X)
    (f : X → Y) (η α : ℝ) (hη : 0 < η) (hα : 0 < α)
    (acceptance_large : 4 * η ≤ equalityAcceptance left right f)
    (left_uniform : ∀ B : X → Prop,
      uniformMass (fun e => B (left e)) = uniformMass B)
    (right_uniform : ∀ B : X → Prop,
      uniformMass (fun e => B (right e)) = uniformMass B)
    (inverse : ∀ g : X → Y, η ≤ equalityAcceptance left right g →
      ∃ d, (F.points d).Nonempty ∧ α ≤ F.agreement g d)
    (erasure : ∃ replacement : X → Y, ∀ d, (F.points d).Nonempty →
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily, OAI.MaxCutGames.Inverse.RowErasure.equalityAcceptance, OAI.MaxCutGames.Inverse.RowErasure.uniformMass

  33. theorem OAI.MaxCutGames.Inverse.RowErasure.uniformMass_exists_le_sum line 304
  34. theorem OAI.MaxCutGames.Inverse.RowErasure.exists_avoiding_of_sum_bad_lt_one line 321
  35. theorem OAI.MaxCutGames.Inverse.RowErasure.exists_avoiding_of_card_mul_bound_lt_one line 337
  36. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.exists_erasure_of_probability_bound line 351

    Source documentation

    The union-bound step for actual replacement tables. Nonempty slice descriptions with randomized agreement at least α/4 are the bad events.

    theorem SliceFamily.exists_erasure_of_probability_bound
    {X Y A S D : Type*} [Fintype X] [Fintype Y] [Nonempty Y] [Fintype D]
    (F : SliceFamily X Y A S D) (B : X → Prop) (α ρ : ℝ)
    (hprob : ∀ d, uniformMass (fun replacement : X → Y =>
      (F.points d).Nonempty ∧ α / 4 ≤ F.randomizedAgreement B replacement d) ≤ ρ)
    (hsmall : (Fintype.card D : ℝ) * ρ < 1) :
    ∃ replacement : X → Y, ∀ d, (F.points d).Nonempty →
      F.randomizedAgreement B replacement d < α / 4 := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily, OAI.MaxCutGames.Inverse.RowErasure.uniformMass

  37. theorem OAI.MaxCutGames.Inverse.RowErasure.advice_average_ge line 368

    Source documentation

    Average the fixed-context advice bound over the spectral good contexts. Both samples remain explicit: the context, then the row map and matrix.

    theorem advice_average_ge
    {Q A X : Type*} [Fintype Q] [Fintype A] [Nonempty A] [Fintype X]
    (goodContext : Q → Prop) (good : Q → A → X → Prop)
    (β η : ℝ) (hη : 0 ≤ η)
    (hcontext : β ≤ uniformMass goodContext)
    (hlocal : ∀ q, goodContext q → η ≤ uniformMass (goodUnion (good q))) :
    β * (η / (Fintype.card A : ℝ)) ≤
      Finset.univ.expect (fun q => adviceMass (good q)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.uniformMass, OAI.MaxCutGames.Inverse.RowErasure.goodUnion, OAI.MaxCutGames.Inverse.RowErasure.adviceMass

  38. theorem OAI.MaxCutGames.Inverse.RowErasure.advice_average_ge_ten_eta_sq_div_card line 389
  39. abbrev OAI.MaxCutGames.Inverse.Shortcode.F2 line 411
  40. abbrev OAI.MaxCutGames.Inverse.Shortcode.Vector line 412
  41. abbrev OAI.MaxCutGames.Inverse.Shortcode.Mat line 413
  42. def OAI.MaxCutGames.Inverse.Shortcode.rankOne line 415
  43. def OAI.MaxCutGames.Inverse.Shortcode.evaluate line 418
  44. theorem OAI.MaxCutGames.Inverse.Shortcode.evaluate_zero line 421
  45. theorem OAI.MaxCutGames.Inverse.Shortcode.rankOne_zero_left line 425
  46. theorem OAI.MaxCutGames.Inverse.Shortcode.rankOne_zero_right line 430
  47. def OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance line 437

    Source documentation

    Both perturbation factors are independent uniform vectors, including zero. The matrix is sampled independently as well.

    def equalityAcceptance {ell m : ℕ} (f : Mat ell m → Vector ell) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.Shortcode.Vector

  48. structure OAI.MaxCutGames.Inverse.Shortcode.Slice line 442

    Source documentation

    A description includes possibly dependent equations; the row and column counts need not equal their ranks.

    structure Slice (ell m : ℕ) where
…
  49. def OAI.MaxCutGames.Inverse.Shortcode.Slice.Contains line 450
  50. def OAI.MaxCutGames.Inverse.Shortcode.Slice.points line 454
  51. def OAI.MaxCutGames.Inverse.Shortcode.Slice.affineAgreement line 457
  52. def OAI.MaxCutGames.Inverse.Shortcode.Slice.constantAgreement line 461
  53. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.constantAgreement_eq_affine line 467

    Source documentation

    The fiber/Grassmann route produces the constant affine target 0,u. Keeping u is essential: this result does not claim a homogeneous target.

    theorem Slice.constantAgreement_eq_affine {ell m : ℕ} (S : Slice ell m)
    (f : Mat ell m → Vector ell) (u : Vector ell) :
    S.constantAgreement f u = S.affineAgreement f 0 u := by
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.Shortcode.Vector

  54. def OAI.MaxCutGames.Inverse.Shortcode.HasAffineSlice line 472
  55. theorem OAI.MaxCutGames.Inverse.Shortcode.hasAffineSlice_of_constant line 476
  56. def OAI.MaxCutGames.Inverse.Shortcode.InversePrinciple line 486

    Source documentation

    Dimension-uniform inverse statement. The constants α,r depend only on η; only the final input dimension threshold may depend on ell. There is no folding assumption, and no inverse-theorem certificate is hidden in f.

    def InversePrinciple : Prop :=
…
  57. abbrev OAI.MaxCutGames.Inverse.RowErasureDescriptions.RowMap line 509

    Source documentation

    A row map is represented by all its binary matrix coefficients.

    abbrev RowMap (ell r : ℕ) := Fin r → Vector ell
  58. abbrev OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description line 514

    Source documentation

    Ordered padded row coefficients, row values, column coefficients, column values, affine coefficient, and affine intercept. Redundant descriptions are intentional: counting descriptions provides an upper bound on distinct slices.

    abbrev Description (ell m r : ℕ) :=
…
  59. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.card_vector line 518
  60. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.card_rowMap line 521
  61. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.card_description line 524
  62. def OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.toSlice line 531
  63. def OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.coefficient line 539
  64. def OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.intercept line 542
  65. def OAI.MaxCutGames.Inverse.RowErasureDescriptions.padZero line 546

    Source documentation

    Add vacuous equations after the original finite list.

    def padZero {n r : ℕ} {V : Type*} [Zero V] (f : Fin n → V) : Fin r → V :=
…
  66. def OAI.MaxCutGames.Inverse.RowErasureDescriptions.padSlice line 549
  67. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.padSlice_contains_iff line 557
  68. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.padSlice_points line 581
  69. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.padSlice_affineAgreement line 588
  70. def OAI.MaxCutGames.Inverse.RowErasureDescriptions.describe line 594
  71. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.describe_toSlice line 599
  72. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.describe_coefficient line 603
  73. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.describe_intercept line 606
  74. theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.exists_description line 611

    Source documentation

    Every slice/target returned by the bounded inverse theorem has a fixed-size description with the same solution set and exactly the same agreement.

    theorem exists_description {ell m r : ℕ} (S : Slice ell m)
    (hrows : S.rows ≤ r) (hcols : S.columns ≤ r)
    (z : Vector m) (u : Vector ell) :
    ∃ d : Description ell m r, d.toSlice.points = S.points ∧
      d.coefficient = z ∧ d.intercept = u := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description

  75. def OAI.MaxCutGames.Inverse.RowErasureMatrix.rowAdvice line 628
  76. def OAI.MaxCutGames.Inverse.RowErasureMatrix.family line 631
  77. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.family_agreement line 645
  78. abbrev OAI.MaxCutGames.Inverse.RowErasureMatrix.Samples line 657
  79. def OAI.MaxCutGames.Inverse.RowErasureMatrix.left line 659
  80. def OAI.MaxCutGames.Inverse.RowErasureMatrix.right line 661
  81. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.expect_prod line 664
  82. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.left_uniform line 673
  83. def OAI.MaxCutGames.Inverse.RowErasureMatrix.stepEquiv line 681

    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.MaxCutGames.Inverse.RowErasureMatrix.Samples

  84. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.right_uniform line 693
  85. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.acceptance_eq line 700
  86. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.described_inverse line 719

    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.MaxCutGames.Inverse.Shortcode.equalityAcceptance, OAI.MaxCutGames.Inverse.RowErasure.equalityAcceptance, OAI.MaxCutGames.Inverse.RowErasureMatrix.left, OAI.MaxCutGames.Inverse.RowErasureMatrix.right

  87. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.advice_mass_ge_of_inverse_and_erasure line 739

    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.MaxCutGames.Inverse.Shortcode.equalityAcceptance, OAI.MaxCutGames.Inverse.RowErasureMatrix.family