AffineWitnessNormalizationLemmas.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The finite orbit count completing the first-bit witness normalization. The assumption in normalize_of_good_count is precisely that agreement is strictly greater than the reciprocal of the row-kernel cardinality, expressed without division. It is a quantitative goodness hypothesis, not an inverse theorem or a nonlinear rank premise.

abbrev OAI.UniqueGamesTheorem.Inverse.AffineWitness.Slice line 28
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.UniqueGamesTheorem.Inverse.AffineWitness.F2
def OAI.UniqueGamesTheorem.Inverse.AffineWitness.sliceShift line 31
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.sliceShift_zero line 37
theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.sliceShift_add line 44

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.agreement_count_le line 54

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

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.normalize_of_good_count line 80

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

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.normalize_of_density line 110

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
…

theorem OAI.UniqueGamesTheorem.Inverse.AffineWitness.first_bit_witness line 148