MatrixChartLemmas.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Concrete matrix coordinates for the graph chart. In particular the upper interval equations become M q = t, while the lower equations become dᵀ M = sᵀ. The right-hand sides are retained; none of these slices is required to be linear.

def OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphEquiv line 22
Source documentation
The first coordinate identifies the graph with its domain.
```
def graphEquiv (T : X →ₗ[K] Y) : X ≃ₗ[K] T.graph where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.graph_injective line 36
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.exists_unique_graph_iff line 45
Source documentation
Membership in the graph chart is precisely invertibility of the first projection; this includes both existence and uniqueness of the matrix.
```
theorem exists_unique_graph_iff (L : Submodule K (X × Y)) :
    (∃! T : X →ₗ[K] Y, L = T.graph) ↔
      Function.Bijective (fun x : L => x.val.1) := by
…
```
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.intersectionEquiv line 58
Source documentation
Common graph vectors correspond exactly to the kernel of the difference.
```
def intersectionEquiv (T U : X →ₗ[K] Y) :
    LinearMap.ker (T - U) ≃ₗ[K] (T.graph ⊓ U.graph : Submodule K (X × Y)) where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.finrank_graph line 78

theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.finrank_intersection_add_rank line 83

Source documentation

Rank-nullity in the graph chart, without truncated natural subtraction.

theorem finrank_intersection_add_rank [FiniteDimensional K X] (T U : X →ₗ[K] Y) :
    Module.finrank K (T.graph ⊓ U.graph : Submodule K (X × Y)) +
      Module.finrank K (LinearMap.range (T - U)) = Module.finrank K X := by
…

theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.adjacent_iff_rank_one line 90

Source documentation

Grassmann adjacency within the chart is exactly rank-one difference.

theorem adjacent_iff_rank_one [FiniteDimensional K X] (T U : X →ₗ[K] Y) :
    Module.finrank K (T.graph ⊓ U.graph : Submodule K (X × Y)) + 1 =
        Module.finrank K X ↔
      Module.finrank K (LinearMap.range (T - U)) = 1 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.adjacent_rank_one_step line 98

Source documentation

A nonzero rank-one perturbation gives an adjacent graph vertex.

theorem adjacent_rank_one_step [FiniteDimensional K X]
    (T : X →ₗ[K] Y) (a : X →ₗ[K] K) (l : Y) (ha : a ≠ 0) (hl : l ≠ 0) :
    Module.finrank K (T.graph ⊓ (T + a.smulRight l).graph :
      Submodule K (X × Y)) + 1 = Module.finrank K X := by
…

def OAI.UniqueGamesTheorem.Inverse.MatrixChart.lowerRows line 111
Source documentation
The lower end of an interval is given by a spanning list of graph vectors.
```
def lowerRows {ι : Type*} (d : ι → X) (s : ι → Y) : Submodule K (X × Y) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.lowerRows_le_graph_iff line 114
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.upperColumns line 124
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.graph_le_upperColumns_iff line 129
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.interval_iff_slice line 148
Source documentation
Exact translation of a Grassmann interval into simultaneous row and column constraints, retaining their inhomogeneous right-hand sides.
```
theorem interval_iff_slice {ι κ : Type*} (d : ι → X) (s : ι → Y)
    (t : κ → X →ₗ[K] K) (q : κ → Y →ₗ[K] K) (T : X →ₗ[K] Y) :
    lowerRows d s ≤ T.graph ∧ T.graph ≤ upperColumns t q ↔
      (∀ i, T (d i) = s i) ∧ (∀ j, (q j).comp T = t j) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.lowerRows, OAI.UniqueGamesTheorem.Inverse.MatrixChart.upperColumns
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixGraph line 171
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.mem_matrixGraph line 175
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixGraph_injective line 181
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional line 188
Source documentation
A coordinate vector as a linear functional, for the standard dot pairing.
```
abbrev dotFunctional (x : ι → K) : (ι → K) →ₗ[K] K := dotProductBilin K K x
```
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional_injective line 190
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional_comp_vecMulLinear line 197
Source documentation
Transposing the chart map sends a column specification to its dot functional.
```
theorem dotFunctional_comp_vecMulLinear (M : Matrix ι κ K) (q : κ → K) :
    (dotFunctional q).comp M.vecMulLinear = dotFunctional (M *ᵥ q) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.column_equation_iff line 204
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrix_interval_iff_slice line 210
Source documentation
Exact concrete row-and-column slice corresponding to an interval.
```
theorem matrix_interval_iff_slice {ρ σ : Type*}
    (d : ρ → ι → K) (s : ρ → κ → K)
    (t : σ → ι → K) (q : σ → κ → K) (M : Matrix ι κ K) :
    lowerRows d s ≤ matrixGraph M ∧
        matrixGraph M ≤ upperColumns (fun j => dotFunctional (t j))
          (fun j => dotFunctional (q j)) ↔
      (∀ i, d i ᵥ* M = s i) ∧ (∀ j, M *ᵥ q j = t j) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.lowerRows, OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixGraph, OAI.UniqueGamesTheorem.Inverse.MatrixChart.upperColumns, OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.finrank_matrixGraph line 222
Source documentation
The graph always has the row dimension, including degenerate zero dimensions.
```
theorem finrank_matrixGraph (M : Matrix ι κ K) :
    Module.finrank K (matrixGraph M) = Fintype.card ι := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixGraph
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.Lines line 245
Source documentation
One-dimensional vector subspaces.
```
abbrev Lines (K E : Type*) [Field K] [AddCommGroup E] [Module K E] :=
…
```
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.Hyperplanes line 249
Source documentation
Hyperplanes, expressed without truncated dimension subtraction.
```
abbrev Hyperplanes (K E : Type*) [Field K] [AddCommGroup E] [Module K E] :=
…
```
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.hyperplanesEquivDualLines line 253
Source documentation
Dual annihilation bijects hyperplanes with lines in the dual space.
```
noncomputable def hyperplanesEquivDualLines [FiniteDimensional K E] :
    Hyperplanes K E ≃ Lines K (Module.Dual K E) where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.Hyperplanes, OAI.UniqueGamesTheorem.Inverse.MatrixChart.Lines
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_lines_binary line 270
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_hyperplanes_binary line 302
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.finrank_map_mkQ_add line 309
Source documentation
A dimension identity for the quotient correspondence, retaining addition.
```
theorem finrank_map_mkQ_add [FiniteDimensional K E]
    (H W : Submodule K E) (hHW : H ≤ W) :
    finrank K (W.map H.mkQ) + finrank K H = finrank K W := by
…
```
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.Extensions line 321
Source documentation
One-dimensional extensions of a subspace.
```
abbrev Extensions (H : Submodule K E) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.extensionsEquivLines line 325
Source documentation
The quotient correspondence identifies extensions with quotient lines.
```
noncomputable def extensionsEquivLines [FiniteDimensional K E]
    (H : Submodule K E) : Extensions H ≃ Lines K (E ⧸ H) where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.Extensions, OAI.UniqueGamesTheorem.Inverse.MatrixChart.Lines
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_extensions_binary line 345
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.HyperplanesBelow line 367
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors line 370
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.hyperplanesBelowEquiv line 374

theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.inf_eq_base_of_distinct_extensions line 390

Source documentation

Distinct one-dimensional extensions intersect in their common base.

theorem inf_eq_base_of_distinct_extensions [FiniteDimensional K E]
    (H L W : Submodule K E) (hHL : H ≤ L) (hHW : H ≤ W)
    (hL : finrank K L = finrank K H + 1)
    (hW : finrank K W = finrank K H + 1) (hWL : W ≠ L) :
    L ⊓ W = H := by
…

abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.NeighborExtensionData line 407
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.neighborsEquivExtensionData line 411
Source documentation
Each neighbor has a unique intersection hyperplane and extension.
```
noncomputable def neighborsEquivExtensionData [FiniteDimensional K E]
    (L : Submodule K E) : GrassmannNeighbors L ≃ NeighborExtensionData L where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.NeighborExtensionData
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_other_extensions_binary line 433
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_grassmann_neighbors_binary line 459
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate line 503
Source documentation
The actual rank-one update of an ordered basis map.
```
def rankOneUpdate (X : E →ₗ[K] F) (a : E →ₗ[K] K) (y : F) : E →ₗ[K] F :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate_apply line 506
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate_mem_range_iff line 511
Source documentation
An outside direction returns to the original image exactly when its coefficient vanishes. This does not require injectivity of X.
```
theorem rankOneUpdate_mem_range_iff (X : E →ₗ[K] F) (a : E →ₗ[K] K)
    {y : F} (hy : y ∉ LinearMap.range X) (x : E) :
    rankOneUpdate X a y x ∈ LinearMap.range X ↔ a x = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injective_rankOneUpdate line 526
Source documentation
Rank-one perturbation in an outside direction preserves independence.
```
theorem injective_rankOneUpdate (X : E →ₗ[K] F) (hX : Function.Injective X)
    (a : E →ₗ[K] K) {y : F} (hy : y ∉ LinearMap.range X) :
    Function.Injective (rankOneUpdate X a y) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.range_inf_rankOneUpdate line 538
Source documentation
Exact intersection, retaining the functional rather than only its rank.
```
theorem range_inf_rankOneUpdate (X : E →ₗ[K] F) (a : E →ₗ[K] K)
    {y : F} (hy : y ∉ LinearMap.range X) :
    LinearMap.range X ⊓ LinearMap.range (rankOneUpdate X a y) =
      (LinearMap.ker a).map X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.comap_range_inf_rankOneUpdate line 555

Source documentation

In the domain coordinates, the intersection recovers the entire kernel.

theorem comap_range_inf_rankOneUpdate (X : E →ₗ[K] F)
    (hX : Function.Injective X) (a : E →ₗ[K] K)
    {y : F} (hy : y ∉ LinearMap.range X) :
    (LinearMap.range X ⊓ LinearMap.range (rankOneUpdate X a y)).comap X =
      LinearMap.ker a := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate

def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdateNeighbor line 565
Source documentation
The updated image is a genuine Grassmann neighbor, with the full ambient neighbor predicate rather than its chart restriction.
```
noncomputable def rankOneUpdateNeighbor [FiniteDimensional K E]
    (X : E →ₗ[K] F) (hX : Function.Injective X)
    (a : E →ₗ[K] K) (ha : a ≠ 0)
    (y : F) (hy : y ∉ LinearMap.range X) :
    MatrixChart.GrassmannNeighbors (LinearMap.range X) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdateNeighbor_val line 579
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.exists_functional_ker_eq line 603
Source documentation
A codimension-one subspace is the kernel of a nonzero functional.
```
theorem exists_functional_ker_eq (H : Submodule K E)
    (hH : finrank K H + 1 = finrank K E) :
    ∃ a : E →ₗ[K] K, a ≠ 0 ∧ LinearMap.ker a = H := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.exists_rankOneUpdate_range_eq line 617
Source documentation
An arbitrary Grassmann neighbor is the range of one of the actual rank-one updates used by the ordered-basis test.
```
theorem exists_rankOneUpdate_range_eq (X : E →ₗ[K] F)
    (hX : Function.Injective X)
    (W : MatrixChart.GrassmannNeighbors (LinearMap.range X)) :
    ∃ (a : E →ₗ[K] K) (y : F), a ≠ 0 ∧ y ∉ LinearMap.range X ∧
      LinearMap.range (rankOneUpdate X a y) = W.val := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdateNeighbor_surjective line 668

Source documentation

Surjectivity includes all neighbors, including those outside any fixed matrix chart.

theorem rankOneUpdateNeighbor_surjective (X : E →ₗ[K] F)
    (hX : Function.Injective X) :
    Function.Surjective (fun p : {a : E →ₗ[K] K // a ≠ 0} ×
      {y : F // y ∉ LinearMap.range X} =>
        rankOneUpdateNeighbor X hX p.1.val p.1.property p.2.val p.2.property) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdateNeighbor

def OAI.UniqueGamesTheorem.Inverse.MatrixChart.coordinateJoin line 692
Source documentation
Concatenate the two coordinate blocks of the chart ambient space.
```
def coordinateJoin (K : Type*) [Field K] (ell m : Nat) :
    ((Fin ell → K) × (Fin m → K)) ≃ₗ[K] (Fin (ell + m) → K) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixVertex line 698
Source documentation
A matrix as an actual Grassmann vertex on ell + m binary coordinates.
```
def matrixVertex {ell m : Nat} (M : Matrix (Fin ell) (Fin m) (ZMod 2)) :
    KMS.Vertex (ell + m) ell :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixVertex_injective line 703
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.finrank_matrixVertex_intersection line 710
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.adjacent_matrixVertex_iff line 725
Source documentation
Exact correspondence with the KMS adjacency predicate, including its explicit inequality requirement.
```
theorem adjacent_matrixVertex_iff {ell m : Nat}
    (M N : Matrix (Fin ell) (Fin m) (ZMod 2)) :
    KMS.Adjacent (matrixVertex M) (matrixVertex N) ↔
      Module.finrank (ZMod 2) (LinearMap.range (M.vecMulLinear - N.vecMulLinear)) = 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Adjacent, OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixVertex
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixChart line 751
Source documentation
The finite matrix chart in the Grassmann vertex type.
```
def matrixChart (ell m : Nat) : Finset (KMS.Vertex (ell + m) ell) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.mem_matrixChart line 755
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_matrixChart line 761