KMSDimensionOne.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A proved one-dimensional Grassmann expansion case

Distinct lines always intersect trivially, so this Grassmann graph is complete. Its retention never exceeds global density. This proves a genuine restricted expansion statement; it does not imply the OPEN large-dimension KMS principle.

theorem OAI.UniqueGamesTheorem.Inverse.KMS.adjacent_one_iff line 22
theorem OAI.UniqueGamesTheorem.Inverse.KMS.neighbors_one_eq line 39
theorem OAI.UniqueGamesTheorem.Inverse.KMS.inter_univ_erase line 44
theorem OAI.UniqueGamesTheorem.Inverse.KMS.dimensionOne_neighbor_density line 49
theorem OAI.UniqueGamesTheorem.Inverse.KMS.dimensionOne_retention line 62
Source documentation
Exact retention of a nonempty collection of binary lines.
```
theorem dimensionOne_retention {n : ℕ} (S : Finset (Vertex n 1))
    (hS : S.Nonempty) :
    retention S = ((S.card : ℝ) - 1) /
      ((Fintype.card (Vertex n 1) : ℝ) - 1) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.retention
theorem OAI.UniqueGamesTheorem.Inverse.KMS.dimensionOne_retention_le_density line 80
Source documentation
The one-dimensional Grassmann graph has retention at most global density. The cardinality hypothesis rules out the single-vertex, zero-degree case.
```
theorem dimensionOne_retention_le_density {n : ℕ} (S : Finset (Vertex n 1))
    (hS : S.Nonempty) (hV : 1 < Fintype.card (Vertex n 1)) :
    retention S ≤ relativeDensity S Finset.univ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.retention, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity
theorem OAI.UniqueGamesTheorem.Inverse.KMS.dimensionOne_dense_interval line 93
Source documentation
In dimension one, the whole ambient interval already has the required density. This is a proved special case, not a premise for higher dimensions.
```
theorem dimensionOne_dense_interval {n : ℕ} (S : Finset (Vertex n 1))
    (hS : S.Nonempty) (hV : 1 < Fintype.card (Vertex n 1))
    {ζ : ℝ} (hζ : ζ ≤ retention S) :
    ζ ≤ relativeDensity S (interval (⊥ : Submodule F2 (Ambient n)) ⊤) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.retention, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.interval, OAI.UniqueGamesTheorem.Inverse.KMS.F2, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient