Identities.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

The unique selector in (A.4)

abbrev OAI.MaxCutGames.Appendix.Identities.Vector line 9
def OAI.MaxCutGames.Appendix.Identities.add line 11
def OAI.MaxCutGames.Appendix.Identities.zero line 13
theorem OAI.MaxCutGames.Appendix.Identities.add_assoc line 15
theorem OAI.MaxCutGames.Appendix.Identities.add_self line 20
theorem OAI.MaxCutGames.Appendix.Identities.add_zero line 24
theorem OAI.MaxCutGames.Appendix.Identities.zero_add line 28
theorem OAI.MaxCutGames.Appendix.Identities.add_comm line 32
theorem OAI.MaxCutGames.Appendix.Identities.add_shuffle line 36
structure OAI.MaxCutGames.Appendix.Identities.Subspace line 42
def OAI.MaxCutGames.Appendix.Identities.Subspace.Included line 47
structure OAI.MaxCutGames.Appendix.Identities.LinearMap line 50
def OAI.MaxCutGames.Appendix.Identities.Hybrid line 55
def OAI.MaxCutGames.Appendix.Identities.OuterHybrid line 66
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.MaxCutGames.Appendix.Identities.LinearMap, OAI.MaxCutGames.Appendix.Identities.Subspace
theorem OAI.MaxCutGames.Appendix.Identities.nested_hybrid_selector_iff line 77
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.MaxCutGames.Appendix.Identities.LinearMap, OAI.MaxCutGames.Appendix.Identities.Subspace, OAI.MaxCutGames.Appendix.Identities.Hybrid, OAI.MaxCutGames.Appendix.Identities.OuterHybrid
def OAI.MaxCutGames.Appendix.Identities.ImagesDisjointModulo line 117
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.MaxCutGames.Appendix.Identities.LinearMap, OAI.MaxCutGames.Appendix.Identities.Subspace
theorem OAI.MaxCutGames.Appendix.Identities.reverse_sum_image line 122
theorem OAI.MaxCutGames.Appendix.Identities.reverse_sum_preimage line 145
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.MaxCutGames.Appendix.Identities.LinearMap, OAI.MaxCutGames.Appendix.Identities.Subspace, OAI.MaxCutGames.Appendix.Identities.add, OAI.MaxCutGames.Appendix.Identities.Hybrid
def OAI.MaxCutGames.Appendix.LinearIdentities.Hybrid line 174
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.MaxCutGames.Appendix.LinearIdentities.compress line 178

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.MaxCutGames.Appendix.LinearIdentities.compress_apply line 181
theorem OAI.MaxCutGames.Appendix.LinearIdentities.compress_sub line 184
theorem OAI.MaxCutGames.Appendix.LinearIdentities.quotient_mem_image_iff line 189
theorem OAI.MaxCutGames.Appendix.LinearIdentities.nested_hybrid_iff line 196
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.MaxCutGames.Appendix.LinearIdentities.Hybrid, OAI.MaxCutGames.Appendix.LinearIdentities.compress
theorem OAI.MaxCutGames.Appendix.LinearIdentities.compress_rank_preserved line 248
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.MaxCutGames.Appendix.LinearIdentities.compress
theorem OAI.MaxCutGames.Appendix.LinearIdentities.reverse_hybrid_of_compressed_rankBelow line 276
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.MaxCutGames.Appendix.LinearIdentities.Hybrid, OAI.MaxCutGames.Appendix.RankAdditivity.RankBelow, OAI.MaxCutGames.Appendix.LinearIdentities.compress
theorem OAI.MaxCutGames.Appendix.LinearIdentities.rankBelow_of_compressed_rankBelow line 324
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.MaxCutGames.Appendix.LinearIdentities.Hybrid, OAI.MaxCutGames.Appendix.RankAdditivity.RankBelow, OAI.MaxCutGames.Appendix.LinearIdentities.compress
theorem OAI.MaxCutGames.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.MaxCutGames.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.MaxCutGames.Appendix.LinearIdentities.surviving_pair_forced line 382

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.MaxCutGames.Appendix.LinearIdentities.Hybrid, OAI.MaxCutGames.Appendix.RankAdditivity.RankBelow, OAI.MaxCutGames.Appendix.LinearIdentities.compress

theorem OAI.MaxCutGames.Appendix.LinearIdentities.canonical_inner_hybrid line 410
theorem OAI.MaxCutGames.Appendix.LinearIdentities.canonical_remainder_hybrid line 433
theorem OAI.MaxCutGames.Appendix.LinearIdentities.canonical_codomain_complement line 463
theorem OAI.MaxCutGames.Appendix.LinearIdentities.canonical_domain_complement line 489
theorem OAI.MaxCutGames.Appendix.LinearIdentities.compressed_rankBelow_of_hybrids line 525
theorem OAI.MaxCutGames.Appendix.LinearIdentities.reverse_outer_hybrid line 548

def OAI.MaxCutGames.Appendix.LinearIdentities.A5PairSurvives line 595

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.MaxCutGames.Appendix.LinearIdentities.a5_unique_selector line 605
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.MaxCutGames.Appendix.RankAdditivity.RankBelow, OAI.MaxCutGames.Appendix.LinearIdentities.Hybrid, OAI.MaxCutGames.Appendix.LinearIdentities.compress, OAI.MaxCutGames.Appendix.LinearIdentities.A5PairSurvives
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_codomain_forced line 634
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_domain_forced line 672
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_apply_on_preimage line 714
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_map_unique line 732
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_weak_selector_of_summand line 761
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_kernel_of_gluing line 790
theorem OAI.MaxCutGames.Appendix.LinearIdentities.disjoint_quotient_images_of_intersection line 831
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_range_of_gluing line 851
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_remainder_of_gluing line 878
abbrev OAI.MaxCutGames.Appendix.LinearIdentities.A4Index line 911
def OAI.MaxCutGames.Appendix.LinearIdentities.A4Survives line 914
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.MaxCutGames.Appendix.LinearIdentities.A4Index
theorem OAI.MaxCutGames.Appendix.LinearIdentities.a4_surviving_index_unique line 922
abbrev OAI.MaxCutGames.Appendix.BinaryA4.F2 line 946

theorem OAI.MaxCutGames.Appendix.BinaryA4.canonical_glued_map line 953

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.MaxCutGames.Appendix.BinaryA4.F2

theorem OAI.MaxCutGames.Appendix.BinaryA4.a4_selector_exists line 987
theorem OAI.MaxCutGames.Appendix.BinaryA4.a4_unique_selector line 1015
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.MaxCutGames.Appendix.BinaryA4.F2