Identities.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

The unique selector in (A.4)

abbrev OAI.UniqueGamesTheorem.Appendix.Identities.Vector line 13
def OAI.UniqueGamesTheorem.Appendix.Identities.add line 15
def OAI.UniqueGamesTheorem.Appendix.Identities.zero line 17
theorem OAI.UniqueGamesTheorem.Appendix.Identities.add_assoc line 19
theorem OAI.UniqueGamesTheorem.Appendix.Identities.add_self line 24
theorem OAI.UniqueGamesTheorem.Appendix.Identities.add_zero line 28
theorem OAI.UniqueGamesTheorem.Appendix.Identities.zero_add line 32
theorem OAI.UniqueGamesTheorem.Appendix.Identities.add_comm line 36
theorem OAI.UniqueGamesTheorem.Appendix.Identities.add_shuffle line 40
structure OAI.UniqueGamesTheorem.Appendix.Identities.Subspace line 46
def OAI.UniqueGamesTheorem.Appendix.Identities.Subspace.Included line 51
structure OAI.UniqueGamesTheorem.Appendix.Identities.LinearMap line 54
def OAI.UniqueGamesTheorem.Appendix.Identities.Hybrid line 59
def OAI.UniqueGamesTheorem.Appendix.Identities.OuterHybrid line 70
Source documentation
The hybrid selector for Q_A₀ Y|_B₀ at (A/A₀, B).
The first component states that every coset of A/A₀ has a preimage in B₀; the second states that the preimage of A/A₀ is contained in B. A₀ ≤ A and B ≤ B₀ are supplied by the composition theorem.
```
def OuterHybrid {n m : Nat} (Y : LinearMap n m)
    (A₀ A : Subspace m) (B B₀ : Subspace n) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Identities.LinearMap, OAI.UniqueGamesTheorem.Appendix.Identities.Subspace
theorem OAI.UniqueGamesTheorem.Appendix.Identities.nested_hybrid_selector_iff line 81
Source documentation
Equation (A.3), at the level of the exact character selectors.
In particular the forward proof checks the subtle point that the outer image condition forces the full preimage Y⁻¹(A) into B₀.
```
theorem nested_hybrid_selector_iff {n m : Nat} (Y : LinearMap n m)
    (A₀ A : Subspace m) (B B₀ : Subspace n)
    (hA : A₀.Included A) (hB : B.Included B₀) :
    (Hybrid Y A₀ B₀ ∧ OuterHybrid Y A₀ A B B₀) ↔ Hybrid Y A B := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Identities.LinearMap, OAI.UniqueGamesTheorem.Appendix.Identities.Subspace, OAI.UniqueGamesTheorem.Appendix.Identities.Hybrid, OAI.UniqueGamesTheorem.Appendix.Identities.OuterHybrid
def OAI.UniqueGamesTheorem.Appendix.Identities.ImagesDisjointModulo line 121
Source documentation
Disjointness of the images of Q_A X|_B and Q_A Z|_B, written without quotient objects. Equality of the two cosets means their sum lies in A, in which case both cosets must be zero.
```
def ImagesDisjointModulo {n m : Nat} (X Z : LinearMap n m)
    (A : Subspace m) (B : Subspace n) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Identities.LinearMap, OAI.UniqueGamesTheorem.Appendix.Identities.Subspace
theorem OAI.UniqueGamesTheorem.Appendix.Identities.reverse_sum_image line 126
theorem OAI.UniqueGamesTheorem.Appendix.Identities.reverse_sum_preimage line 149
Source documentation
The second asserted implication in the reverse direction of (A.5).
covered expresses B₀ + ker X = W; localLift expresses im (Q_A₀ X|_B₀) ≤ im (Q_A₀ Y|_B₀). The rank-additive summand gives the latter inclusion. This theorem checks the passage from those specific linear-algebra hypotheses to the full preimage inclusion.
```
theorem reverse_sum_preimage {n m : Nat} (X Y Z : LinearMap n m)
    (A₀ : Subspace m) (B₀ : Subspace n)
    (hZ : ∀ w, Z.apply w = add (Y.apply w) (X.apply w))
    (inner : Hybrid Y A₀ B₀)
    (covered : ∀ w, ∃ b, B₀.mem b ∧ X.apply b = X.apply w)
    (localLift : ∀ b, B₀.mem b →
      ∃ c, B₀.mem c ∧ A₀.mem (add (Y.apply c) (X.apply b))) :
    ∀ w, A₀.mem (Z.apply w) → B₀.mem w := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Identities.LinearMap, OAI.UniqueGamesTheorem.Appendix.Identities.Subspace, OAI.UniqueGamesTheorem.Appendix.Identities.add, OAI.UniqueGamesTheorem.Appendix.Identities.Hybrid
def OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid line 178
Source documentation
The actual hybrid selector from Appendix A.1, for genuine linear maps.
```
def Hybrid (Y : W →ₗ[K] V) (A : Submodule K V) (B : Submodule K W) : Prop :=
…
```

def OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress line 182

Source documentation

The compressed dual frequency Q_A Y|_B.

def compress (Y : W →ₗ[K] V) (A : Submodule K V) (B : Submodule K W) :
    B →ₗ[K] (V ⧸ A) := A.mkQ.comp (Y.domRestrict B)

theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress_apply line 185
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress_sub line 188
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.quotient_mem_image_iff line 193
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.nested_hybrid_iff line 200
Source documentation
The exact nested-selector equivalence of (A.3), now using Mathlib's linear maps, submodules, restriction, and quotient construction.
```
theorem nested_hybrid_iff (Y : W →ₗ[K] V) (A₀ A : Submodule K V)
    (B B₀ : Submodule K W) (hA : A₀ ≤ A) (hB : B ≤ B₀) :
    (Hybrid Y A₀ B₀ ∧
      Hybrid (compress Y A₀ B₀) (A.map A₀.mkQ) (B.comap B₀.subtype)) ↔
    Hybrid Y A B := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress_rank_preserved line 251
Source documentation
Compression preserves the full rank when its quotient is disjoint from the image and its restricted domain spans the domain modulo the kernel.
```
theorem compress_rank_preserved (X : W →ₗ[K] V)
    (A : Submodule K V) (B : Submodule K W)
    (hdis : Disjoint A (LinearMap.range X))
    (hcover : B ⊔ LinearMap.ker X = ⊤) :
    Module.finrank K (LinearMap.range (compress X A B)) =
      Module.finrank K (LinearMap.range X) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.reverse_hybrid_of_compressed_rankBelow line 278
Source documentation
The reverse summand of (A.5) really satisfies the hybrid selector for the remainder Y - X. The hypotheses here are exactly the inner hybrid selector, complement conditions, and the compressed rank-order selector. No image-lifting or disjointness conclusion is assumed separately.
```
theorem reverse_hybrid_of_compressed_rankBelow (X Y : W →ₗ[K] V)
    (A₀ : Submodule K V) (B₀ : Submodule K W)
    (inner : Hybrid Y A₀ B₀)
    (hdis : Disjoint A₀ (LinearMap.range X))
    (hcover : B₀ ⊔ LinearMap.ker X = ⊤)
    (hlocal : RankAdditivity.RankBelow (compress X A₀ B₀) (compress Y A₀ B₀)) :
    Hybrid (Y - X) A₀ B₀ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid, OAI.UniqueGamesTheorem.Appendix.RankAdditivity.RankBelow, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.rankBelow_of_compressed_rankBelow line 325
Source documentation
A surviving right-hand summand of (A.5) forces the original rank order X ⪯ Y. This lifts the local rank equation using the two actual hybrid rank-loss equalities, so it does not assume global rank additivity.
```
theorem rankBelow_of_compressed_rankBelow (X Y : W →ₗ[K] V)
    (A₀ : Submodule K V) (B₀ : Submodule K W)
    (inner : Hybrid Y A₀ B₀)
    (hdis : Disjoint A₀ (LinearMap.range X))
    (hcover : B₀ ⊔ LinearMap.ker X = ⊤)
    (hlocal : RankAdditivity.RankBelow (compress X A₀ B₀) (compress Y A₀ B₀)) :
    RankAdditivity.RankBelow X Y := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid, OAI.UniqueGamesTheorem.Appendix.RankAdditivity.RankBelow, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.image_inter_complement_eq line 350
Source documentation
The complement in the codomain is forced by the remainder image.
```
theorem image_inter_complement_eq (A₀ I J : Submodule K V)
    (hA : A₀ ≤ J) (hdis : Disjoint I J) : J ⊓ (A₀ ⊔ I) = A₀ := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.domain_complement_eq line 367
Source documentation
The complement in the domain is forced by the remainder kernel.
```
theorem domain_complement_eq (B₀ K₀ J : Submodule K W)
    (hJ : J ≤ B₀) (hcover : K₀ ⊔ J = ⊤) : B₀ = (B₀ ⊓ K₀) ⊔ J := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.surviving_pair_forced line 381

Source documentation

Every surviving right-hand pair in (A.5) is the displayed canonical pair.

theorem surviving_pair_forced (X Y : W →ₗ[K] V)
    (A₀ A : Submodule K V) (B B₀ : Submodule K W)
    (inner : Hybrid Y A₀ B₀)
    (hdis : Disjoint A₀ (LinearMap.range X))
    (hA : A₀ ⊔ LinearMap.range X = A)
    (hcover : B₀ ⊔ LinearMap.ker X = ⊤)
    (hB : B₀ ⊓ LinearMap.ker X = B)
    (hlocal : RankAdditivity.RankBelow (compress X A₀ B₀) (compress Y A₀ B₀)) :
    A₀ = LinearMap.range (Y - X) ⊓ A ∧ B₀ = B ⊔ LinearMap.ker (Y - X) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid, OAI.UniqueGamesTheorem.Appendix.RankAdditivity.RankBelow, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress

theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.canonical_inner_hybrid line 408
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.canonical_remainder_hybrid line 430
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.canonical_codomain_complement line 459
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.canonical_domain_complement line 484
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compressed_rankBelow_of_hybrids line 519
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.reverse_outer_hybrid line 541
def OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A5PairSurvives line 588
Source documentation
The precise right-hand pair selector of (A.5).
```
def A5PairSurvives (X Y : W →ₗ[K] V) (A : Submodule K V) (B : Submodule K W)
    (p : Submodule K V × Submodule K W) : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a5_unique_selector line 597
Source documentation
The complete unique-summand selector identity in (A.5), in arbitrary finite dimensions. In characteristic two the remainder Y-X is Y+X.
```
theorem a5_unique_selector (X Y : W →ₗ[K] V)
    (A : Submodule K V) (B : Submodule K W)
    (hI : LinearMap.range X ≤ A) (hB : B ≤ LinearMap.ker X) :
    (RankAdditivity.RankBelow X Y ∧
      Hybrid (compress Y (LinearMap.range X) (LinearMap.ker X))
        (A.map (LinearMap.range X).mkQ) (B.comap (LinearMap.ker X).subtype)) ↔
      ∃! p : Submodule K V × Submodule K W, A5PairSurvives X Y A B p := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.RankAdditivity.RankBelow, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.Hybrid, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A5PairSurvives
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_codomain_forced line 625
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_domain_forced line 662
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_apply_on_preimage line 703
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_map_unique line 720
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_weak_selector_of_summand line 748
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_kernel_of_gluing line 777
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.disjoint_quotient_images_of_intersection line 817
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_range_of_gluing line 837
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_remainder_of_gluing line 864
abbrev OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A4Index line 897
def OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A4Survives line 900
Source documentation
The full index and selectors of a right-hand summand of (A.4).
```
def A4Survives (Y : W →ₗ[K] V) (A : Submodule K V) (B : Submodule K W)
    (p : A4Index (K := K) (W := W) (V := V)) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.A4Index
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a4_surviving_index_unique line 907
abbrev OAI.UniqueGamesTheorem.Appendix.BinaryA4.F2 line 931

theorem OAI.UniqueGamesTheorem.Appendix.BinaryA4.canonical_glued_map line 938

Source documentation

Construct the actual linear map in the canonical (A.4) summand by gluing zero on B with Q_A₀ Y on Y⁻¹(A).

theorem canonical_glued_map (Y : W →ₗ[F2] V) (A : Submodule F2 V) (B : Submodule F2 W) :
    ∃ X : ↥(B ⊔ A.comap Y) →ₗ[F2] (V ⧸ ((B.map Y) ⊓ A)),
      (∀ b : ↥(B ⊔ A.comap Y), (b : W) ∈ B → X b = 0) ∧
      (∀ p : ↥(B ⊔ A.comap Y), Y p ∈ A → X p = ((B.map Y) ⊓ A).mkQ (Y p)) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.BinaryA4.F2

theorem OAI.UniqueGamesTheorem.Appendix.BinaryA4.a4_selector_exists line 972
theorem OAI.UniqueGamesTheorem.Appendix.BinaryA4.a4_unique_selector line 1000
Source documentation
The complete unique-index selector identity in (A.4) for arbitrary finite-dimensional binary vector spaces. The index records both subspaces and the genuine linear map with the required kernel and range.
```
theorem a4_unique_selector (Y : W →ₗ[F2] V) (A : Submodule F2 V) (B : Submodule F2 W) :
    (A ≤ LinearMap.range Y ∧ LinearMap.ker Y ≤ B) ↔
      ∃! p : A4Index (K := F2) (W := W) (V := V), A4Survives Y A B p := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.BinaryA4.F2