MatrixChartDegreeNeighbors.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

The full Grassmann degree, by choosing the intersection hyperplane and a different one-dimensional extension. No graph regularity is assumed.

abbrev OAI.MaxCutGames.Inverse.MatrixChart.HyperplanesBelow line 17
abbrev OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors line 20
def OAI.MaxCutGames.Inverse.MatrixChart.hyperplanesBelowEquiv line 24

theorem OAI.MaxCutGames.Inverse.MatrixChart.inf_eq_base_of_distinct_extensions line 40

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.MaxCutGames.Inverse.MatrixChart.NeighborExtensionData line 57
def OAI.MaxCutGames.Inverse.MatrixChart.neighborsEquivExtensionData line 61
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.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors, OAI.MaxCutGames.Inverse.MatrixChart.NeighborExtensionData
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_other_extensions_binary line 83
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_grassmann_neighbors_binary line 109
def OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate line 149
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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate_apply line 152
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate_mem_range_iff line 157
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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.injective_rankOneUpdate line 172
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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.range_inf_rankOneUpdate line 184
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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.comap_range_inf_rankOneUpdate line 201

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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate

def OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor line 211
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.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor_val line 225
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.exists_functional_ker_eq line 245
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.MaxCutGames.Inverse.KMSBasisComparison.exists_rankOneUpdate_range_eq line 259
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.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor_surjective line 310

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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor

def OAI.MaxCutGames.Inverse.MatrixChart.graphEquiv line 327
Source documentation
The first coordinate identifies the graph with its domain.
```
def graphEquiv (T : X →ₗ[K] Y) : X ≃ₗ[K] T.graph where
…
```
theorem OAI.MaxCutGames.Inverse.MatrixChart.graph_injective line 341
theorem OAI.MaxCutGames.Inverse.MatrixChart.exists_unique_graph_iff line 350
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.MaxCutGames.Inverse.MatrixChart.intersectionEquiv line 363
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.MaxCutGames.Inverse.MatrixChart.finrank_graph line 383

theorem OAI.MaxCutGames.Inverse.MatrixChart.finrank_intersection_add_rank line 388

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.MaxCutGames.Inverse.MatrixChart.adjacent_iff_rank_one line 395

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.MaxCutGames.Inverse.MatrixChart.adjacent_rank_one_step line 403

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.MaxCutGames.Inverse.MatrixChart.lowerRows line 416
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.MaxCutGames.Inverse.MatrixChart.lowerRows_le_graph_iff line 419
def OAI.MaxCutGames.Inverse.MatrixChart.upperColumns line 429
theorem OAI.MaxCutGames.Inverse.MatrixChart.graph_le_upperColumns_iff line 434
theorem OAI.MaxCutGames.Inverse.MatrixChart.interval_iff_slice line 453
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.MaxCutGames.Inverse.MatrixChart.lowerRows, OAI.MaxCutGames.Inverse.MatrixChart.upperColumns
theorem OAI.MaxCutGames.Inverse.MatrixChart.exists_smulRight_of_rank_one line 477
Source documentation
Every map with one-dimensional range is a nonzero functional times a nonzero vector. This existence statement is valid over any field.
```
theorem exists_smulRight_of_rank_one (T : X →ₗ[K] Y)
    (hT : Module.finrank K T.range = 1) :
    ∃ (a : X →ₗ[K] K) (l : Y), a ≠ 0 ∧ l ≠ 0 ∧ T = a.smulRight l := by
…
```

theorem OAI.MaxCutGames.Inverse.MatrixChart.rank_one_iff_exists_smulRight line 502

Source documentation

The exact algebraic characterization of nonzero rank-one maps.

theorem rank_one_iff_exists_smulRight (T : X →ₗ[K] Y) :
    Module.finrank K T.range = 1 ↔
      ∃ (a : X →ₗ[K] K) (l : Y), a ≠ 0 ∧ l ≠ 0 ∧ T = a.smulRight l := by
…

theorem OAI.MaxCutGames.Inverse.MatrixChart.binary_smulRight_unique line 518

Source documentation

Over the two-element field there is no nontrivial rescaling ambiguity.

theorem binary_smulRight_unique
    {a b : X →ₗ[ZMod 2] ZMod 2} {l k : Y}
    (ha : a ≠ 0) (hl : l ≠ 0)
    (h : a.smulRight l = b.smulRight k) : a = b ∧ l = k := by
…

abbrev OAI.MaxCutGames.Inverse.MatrixChart.BinaryRankOneFactors line 539
Source documentation
Ordered nonzero factors, with functional coordinate first.
```
abbrev BinaryRankOneFactors (X Y : Type*)
    [AddCommGroup X] [Module (ZMod 2) X]
    [AddCommGroup Y] [Module (ZMod 2) Y] :=
…
```
abbrev OAI.MaxCutGames.Inverse.MatrixChart.BinaryRankOneMaps line 545
Source documentation
The actual linear maps whose range has dimension one.
```
abbrev BinaryRankOneMaps (X Y : Type*)
    [AddCommGroup X] [Module (ZMod 2) X]
    [AddCommGroup Y] [Module (ZMod 2) Y] :=
…
```
def OAI.MaxCutGames.Inverse.MatrixChart.binaryRankOneMap line 550
theorem OAI.MaxCutGames.Inverse.MatrixChart.binary_smulRight_injective line 555
theorem OAI.MaxCutGames.Inverse.MatrixChart.binary_smulRight_surjective line 562
def OAI.MaxCutGames.Inverse.MatrixChart.binaryRankOneEquiv line 570
Source documentation
Bijection justifying uniform rank-one sampling by independent uniform nonzero factors. The inverse uses choice only to select the proved unique pair.
```
noncomputable def binaryRankOneEquiv :
    BinaryRankOneFactors X Y ≃ BinaryRankOneMaps X Y :=
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.BinaryRankOneFactors, OAI.MaxCutGames.Inverse.MatrixChart.BinaryRankOneMaps
theorem OAI.MaxCutGames.Inverse.MatrixChart.binaryRankOneEquiv_apply line 575
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_binaryRankOneMaps line 580
Source documentation
The number of binary rank-one maps is exactly the product of the two nonzero-factor counts, including the zero-dimensional edge cases.
```
theorem card_binaryRankOneMaps [Fintype (X →ₗ[ZMod 2] ZMod 2)] [Fintype Y] :
    Nat.card (BinaryRankOneMaps X Y) =
      (Fintype.card (X →ₗ[ZMod 2] ZMod 2) - 1) * (Fintype.card Y - 1) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.BinaryRankOneMaps

theorem OAI.MaxCutGames.Inverse.MatrixChart.card_binaryRankOneMaps_pow line 592

Source documentation

Dimensional form of the exact rank-one count.

theorem card_binaryRankOneMaps_pow [Fintype (X →ₗ[ZMod 2] ZMod 2)] [Fintype Y] :
    Nat.card (BinaryRankOneMaps X Y) =
      (2 ^ Module.finrank (ZMod 2) X - 1) *
        (2 ^ Module.finrank (ZMod 2) Y - 1) := by
…

Mentions: OAI.MaxCutGames.Inverse.MatrixChart.BinaryRankOneMaps

theorem OAI.MaxCutGames.Inverse.MatrixChart.card_binaryRankOneMaps_coordinates line 604
abbrev OAI.MaxCutGames.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber line 630
Source documentation
Vectors external to the starting image which give the same updated image.
```
abbrev FixedFunctionalNeighborFiber (X : E →ₗ[ZMod 2] F)
    (a : E →ₗ[ZMod 2] ZMod 2) (y₀ : F) :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.add_image_not_mem_range line 635

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.range_update_add_kernel line 641

Source documentation

Kernel translations of the perturbation vector preserve its image.

theorem range_update_add_kernel (X : E →ₗ[ZMod 2] F)
    (a : E →ₗ[ZMod 2] ZMod 2) (y : F) (z : a.ker) :
    (X + a.smulRight (y + X z)).range = (X + a.smulRight y).range := by
…

def OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap line 660
Source documentation
The affine parametrization of a fixed-functional image fiber.
```
def fixedFunctionalFiberMap (X : E →ₗ[ZMod 2] F)
    (a : E →ₗ[ZMod 2] ZMod 2) {y₀ : F} (hy₀ : y₀ ∉ X.range) :
    a.ker → FixedFunctionalNeighborFiber X a y₀ :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap_injective line 666
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap_surjective line 675
def OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalNeighborFiberEquiv line 705
Source documentation
Exact constant-multiplicity fiber over an updated subspace.
```
def fixedFunctionalNeighborFiberEquiv (X : E →ₗ[ZMod 2] F)
    (hX : Function.Injective X) (a : E →ₗ[ZMod 2] ZMod 2)
    (ha : a ≠ 0) {y₀ : F} (hy₀ : y₀ ∉ X.range) :
    a.ker ≃ FixedFunctionalNeighborFiber X a y₀ :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_fixedFunctionalNeighborFiber line 713
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_fixedFunctionalNeighborFiber_pow line 719