CompressionCountLemmas.lean`

76 declarations, 0 contain sorry, 0 declared as axioms

The actual Appendix A.4 index encoding. Its kernel and range recover the two subspaces, and its quotient relation recovers the linear map. The final count follows from this injection into a genuine binary linear-map space.

def OAI.UniqueGamesTheorem.Appendix.CompressionCount.base line 28
Source documentation
Canonical rank-dim U map.
```
def base : (U × K) →ₗ[F2] (U × C) :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.base_apply line 31
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.compress line 37
Source documentation
Compress by restricting to the second domain factor and taking the second codomain coordinate.
```
def compress (Y : (U × K) →ₗ[F2] (U × C)) : K →ₗ[F2] C :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.compress_apply line 40
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber line 45
Source documentation
The actual rank-order compression fiber; subtraction agrees with addition over the binary field.
```
def Fiber (Z : K →ₗ[F2] C) :=
…
```
abbrev OAI.UniqueGamesTheorem.Appendix.CompressionCount.Parameters line 50
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.graph line 53
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.inclusion line 56
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.lower line 59
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.lift line 63
Source documentation
The block matrix [I+FH,FZ;H,Z].
```
def lift (Z : K →ₗ[F2] C) (P : Parameters (U := U) Z) :
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CompressionCount.Parameters
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.lift_apply line 67
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.compress_lift line 73
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.graph_injective line 78
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.inclusion_injective line 83
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.lower_surjective line 89
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.range_lift_sub_base line 96
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.range_lift line 102
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.finrank_base line 122
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.lift_rank_order line 127
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.toFiber line 134
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.lift_injective line 138
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.natCard_linearMap line 152
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.card_parameters line 165
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.fiber_geometry line 173
Source documentation
Rank additivity supplies exactly the image/kernel hypotheses used by the block argument.
```
theorem fiber_geometry (Z : K →ₗ[F2] C) (Y : Fiber (U := U) Z) :
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.snd_mem_range line 183
Source documentation
Every lower coordinate of a map in the fiber lies in the compressed image. This is the step that permits taking H : U → range Z.
```
theorem snd_mem_range (Z : K →ₗ[F2] C) (Y : Fiber (U := U) Z) (p : U × K) :
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.linearSection line 201
Source documentation
Choose a linear section of the map onto its image.
```
noncomputable def linearSection (Z : K →ₗ[F2] C) : Z.range →ₗ[F2] K :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.section_spec line 205
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.extractedF line 210
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.extractedH line 215
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.extracted_lower line 220
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.difference_ext_snd line 232
Source documentation
On the difference image, the lower coordinate uniquely determines the upper coordinate.
```
theorem difference_ext_snd (Z : K →ₗ[F2] C) (Y : Fiber (U := U) Z)
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.lift_extracted line 247
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.toFiber_bijective line 270
def OAI.UniqueGamesTheorem.Appendix.CompressionCount.fiberEquiv line 280
Source documentation
The exact compression fiber is in bijection with two independent spaces of linear maps. No rank or cardinality claim is an assumption of this equivalence.
```
noncomputable def fiberEquiv (Z : K →ₗ[F2] C) :
    Parameters (U := U) Z ≃ Fiber (U := U) Z :=
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CompressionCount.Parameters, OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.fiber_remainder_rank line 284
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.fiber_rank line 291
theorem OAI.UniqueGamesTheorem.Appendix.CompressionCount.card_fiber line 296
Source documentation
Lemma A.2 in arbitrary finite-dimensional block coordinates.
```
theorem card_fiber (Z : K →ₗ[F2] C) : Nat.card (Fiber (U := U) Z) =
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
def OAI.UniqueGamesTheorem.Appendix.A4IndexCount.factorViaRange line 319
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.factorViaRange_apply line 326
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.factorViaRange_injective line 337
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.factorViaRange_range line 355
def OAI.UniqueGamesTheorem.Appendix.A4IndexCount.quotientRestriction line 372
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.ker_quotientRestriction line 375
def OAI.UniqueGamesTheorem.Appendix.A4IndexCount.aToRange line 381
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.aToRange_surjective line 388
def OAI.UniqueGamesTheorem.Appendix.A4IndexCount.encodeFixed line 396
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.encodeFixed_relation line 403
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.ker_encodeFixed line 416
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.range_encodeFixed line 424
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.recover_A0 line 432
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.recover_B0 line 445
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.encodeFixed_injective line 463
def OAI.UniqueGamesTheorem.Appendix.A4IndexCount.Valid line 480
abbrev OAI.UniqueGamesTheorem.Appendix.A4IndexCount.Index line 485
abbrev OAI.UniqueGamesTheorem.Appendix.A4IndexCount.GeometricIndex line 488
def OAI.UniqueGamesTheorem.Appendix.A4IndexCount.encode line 490
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.encode_injective line 495
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.card_index_le line 529
theorem OAI.UniqueGamesTheorem.Appendix.A4IndexCount.card_geometricIndex_le line 539
def OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.complementRangeEquiv line 561
Source documentation
A complement to the kernel maps isomorphically onto the range.
```
def complementRangeEquiv (X : E →ₗ[𝕜] F) (P : Submodule 𝕜 E)
    (hP : IsCompl X.ker P) : P ≃ₗ[𝕜] X.range :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.complementRangeEquiv_apply line 565
def OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.domainEquiv line 571
Source documentation
Domain coordinates, with the first coordinate literally in range X.
```
def domainEquiv (X : E →ₗ[𝕜] F) (P : Submodule 𝕜 E)
    (hP : IsCompl X.ker P) : (X.range × X.ker) ≃ₗ[𝕜] E :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.apply_domainEquiv line 577
Source documentation
The domain equivalence exhibits precisely the image coordinate of X.
```
@[simp] theorem apply_domainEquiv (X : E →ₗ[𝕜] F)
    (P : Submodule 𝕜 E) (hP : IsCompl X.ker P) (u : X.range) (k : X.ker) :
    X (domainEquiv X P hP (u, k)) = (u : F) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.domainEquiv
def OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.codomainEquiv line 587
Source documentation
Codomain coordinates split the range off from a chosen complement.
```
def codomainEquiv (X : E →ₗ[𝕜] F) (C : Submodule 𝕜 F)
    (hC : IsCompl X.range C) : (X.range × C) ≃ₗ[𝕜] F :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.canonical_block line 592
Source documentation
An arbitrary map has the canonical compression-fiber block form.
```
theorem canonical_block (X : E →ₗ[𝕜] F) (P : Submodule 𝕜 E)
    (hP : IsCompl X.ker P) (C : Submodule 𝕜 F)
    (hC : IsCompl X.range C) (u : X.range) (k : X.ker) :
    (codomainEquiv X C hC).symm (X (domainEquiv X P hP (u, k))) = (u, 0) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.codomainEquiv, OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.domainEquiv
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.exists_canonical_coordinates line 601
Source documentation
Choice of complements is available over every field; this is an actual normal-form existence result, including zero-dimensional kernel/range cases.
```
theorem exists_canonical_coordinates (X : E →ₗ[𝕜] F) :
    ∃ (P : Submodule 𝕜 E) (C : Submodule 𝕜 F)
      (hP : IsCompl X.ker P) (hC : IsCompl X.range C),
      ∀ (u : X.range) (k : X.ker),
        (codomainEquiv X C hC).symm (X (domainEquiv X P hP (u, k))) = (u, 0) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.codomainEquiv, OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.domainEquiv
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.domainEquiv_zero_left line 610
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.quotient_coordinates line 616

def OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.toBlocks line 623

Source documentation

Re-express all maps in the chosen domain/codomain coordinates at once.

def toBlocks (X : E →ₗ[𝕜] F) (P : Submodule 𝕜 E)
    (hP : IsCompl X.ker P) (C : Submodule 𝕜 F) (hC : IsCompl X.range C) :
    (E →ₗ[𝕜] F) ≃ₗ[𝕜] ((X.range × X.ker) →ₗ[𝕜] (X.range × C)) :=
…

theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.toBlocks_apply line 628
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.compressed_toBlocks line 637
Source documentation
The lower-right block is exactly the original quotient restriction, transported through the quotient/complement equivalence.
```
theorem compressed_toBlocks (X Y : E →ₗ[𝕜] F) (P : Submodule 𝕜 E)
    (hP : IsCompl X.ker P) (C : Submodule 𝕜 F) (hC : IsCompl X.range C)
    (k : X.ker) :
    (toBlocks X P hP C hC Y (0, k)).2 =
      X.range.quotientEquivOfIsCompl C hC (X.range.mkQ (Y k)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.toBlocks
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.toBlocks_base line 644
def OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.rangeTransport line 658
Source documentation
Changing coordinates induces a genuine linear equivalence on ranges.
```
def rangeTransport (e : E ≃ₗ[𝕜] U) (f : F ≃ₗ[𝕜] V) (Y : E →ₗ[𝕜] F) :
    Y.range ≃ₗ[𝕜] (LinearEquiv.arrowCongr e f Y).range where
…
```
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.finrank_range_transport line 673
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.finrank_toBlocks line 681
theorem OAI.UniqueGamesTheorem.Appendix.CoordinateTransport.finrank_comp_equiv line 687