FiniteFieldRows.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The finite-field graph matrix

The rows are literal symmetric forms, the labels are their actual contractions, and every admissible set is included as a column index. The only input to the separation theorem is the repeated-tuple nonvanishing conclusion constructed by the robust-directions argument; graph separation is proved from it.

def OAI.MetricEntropyDuality.FiniteFieldRows.admissibleSets line 21
Source documentation
All admissible subsets are fixed before a pair of rows is chosen.
```
def admissibleSets (θ : ℝ) (u : ℕ) : Finset (Finset (Fin u)) := by
…
```
theorem OAI.MetricEntropyDuality.FiniteFieldRows.mem_admissibleSets line 25
theorem OAI.MetricEntropyDuality.FiniteFieldRows.full_mem_admissibleSets line 30
theorem OAI.MetricEntropyDuality.FiniteFieldRows.admissibleSets_nonempty line 36
abbrev OAI.MetricEntropyDuality.FiniteFieldRows.RowIndex line 39
abbrev OAI.MetricEntropyDuality.FiniteFieldRows.ColumnIndex line 41
abbrev OAI.MetricEntropyDuality.FiniteFieldRows.labels line 45
Source documentation
The literal contraction partition maps on forms of positive degree.
```
abbrev labels {p r j u : ℕ} (t : Fin u → (Fin r → ZMod p)) :=
…
```
def OAI.MetricEntropyDuality.FiniteFieldRows.column line 49
Source documentation
The actual matrix, in the column-first convention of compression.
```
def column {p r j u : ℕ} (θ : ℝ) (t : Fin u → (Fin r → ZMod p)) :
    ColumnIndex θ p r (j + 1) u → RowIndex p r (j + 1) → ℝ :=
…
```
Mentions: OAI.MetricEntropyDuality.FiniteFieldRows.ColumnIndex, OAI.MetricEntropyDuality.FiniteFieldRows.RowIndex
def OAI.MetricEntropyDuality.FiniteFieldRows.row line 53
theorem OAI.MetricEntropyDuality.FiniteFieldRows.card_rowIndex line 57
theorem OAI.MetricEntropyDuality.FiniteFieldRows.card_label_image_le line 63
Source documentation
The label range is counted in the actual space of lower-degree forms; surjectivity of contraction is not needed.
```
theorem card_label_image_le {p r j u : ℕ} [NeZero p]
    (t : Fin u → (Fin r → ZMod p)) (i : Fin u) :
    (Finset.univ.image (labels (j := j) t i)).card ≤ p ^ formDimension r j := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteFieldRows.labels, OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.FiniteFieldRows.card_rowIndex_le_columns line 72
Source documentation
Including the full index set gives at least one column per row.
```
theorem card_rowIndex_le_columns {θ : ℝ} (hθ : 0 ≤ θ)
    (p r h u : ℕ) [NeZero p] :
    Fintype.card (RowIndex p r h) ≤ Fintype.card (ColumnIndex θ p r h u) := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteFieldRows.RowIndex, OAI.MetricEntropyDuality.FiniteFieldRows.ColumnIndex
theorem OAI.MetricEntropyDuality.FiniteFieldRows.columnIndex_nonempty line 81
theorem OAI.MetricEntropyDuality.FiniteFieldRows.graph_separation line 98
Source documentation
Robust nonvanishing gives separation in one of the actual admissible graphs.
```
theorem graph_separation (x y : RowIndex p r (j + 1)) (hxy : x ≠ y) :
    ∃ T ∈ admissibleSets θ u,
      ((j + 1 : ℕ) : ℕ∞) < PartitionGraph.distance (labels t) T x y := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteFieldRows.RowIndex, OAI.MetricEntropyDuality.FiniteFieldRows.admissibleSets, OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.FiniteFieldRows.labels
theorem OAI.MetricEntropyDuality.FiniteFieldRows.exists_column_abs_eq_one line 107
Source documentation
This coordinate statement is the direct input to the convex-body argument.
```
theorem exists_column_abs_eq_one (x y : RowIndex p r (j + 1)) (hxy : x ≠ y) :
    ∃ c : ColumnIndex θ p r (j + 1) u,
      |column θ t c x - column θ t c y| = 1 :=
…
```
Mentions: OAI.MetricEntropyDuality.FiniteFieldRows.RowIndex, OAI.MetricEntropyDuality.FiniteFieldRows.ColumnIndex, OAI.MetricEntropyDuality.FiniteFieldRows.column
theorem OAI.MetricEntropyDuality.FiniteFieldRows.norm_row_sub_eq_one line 114
Source documentation
The full row distance is exactly one.
```
theorem norm_row_sub_eq_one (x y : RowIndex p r (j + 1)) (hxy : x ≠ y) :
    ‖row θ t x - row θ t y‖ = 1 :=
…
```
Mentions: OAI.MetricEntropyDuality.FiniteFieldRows.RowIndex, OAI.MetricEntropyDuality.FiniteFieldRows.row