NineGridDeterminant.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The denominator-cleared matrix has rows and columns indexed by Fin 3 × Fin 3. At the grid (0, 1, -1)², its polynomial evaluation is a Kronecker square with nonzero determinant.

abbrev OAI.EuclideanRamsey.NineGrid.Index line 19
abbrev OAI.EuclideanRamsey.NineGrid.Vars line 20
abbrev OAI.EuclideanRamsey.NineGrid.Poly line 21
def OAI.EuclideanRamsey.NineGrid.q line 24
Source documentation
The denominator-cleared rational parametrization coordinates.
```
def q {R : Type*} [CommRing R] (z : R) : Fin 3 → R :=
…
```
def OAI.EuclideanRamsey.NineGrid.T line 27
def OAI.EuclideanRamsey.NineGrid.U line 28
def OAI.EuclideanRamsey.NineGrid.E line 31
Source documentation
Polynomial evaluation rows before dividing by (1+T²)(1+U²).
```
def E : Matrix Index Index Poly :=
…
```
Mentions: OAI.EuclideanRamsey.NineGrid.Index, OAI.EuclideanRamsey.NineGrid.Poly
def OAI.EuclideanRamsey.NineGrid.grid line 34
def OAI.EuclideanRamsey.NineGrid.gridAssignment line 37
Source documentation
T_(a,b) is sent to grid a, and U_(a,b) to grid b.
```
def gridAssignment : Vars → ℚ
  | Sum.inl i => grid i.1
  | Sum.inr i => grid i.2
```
Mentions: OAI.EuclideanRamsey.NineGrid.Vars, OAI.EuclideanRamsey.NineGrid.grid
def OAI.EuclideanRamsey.NineGrid.gridEval line 41
def OAI.EuclideanRamsey.NineGrid.C line 44
Source documentation
The evaluated one-parameter matrix C'.
```
def C : Matrix (Fin 3) (Fin 3) ℚ := fun i j => q (grid i) j
```
Mentions: OAI.EuclideanRamsey.NineGrid.q, OAI.EuclideanRamsey.NineGrid.grid
lemma OAI.EuclideanRamsey.NineGrid.map_q line 46
lemma OAI.EuclideanRamsey.NineGrid.gridEval_T line 51
lemma OAI.EuclideanRamsey.NineGrid.gridEval_U line 54
lemma OAI.EuclideanRamsey.NineGrid.C_eq line 58
Source documentation
Exact rational entries, with rows indexed in the order 0,1,2.
```
lemma C_eq : C = ![![1, 1, 0], ![2, 0, 2], ![2, 0, -2]] := by
…
```
Mentions: OAI.EuclideanRamsey.NineGrid.C
lemma OAI.EuclideanRamsey.NineGrid.det_C line 62
lemma OAI.EuclideanRamsey.NineGrid.evaluated_E line 67
Source documentation
The evaluation is on the polynomial ring alone.
```
lemma evaluated_E : gridEval.mapMatrix E = C ⊗ₖ C := by
…
```
Mentions: OAI.EuclideanRamsey.NineGrid.E, OAI.EuclideanRamsey.NineGrid.C
lemma OAI.EuclideanRamsey.NineGrid.det_evaluated_E line 75
lemma OAI.EuclideanRamsey.NineGrid.gridEval_det_E line 79
theorem OAI.EuclideanRamsey.NineGrid.det_E_ne_zero line 84
Source documentation
The full denominator-cleared nine-row polynomial determinant is nonzero.
```
theorem det_E_ne_zero : Matrix.det E ≠ 0 := by
…
```
Mentions: OAI.EuclideanRamsey.NineGrid.E