AffineWitnessLemmas.lean`

23 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.

abbrev OAI.UniqueGamesTheorem.Inverse.AffineWitness.F2 line 21
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.add_self_binary line 28
def OAI.UniqueGamesTheorem.Inverse.AffineWitness.InSlice line 37
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.UniqueGamesTheorem.Inverse.AffineWitness.F2
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.translate_target line 42
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.UniqueGamesTheorem.Inverse.AffineWitness.F2, OAI.UniqueGamesTheorem.Inverse.AffineWitness.InSlice
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.no_affine_representative line 52
def OAI.UniqueGamesTheorem.Inverse.AffineWitness.shift line 67
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.UniqueGamesTheorem.Inverse.AffineWitness.F2
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.shift_apply line 70
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.shift_zero line 73
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.shift_add line 78
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.shift_preserves_slice line 84
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.shift_preserves_target line 98

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.normalize line 104

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.UniqueGamesTheorem.Inverse.AffineWitness.F2, OAI.UniqueGamesTheorem.Inverse.AffineWitness.InSlice

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.columns_iff_span line 128
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.explicit_slice_iff line 142
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.UniqueGamesTheorem.Inverse.AffineWitness.F2, OAI.UniqueGamesTheorem.Inverse.AffineWitness.InSlice

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.translate_explicit_target line 152

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.UniqueGamesTheorem.Inverse.AffineWitness.F2

theorem OAI.UniqueGamesTheorem.Inverse.folded_action_injective line 186

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
…

theorem OAI.UniqueGamesTheorem.Inverse.folded_action_card_mul_agreement_le line 221

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
…

theorem OAI.UniqueGamesTheorem.Inverse.card_finset_subtype_eq_filter_card line 261
Source documentation
Filtering a finite sample set counts the same objects as first restricting to the sample set and then imposing the event predicate.
```
theorem card_finset_subtype_eq_filter_card (s : Finset X)
    (p : X → Prop) [DecidablePred p] :
    Nat.card {x : s // p x.val} = (s.filter p).card := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.finset_expect_indicator_eq_card_ratio line 277

Source documentation

An indicator's expectation on a finite set is its agreement count divided by the cardinality of that same finite set.

theorem finset_expect_indicator_eq_card_ratio (s : Finset X)
    (p : X → Prop) [DecidablePred p] :
    s.expect (fun x => if p x then (1 : ℝ) else 0) =
      (Nat.card {x : s // p x.val} : ℝ) / (Nat.card s : ℝ) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.nat_card_subtype_equiv line 286
Source documentation
A bijection preserving the event preserves its count. No choice of a Fintype enumeration is involved in this identity.
```
theorem nat_card_subtype_equiv (e : X ≃ Y) (p : X → Prop) (q : Y → Prop)
    (h : ∀ x, p x ↔ q (e x)) :
    Nat.card {x : X // p x} = Nat.card {y : Y // q y} :=
…
```

theorem OAI.UniqueGamesTheorem.Inverse.finset_expect_indicator_eq_card_ratio_of_equiv line 293

Source documentation

Transfer the indicator expectation through an equivalence of the complete finite sample space, including the denominator of the conditional law.

theorem finset_expect_indicator_eq_card_ratio_of_equiv (s : Finset X)
    (p : X → Prop) [DecidablePred p] (e : ↥s ≃ Y) (q : Y → Prop)
    (h : ∀ x : s, p x.val ↔ q (e x)) :
    s.expect (fun x => if p x then (1 : ℝ) else 0) =
      (Nat.card {y : Y // q y} : ℝ) / (Nat.card Y : ℝ) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.binary_kernel_finrank_lower line 321

Source documentation

Even dependent binary row constraints remove at most one dimension per row.

theorem binary_kernel_finrank_lower {ℓ r : ℕ}
    (A : (Fin ℓ → ZMod 2) →ₗ[ZMod 2] (Fin r → ZMod 2)) :
    ℓ - r ≤ Module.finrank (ZMod 2) A.ker := by
…

theorem OAI.UniqueGamesTheorem.Inverse.binary_kernel_card_lower line 337

Source documentation

The cardinality of the binary row kernel is at least 2^(ℓ-r).

theorem binary_kernel_card_lower {ℓ r : ℕ}
    (A : (Fin ℓ → ZMod 2) →ₗ[ZMod 2] (Fin r → ZMod 2)) :
    2 ^ (ℓ - r) ≤ Nat.card A.ker := by
…