OAI/Computability/MaxCut/Games/AffineWitness.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Conversion between explicitly listed affine column specifications and the span-based slice used in first-bit normalization.

  1. abbrev OAI.MaxCutGames.Inverse.AffineWitness.F2 line 12
  2. theorem OAI.MaxCutGames.Inverse.AffineWitness.add_self_binary line 19
  3. def OAI.MaxCutGames.Inverse.AffineWitness.InSlice line 28

    Source documentation

    A simultaneous row fiber and column slice, based at M₀. Agreement on Z is exactly agreement with all column specifications spanning Z.

    def InSlice (A : C →ₗ[F2] R) (Z : Submodule F2 D)
    (M₀ M : D →ₗ[F2] C) : Prop :=
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2

  4. theorem OAI.MaxCutGames.Inverse.AffineWitness.translate_target line 33

    Source documentation

    Changing the representative also changes the affine intercept.

    theorem translate_target (A : C →ₗ[F2] R) (Z : Submodule F2 D)
    (M₀ M : D →ₗ[F2] C) (hM : InSlice A Z M₀ M)
    (z w : D) (hw : w ∈ Z) (u : C) :
    M (z + w) + (u + M₀ w) = M z + u := by
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2, OAI.MaxCutGames.Inverse.AffineWitness.InSlice

  5. theorem OAI.MaxCutGames.Inverse.AffineWitness.no_affine_representative line 43
  6. def OAI.MaxCutGames.Inverse.AffineWitness.shift line 58

    Source documentation

    Rank-one translation in the row kernel.

    def shift (e : D →ₗ[F2] F2) (h : C) (M : D →ₗ[F2] C) : D →ₗ[F2] C :=
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2

  7. theorem OAI.MaxCutGames.Inverse.AffineWitness.shift_apply line 61
  8. theorem OAI.MaxCutGames.Inverse.AffineWitness.shift_zero line 64
  9. theorem OAI.MaxCutGames.Inverse.AffineWitness.shift_add line 69
  10. theorem OAI.MaxCutGames.Inverse.AffineWitness.shift_preserves_slice line 75
  11. theorem OAI.MaxCutGames.Inverse.AffineWitness.shift_preserves_target line 89
  12. theorem OAI.MaxCutGames.Inverse.AffineWitness.normalize line 95

    Source documentation

    Normalization preserves every affine target value on the complete slice.

    theorem normalize (e : D →ₗ[F2] F2) (A : C →ₗ[F2] R)
    (Z : Submodule F2 D) (M₀ : D →ₗ[F2] C) (z : D) (u : C)
    (h : ∃ w ∈ Z, e (z + w) = 1) :
    ∃ z' : D, ∃ u' : C, e z' = 1 ∧
      ∀ M, InSlice A Z M₀ M → M z' + u' = M z + u := by
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2, OAI.MaxCutGames.Inverse.AffineWitness.InSlice

  13. theorem OAI.MaxCutGames.Inverse.AffineWitness.columns_iff_span line 113
  14. theorem OAI.MaxCutGames.Inverse.AffineWitness.explicit_slice_iff line 128

    Source documentation

    A nonempty explicit affine row/column system is precisely the based slice. The right-hand sides S₀ and t are retained without homogenization.

    theorem explicit_slice_iff (A : C →ₗ[F2] R) (S₀ : D →ₗ[F2] R)
    (q : ι → D) (t : ι → C) (M₀ M : D →ₗ[F2] C)
    (hrow : A.comp M₀ = S₀) (hcol : ∀ i, M₀ (q i) = t i) :
    (A.comp M = S₀ ∧ ∀ i, M (q i) = t i) ↔
      InSlice A (Submodule.span F2 (Set.range q)) M₀ M := by
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2, OAI.MaxCutGames.Inverse.AffineWitness.InSlice

  15. theorem OAI.MaxCutGames.Inverse.AffineWitness.translate_explicit_target line 138

    Source documentation

    The affine target value after normalization is unchanged at every matrix satisfying the original, explicitly listed row and column equations.

    theorem translate_explicit_target (A : C →ₗ[F2] R) (S₀ : D →ₗ[F2] R)
    (q : ι → D) (t : ι → C) (M₀ M : D →ₗ[F2] C)
    (hrow₀ : A.comp M₀ = S₀) (hcol₀ : ∀ i, M₀ (q i) = t i)
    (hrow : A.comp M = S₀) (hcol : ∀ i, M (q i) = t i)
    (z w : D) (hw : w ∈ Submodule.span F2 (Set.range q)) (u : C) :
    M (z + w) + (u + M₀ w) = M z + u :=
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2

  16. theorem OAI.MaxCutGames.Inverse.folded_action_injective line 168

    Source documentation

    Translates of distinct agreement witnesses are distinct. The encoding need not be given as a homomorphism: only its injectivity and the displayed folding identity are needed for this conclusion.

    theorem folded_action_injective
    (shift : H → X → X)
    (shift_zero : ∀ x, shift 0 x = x)
    (shift_add : ∀ h k x, shift (h + k) x = shift h (shift k x))
    (embed : H → Y) (embed_injective : Function.Injective embed)
    (F target : X → Y)
    (folded : ∀ h x, F (shift h x) = F x + embed h)
    (target_invariant : ∀ h x, target (shift h x) = target x) :
    Function.Injective
      (fun a : H × {x : X // F x = target x} => shift a.1 a.2.val) := by
…
  17. theorem OAI.MaxCutGames.Inverse.folded_action_card_mul_agreement_le line 203

    Source documentation

    The agreement set of a folded function with an invariant target occupies at most the reciprocal of the size of the acting group, in denominator-free finite-cardinality form.

    theorem folded_action_card_mul_agreement_le
    [Fintype H] [Fintype X] [DecidableEq Y]
    (shift : H → X → X)
    (shift_zero : ∀ x, shift 0 x = x)
    (shift_add : ∀ h k x, shift (h + k) x = shift h (shift k x))
    (embed : H → Y) (embed_injective : Function.Injective embed)
    (F target : X → Y)
    (folded : ∀ h x, F (shift h x) = F x + embed h)
    (target_invariant : ∀ h x, target (shift h x) = target x) :
    Fintype.card H * Fintype.card {x : X // F x = target x} ≤
      Fintype.card X := by
…
  18. abbrev OAI.MaxCutGames.Inverse.AffineWitness.Slice line 238

    Source documentation

    The actual simultaneous row/column slice, including its affine offsets.

    abbrev Slice (A : C →ₗ[F2] R) (Z : Submodule F2 D) (M₀ : D →ₗ[F2] C) :=
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2

  19. def OAI.MaxCutGames.Inverse.AffineWitness.sliceShift line 241
  20. theorem OAI.MaxCutGames.Inverse.AffineWitness.sliceShift_zero line 247
  21. theorem OAI.MaxCutGames.Inverse.AffineWitness.sliceShift_add line 254
  22. theorem OAI.MaxCutGames.Inverse.AffineWitness.agreement_count_le line 264

    Source documentation

    If the affine coset misses first bit one, folding limits agreement to one point per row-kernel orbit. No rank-level inequality is used.

    theorem agreement_count_le [Finite D] [Finite C]
    (e : D →ₗ[F2] F2) (A : C →ₗ[F2] R)
    (Z : Submodule F2 D) (M₀ : D →ₗ[F2] C) (z : D) (u : C)
    (F : (D →ₗ[F2] C) → C)
    (hfold : ∀ (h : A.ker) M, F (shift e h M) = F M + h)
    (hno : ¬ ∃ w ∈ Z, e (z + w) = 1) :
    Nat.card A.ker * Nat.card {M : Slice A Z M₀ // F M = M.val z + u} ≤
      Nat.card (Slice A Z M₀) := by
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2, OAI.MaxCutGames.Inverse.AffineWitness.shift, OAI.MaxCutGames.Inverse.AffineWitness.Slice

  23. theorem OAI.MaxCutGames.Inverse.AffineWitness.normalize_of_good_count line 290

    Source documentation

    A good affine witness has a first-bit-one representative with an adjusted intercept, agreeing with the original target on every matrix of its slice.

    theorem normalize_of_good_count [Finite D] [Finite C]
    (e : D →ₗ[F2] F2) (A : C →ₗ[F2] R)
    (Z : Submodule F2 D) (M₀ : D →ₗ[F2] C) (z : D) (u : C)
    (F : (D →ₗ[F2] C) → C)
    (hfold : ∀ (h : A.ker) M, F (shift e h M) = F M + h)
    (hgood : Nat.card (Slice A Z M₀) <
      Nat.card A.ker * Nat.card {M : Slice A Z M₀ // F M = M.val z + u}) :
    ∃ z' : D, ∃ u' : C, e z' = 1 ∧
      ∀ M, InSlice A Z M₀ M → M z' + u' = M z + u := by
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2, OAI.MaxCutGames.Inverse.AffineWitness.shift, OAI.MaxCutGames.Inverse.AffineWitness.Slice, OAI.MaxCutGames.Inverse.AffineWitness.InSlice

  24. def OAI.MaxCutGames.Inverse.Shortcode.Slice.rowMap line 324

    Source documentation

    The simultaneous row functionals, allowing dependent and zero rows.

    def rowMap (S : Slice ell m) : Vector ell →ₗ[F2] Vector S.rows :=
…

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

  25. def OAI.MaxCutGames.Inverse.Shortcode.Slice.columnSpan line 328

    Source documentation

    Column specifications fix the matrix on this entire subspace.

    def columnSpan (S : Slice ell m) : Submodule F2 (Vector m) :=
…

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

  26. abbrev OAI.MaxCutGames.Inverse.Shortcode.Slice.Directions line 332

    Source documentation

    Free directions of a row/column slice, intrinsically as quotient maps.

    abbrev Directions (S : Slice ell m) :=
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice

  27. def OAI.MaxCutGames.Inverse.Shortcode.Slice.directionMap line 335
  28. def OAI.MaxCutGames.Inverse.Shortcode.Slice.directionMatrix line 339
  29. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.directionMatrix_injective line 342
  30. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.directionMatrix_row line 353
  31. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.directionMatrix_column line 362
  32. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.contains_add_direction line 372
  33. def OAI.MaxCutGames.Inverse.Shortcode.Slice.directionEmbedding line 389
  34. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.columnSpan_finrank_le line 399
  35. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.quotient_finrank_ge line 407
  36. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.rowKernel_finrank_ge line 415
  37. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.card_directions line 424
  38. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.card_directions_le line 432

    Source documentation

    A nonempty affine slice is at least as large as its free-direction space.

    theorem card_directions_le (S : Slice ell m) (hne : S.points.Nonempty) :
    Nat.card S.Directions ≤ S.points.card := by
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice

  39. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.pow_dimension_le_card line 443

    Source documentation

    The actual v2 bound, with truncation making it valid also in small dimensions. There is no independence hypothesis on the listed equations.

    theorem pow_dimension_le_card (S : Slice ell m) (r : ℕ)
    (hrows : S.rows ≤ r) (hcolumns : S.columns ≤ r)
    (hne : S.points.Nonempty) :
    2 ^ ((ell - r) * (m - r)) ≤ S.points.card := by
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice

  40. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.evaluate_eq_toLin line 469
  41. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.row_equations_iff line 472
  42. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.contains_iff_inSlice line 495

    Source documentation

    This is an equivalence of the actual equations, not merely a cardinality comparison or a homogeneous approximation of the affine slice.

    theorem contains_iff_inSlice (S : Slice ell m) (M₀ : Mat ell m)
    (hM₀ : S.Contains M₀) (M : Mat ell m) :
    S.Contains M ↔
      AffineWitness.InSlice S.rowMap S.columnSpan
        (Matrix.toLin' M₀) (Matrix.toLin' M) := by
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.AffineWitness.InSlice

  43. def OAI.MaxCutGames.Inverse.Shortcode.Slice.linearSliceEquiv line 515

    Source documentation

    Exact finite sample-space equivalence between the matrix representation and the linear-map representation of a nonempty affine slice.

    def linearSliceEquiv (S : Slice ell m) (M₀ : Mat ell m)
    (hM₀ : S.Contains M₀) :
    S.points ≃ AffineWitness.Slice S.rowMap S.columnSpan (Matrix.toLin' M₀) where
…

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

  44. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.affineAgreement_eq_of_target_eq line 534

    Source documentation

    Pointwise preservation on the genuine slice preserves its exact uniform affine agreement, including the empty-slice convention.

    theorem affineAgreement_eq_of_target_eq (S : Slice ell m)
    (f : Mat ell m → Vector ell) (z z' : Vector m) (u u' : Vector ell)
    (htarget : ∀ M, S.Contains M → evaluate M z' + u' = evaluate M z + u) :
    S.affineAgreement f z' u' = S.affineAgreement f z u := by
…

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

  45. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.affineAgreement_eq_of_linear_target_eq line 545
  46. theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.affineAgreement_translate line 557

    Source documentation

    Changing the representative inside the column span and correcting the intercept leaves the shortcode agreement exactly unchanged.

    theorem affineAgreement_translate (S : Slice ell m)
    (M₀ : Mat ell m) (hM₀ : S.Contains M₀)
    (f : Mat ell m → Vector ell) (z w : Vector m) (hw : w ∈ S.columnSpan)
    (u : Vector ell) :
    S.affineAgreement f (z + w) (u + evaluate M₀ w) =
      S.affineAgreement f z u := by
…

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

  47. theorem OAI.MaxCutGames.Inverse.AffineWitness.normalize_of_density line 582

    Source documentation

    An agreement lower bound above the inverse row-kernel size produces a first-bit-one representative while preserving the entire affine target.

    theorem normalize_of_density [Finite D] [Finite C]
    (e : D →ₗ[F2] F2) (A : C →ₗ[F2] R)
    (Z : Submodule F2 D) (M₀ : D →ₗ[F2] C) (z : D) (u : C)
    (F : (D →ₗ[F2] C) → C)
    (hfold : ∀ (h : A.ker) M, F (shift e h M) = F M + h)
    (η : ℝ)
    (hgood : η ≤
      (Nat.card {M : Slice A Z M₀ // F M = M.val z + u} : ℝ) /
        (Nat.card (Slice A Z M₀) : ℝ))
    (hsize : 1 < η * (Nat.card A.ker : ℝ)) :
    ∃ z' : D, ∃ u' : C, e z' = 1 ∧
      ∀ M, InSlice A Z M₀ M → M z' + u' = M z + u := by
…

    Mentions: OAI.MaxCutGames.Inverse.AffineWitness.F2, OAI.MaxCutGames.Inverse.AffineWitness.shift, OAI.MaxCutGames.Inverse.AffineWitness.Slice, OAI.MaxCutGames.Inverse.AffineWitness.InSlice