ObstructionDomains.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Domain instances for the canonical obstruction rings

Transparent adapters from the concrete prime-polynomial proofs in DeterminantDomain to the exact rings used by the filtration and bundle modules.

theorem OAI.StableCoordinate.Obstruction.quadricRelation_prime line 18
theorem OAI.StableCoordinate.Obstruction.determinantRelation_prime line 21
instance OAI.StableCoordinate.Obstruction.idealB_isPrime line 24
instance OAI.StableCoordinate.Obstruction.idealC_isPrime line 28
instance OAI.StableCoordinate.Obstruction.B_isDomain line 32
instance OAI.StableCoordinate.Obstruction.C_isDomain line 34
theorem OAI.StableCoordinate.DeterminantRing.relation_prime line 42
instance OAI.StableCoordinate.DeterminantRing.relationIdeal_isPrime line 45
instance OAI.StableCoordinate.DeterminantRing.C_isDomain line 49
theorem OAI.StableCoordinate.Obstruction.cX_ne_zero line 63
Source documentation
Every determinant variable has a nonzero image, witnessed by an explicit matrix of determinant one.
```
theorem cX_ne_zero (i : Fin 5) : cX k i ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.Obstruction.explicit_au_sub_d_ne_zero line 87
Source documentation
The first factor of the auxiliary leading part of v is genuinely nonzero.
```
theorem explicit_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.explicit_au_add_d_ne_zero line 96
Source documentation
The second factor of the auxiliary leading part of v is genuinely nonzero.
```
theorem explicit_au_add_d_ne_zero : cX k 0 * cX k 4 + cX k 1 ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.Obstruction.v_ne_zero line 105
Source documentation
The principal generator of the extended obstruction ideal is nonzero.
```
theorem v_ne_zero : v k ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.v