Definitions.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The four-variable complex polynomial

Variables are zero-indexed internally: X 0, X 1, X 2, X 3 mean the paper's x₁, x₂, x₃, x₄. The stabilization uses Fin.castSucc, so its fifth independent variable is X 4; no subring-preservation condition is imposed on its automorphism.

Affine fibers are encoded by their complex coordinate algebras, not by sets. An algebra equivalence to the three-variable polynomial algebra is precisely the algebraic affine-space conclusion. Rectifiability is encoded by the ambient algebra automorphism carrying the defining ideal to (X 0).

abbrev OAI.StableCoordinate.R line 26
Also declared: ComparatorChallenges/StableCoordinateFour.lean:9 (same declaration text).
def OAI.StableCoordinate.Q line 28
Also declared: ComparatorChallenges/StableCoordinateFour.lean:11 (same declaration text).
def OAI.StableCoordinate.f line 31
Also declared: ComparatorChallenges/StableCoordinateFour.lean:14 (same declaration text).
def OAI.StableCoordinate.IsCoordinate line 35
Source documentation
A coordinate is sent to the first variable by some complex algebra automorphism.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:17 (same declaration text).
```
def IsCoordinate {n : ℕ} (hn : 0 < n) (g : R n) : Prop :=
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.stabilize line 39
Source documentation
Adjoin one independent variable; the original variables retain their indices.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:20 (same declaration text).
```
noncomputable def stabilize : R 4 →ₐ[ℂ] R 5 :=
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.IsOneStableCoordinate line 43
Source documentation
No requirement to preserve the original four-variable subring is imposed.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:23 (same declaration text).
```
def IsOneStableCoordinate (g : R 4) : Prop :=
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.fiberIdeal line 46
Also declared: ComparatorChallenges/StableCoordinateFour.lean:26 (same declaration text).
abbrev OAI.StableCoordinate.FiberRing line 49
Also declared: ComparatorChallenges/StableCoordinateFour.lean:29 (same declaration text).
def OAI.StableCoordinate.IsAffineThreeSpaceFiber line 52
Source documentation
An isomorphism of affine coordinate algebras, not a set-theoretic bijection.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:31 (same declaration text).
```
def IsAffineThreeSpaceFiber (t : ℂ) : Prop :=
…
```
def OAI.StableCoordinate.IsRectifiableFiber line 56
Source documentation
Algebraic rectifiability of the closed hypersurface embedding.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:34 (same declaration text).
```
def IsRectifiableFiber (t : ℂ) : Prop :=
…
```
def OAI.StableCoordinate.PolynomialPackage line 61
Source documentation
Complete first principal group, with the advertised exact total degree.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:38 (same declaration text).
```
def PolynomialPackage : Prop :=
…
```
def OAI.StableCoordinate.FiberPackage line 67
Source documentation
Complete second principal group, universally including the zero fiber.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:43 (same declaration text).
```
def FiberPackage : Prop :=
…
```
def OAI.StableCoordinate.PrincipalPackage line 71
Source documentation
Both principal groups must be proved together, without additional hypotheses.
Also declared: ComparatorChallenges/StableCoordinateFour.lean:46 (same declaration text).
```
def PrincipalPackage : Prop := PolynomialPackage ∧ FiberPackage
…
```
Mentions: OAI.StableCoordinate.PolynomialPackage, OAI.StableCoordinate.FiberPackage