DeterminantNonzero.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Concrete nonvanishing certificates in the determinant quotient

These elementary evaluations verify the nonzero factors used to split the highest auxiliary part of v, without assuming the unproved headline.

def OAI.StableCoordinate.Obstruction.determinantEval line 21
Source documentation
Evaluate the determinant quotient at any point satisfying its defining relation.
```
def determinantEval (point : Fin 5 → k)
    (hp : point 0 * point 3 - point 2 * point 1 - 1 = 0) : C k →ₐ[k] k :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.Obstruction.determinantEval_cX line 33
def OAI.StableCoordinate.Obstruction.highTestPoint line 40
Source documentation
A specific point where the top auxiliary part and both of its factors are one.
```
def highTestPoint : Fin 5 → k := ![1, 0, 0, 1, 1]
```
theorem OAI.StableCoordinate.Obstruction.highTestPoint_relation line 43
Source documentation
The test point does lie on the determinant hypersurface.
```
theorem highTestPoint_relation :
    highTestPoint k 0 * highTestPoint k 3 - highTestPoint k 2 * highTestPoint k 1 - 1 = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.highTestPoint
def OAI.StableCoordinate.Obstruction.highTestEval line 48
Source documentation
The associated evaluation is an actual algebra homomorphism.
```
def highTestEval : C k →ₐ[k] k := determinantEval k (highTestPoint k) (highTestPoint_relation k)
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.determinantEval, OAI.StableCoordinate.Obstruction.highTestPoint, OAI.StableCoordinate.Obstruction.highTestPoint_relation
theorem OAI.StableCoordinate.Obstruction.highTestEval_cX line 50
theorem OAI.StableCoordinate.Obstruction.highTestEval_vHigh line 53
theorem OAI.StableCoordinate.Obstruction.highTestEval_au_sub_d line 56
theorem OAI.StableCoordinate.Obstruction.highTestEval_au_add_d line 60
theorem OAI.StableCoordinate.Obstruction.adjoin_range_cX line 65
Source documentation
The finite list of displayed generators really generates the actual quotient algebra.
```
theorem adjoin_range_cX : Algebra.adjoin k (Set.range (cX k)) = ⊤ := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.Obstruction.vHigh_ne_zero line 76
Source documentation
The source's highest auxiliary part is genuinely nonzero.
```
theorem vHigh_ne_zero : vHigh k ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.vHigh
theorem OAI.StableCoordinate.Obstruction.au_sub_d_ne_zero line 82
Source documentation
Both difference-of-squares factors are nonzero in the actual quotient.
```
theorem au_sub_d_ne_zero : cX k 0 * cX k 4 - cX k 1 ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.Obstruction.au_add_d_ne_zero line 87
theorem OAI.StableCoordinate.Obstruction.cX_a_ne_zero line 92
theorem OAI.StableCoordinate.Obstruction.cX_u_ne_zero line 97
theorem OAI.StableCoordinate.Obstruction.vLow_ne_zero line 103
Source documentation
The lower auxiliary term is also genuinely nonzero.
```
theorem vLow_ne_zero : vLow k ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.vLow
theorem OAI.StableCoordinate.Obstruction.cX_d_ne_zero line 112
Source documentation
The second weight-one coordinate is nonzero as well.
```
theorem cX_d_ne_zero : cX k 1 ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.Obstruction.auxiliary_proj_v_two_ne_zero line 120
Source documentation
Thus the auxiliary degree-two projection of v is nonzero.
```
theorem auxiliary_proj_v_two_ne_zero : GradedAlgebra.proj (auxiliaryPiece k) 2 (v k) ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.auxiliaryPiece, OAI.StableCoordinate.Obstruction.v