SquareLinear.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Linear algebra, dimensions, and arithmetic of square configurations

theorem OAI.Nagata.Workers.W24.ambientDegreeK_dimension_lt line 28
Source documentation
The ambient ternary degree-k form dimension is less than k² for k≥4.
```
theorem ambientDegreeK_dimension_lt (k : ℕ) (hk : 4 ≤ k) :
    (k + 2).choose 2 < k * k := by
…
```

theorem OAI.Nagata.Workers.W24.nonzero_smul_outside_range line 50

Source documentation

Nonzero scalar multiplication preserves being outside a linear image.

theorem nonzero_smul_outside_range {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    (f : V →ₗ[K] W) (c : W) (hc : c ∉ f.range) (a : K) (ha : a ≠ 0) :
    a • c ∉ f.range := by
…

theorem OAI.Nagata.Workers.W24.evaluation_coefficient_contradiction line 59

Source documentation

This is the final evaluation-map contradiction once the coefficient identity and a nonzero scalar have been supplied by the geometric construction.

theorem evaluation_coefficient_contradiction {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    (f : V →ₗ[K] W) (c : W) (hc : c ∉ f.range) (a : K) (ha : a ≠ 0)
    (s : V) (heq : f s = a • c) : False := by
…

def OAI.Nagata.Workers.W24.normalResiduePolynomial line 79
Source documentation
Polynomial of residue classes along the principal equation G.
```
def normalResiduePolynomial {A : Type*} [CommRing A] (G : A) (F : A[X]) :
    Polynomial (A ⧸ Ideal.span ({G} : Set A)) :=
…
```
theorem OAI.Nagata.Workers.W24.above_normalResidue_degree_dvd line 85
Source documentation
Above the genuine quotient-polynomial degree, every lift coefficient is G-divisible and therefore restricts to zero on every component.
```
theorem above_normalResidue_degree_dvd {A : Type*} [CommRing A]
    (G : A) (F : A[X]) (j : ℕ) (hj : (normalResiduePolynomial G F).natDegree < j) :
    G ∣ F.coeff j := by
…
```
Mentions: OAI.Nagata.Workers.W24.normalResiduePolynomial

theorem OAI.Nagata.Workers.W24.top_normalResidue_coefficient_not_dvd line 93

Source documentation

The highest genuine residue coefficient is not G-divisible.

theorem top_normalResidue_coefficient_not_dvd {A : Type*} [CommRing A]
    (G : A) (F : A[X]) (hne : normalResiduePolynomial G F ≠ 0) :
    ¬ G ∣ F.coeff (normalResiduePolynomial G F).natDegree := by
…

Mentions: OAI.Nagata.Workers.W24.normalResiduePolynomial

theorem OAI.Nagata.Workers.W24.restriction_natDegree_le_normalResidue_degree line 104
Source documentation
Any ring restriction killing G has degree bounded by the top residue index.
```
theorem restriction_natDegree_le_normalResidue_degree {A B : Type*}
    [CommRing A] [CommRing B] (G : A) (F : A[X]) (f : A →+* B) (hG : f G = 0) :
    (F.map f).natDegree ≤ (normalResiduePolynomial G F).natDegree := by
…
```
Mentions: OAI.Nagata.Workers.W24.normalResiduePolynomial
theorem OAI.Nagata.Workers.W24.leadingCoefficient_degree_le line 122
Source documentation
The degree comparison for the leading coefficient of a normal polynomial.
```
theorem leadingCoefficient_degree_le (k d m j : Nat) (hd : d ≤ k * m) :
    k * (d - k * j) ≤ k * k * (m - j) := by
…
```
theorem OAI.Nagata.Workers.W24.leadingCoefficient_degree_lt line 128
Source documentation
Strict degree deficit excludes the prescribed number of zeros, numerically.
```
theorem leadingCoefficient_degree_lt (k d m j : Nat) (hk : 0 < k)
    (hd : d < k * m) (hdj : k * j ≤ d) :
    k * (d - k * j) < k * k * (m - j) := by
…
```

theorem OAI.Nagata.Workers.W24.leadingCoefficient_equality_forces_slope line 136

Source documentation

Equality of the two degree bounds forces equality in the original slope.

theorem leadingCoefficient_equality_forces_slope (k d m j : Nat)
    (hk : 0 < k) (hd : d ≤ k * m) (hdj : k * j ≤ d)
    (heq : k * (d - k * j) = k * k * (m - j)) : d = k * m := by
…

theorem OAI.Nagata.Workers.W24.leadingIndex_le_m line 146
Source documentation
The index bound used before splitting the square-case argument.
```
theorem leadingIndex_le_m (k d m j : Nat) (hk : 0 < k)
    (hdj : k * j ≤ d) (hd : d ≤ k * m) : j ≤ m := by
…
```
theorem OAI.Nagata.Workers.W24.lastIndex_exponent_zero line 154
Source documentation
At the last possible index, the coefficient exponent is zero.
```
theorem lastIndex_exponent_zero (k d m : Nat)
    (hmd : k * m ≤ d) (hdm : d ≤ k * m) : d = k * m ∧ d - k * m = 0 := by
…
```
theorem OAI.Nagata.Workers.W24.penultimate_exponent line 159
Source documentation
The previous coefficient then has the normal bundle's exponent.
```
theorem penultimate_exponent (k m : Nat) (hm : 0 < m) :
    k * m - k * (m - 1) = k := by
…
```
theorem OAI.Nagata.Workers.W24.lowerIndex_positive_power line 167
Source documentation
A positive power is obtained in the lower-index branch.
```
theorem lowerIndex_positive_power (m j : Nat) (hj : j < m) : 0 < m - j := by
…
```
theorem OAI.Nagata.Workers.W24.twice_sectionDimension_lt line 171
Source documentation
Twice the section-space dimension is strictly less than twice k².
```
theorem twice_sectionDimension_lt (k : Nat) (hk : 4 ≤ k) :
    k * k + 3 * k < 2 * (k * k) := by
…
```
theorem OAI.Nagata.Workers.W24.sectionDimension_lt line 179
Source documentation
Integer form of (k²+3k)/2 < k² for the square case.
```
theorem sectionDimension_lt (k : Nat) (hk : 4 ≤ k) :
    (k * k + 3 * k) / 2 < k * k := by
…
```
theorem OAI.Nagata.Workers.W24.genusFormula_pos line 185
Source documentation
Positivity of the plane-curve genus formula in the square range.
```
theorem genusFormula_pos (k : Nat) (hk : 4 ≤ k) :
    0 < ((k - 1) * (k - 2)) / 2 := by
…
```

theorem OAI.Nagata.Workers.W24.polynomial_eq_leadingCoeff_mul_power line 204

Source documentation

A degree-at-most-m polynomial divisible by (X-c)^m has the required shape.

theorem polynomial_eq_leadingCoeff_mul_power {R : Type*} [CommRing R] [Nontrivial R]
    (p : R[X]) (c : R) (m : Nat) (hd : p.natDegree ≤ m)
    (hmult : (X - C c) ^ m ∣ p) :
    p = C p.leadingCoeff * (X - C c) ^ m := by
…

theorem OAI.Nagata.Workers.W24.power_penultimate_coefficient line 213

Source documentation

The coefficient of X^(m-1) in the translated monic power.

theorem power_penultimate_coefficient {R : Type*} [CommRing R] [Nontrivial R]
    (c : R) (m : Nat) (hm : 0 < m) :
    ((X - C c) ^ m).coeff (m - 1) = -((m : R) * c) := by
…

theorem OAI.Nagata.Workers.W24.polynomial_penultimate_coefficient line 224

Source documentation

Coefficient comparison for the actual polynomial, retaining its leading scalar.

theorem polynomial_penultimate_coefficient {R : Type*} [CommRing R] [Nontrivial R]
    (p : R[X]) (c : R) (m : Nat) (hm : 0 < m) (hd : p.natDegree ≤ m)
    (hmult : (X - C c) ^ m ∣ p) :
    p.coeff (m - 1) = p.leadingCoeff * (-((m : R) * c)) := by
…

theorem OAI.Nagata.Workers.W24.polynomial_penultimate_coefficient_scalar line 233

Source documentation

The source manuscript's scalar-times-fiber-vector coefficient form.

theorem polynomial_penultimate_coefficient_scalar {R : Type*} [CommRing R] [Nontrivial R]
    (p : R[X]) (c : R) (m : Nat) (hm : 0 < m) (hd : p.natDegree ≤ m)
    (hmult : (X - C c) ^ m ∣ p) :
    p.coeff (m - 1) = (-(m : R) * p.leadingCoeff) * c := by
…

theorem OAI.Nagata.Workers.W24.coefficient_scalar_ne_zero line 242

Source documentation

The multiplying scalar in characteristic zero is nonzero.

theorem coefficient_scalar_ne_zero {K : Type*} [Field K] [CharZero K]
    (p : K[X]) (hp : p ≠ 0) (m : Nat) (hm : 0 < m) :
    -(m : K) * p.leadingCoeff ≠ 0 := by
…

theorem OAI.Nagata.Workers.W24.rootMultiplicity_penultimate_coefficient line 249

Source documentation

The same coefficient identity from mathlib's genuine root multiplicity.

theorem rootMultiplicity_penultimate_coefficient {R : Type*} [CommRing R]
    [Nontrivial R] (p : R[X]) (hp : p ≠ 0) (c : R) (m : Nat) (hm : 0 < m)
    (hd : p.natDegree ≤ m) (hmult : m ≤ p.rootMultiplicity c) :
    p.coeff (m - 1) = (-(m : R) * p.leadingCoeff) * c := by
…

abbrev OAI.Nagata.Workers.W24.ConePoint line 274
Source documentation
Nonzero homogeneous coordinate vectors on the actual equation G=0.
```
abbrev ConePoint (G : MvPolynomial (Fin 3) ℂ) :=
…
```
abbrev OAI.Nagata.Workers.W24.PlaneForms line 278
Source documentation
The ordinary vector space of homogeneous plane forms of degree n.
```
abbrev PlaneForms (n : Nat) := MvPolynomial.homogeneousSubmodule (Fin 3) ℂ n
```
def OAI.Nagata.Workers.W24.homogeneousEvaluation line 281
Source documentation
Simultaneous evaluation of actual homogeneous forms at chosen coordinates.
```
def homogeneousEvaluation {ι : Type*} (n : Nat) (a : ι → Fin 3 → ℂ) :
    PlaneForms n →ₗ[ℂ] (ι → ℂ) :=
…
```
Mentions: OAI.Nagata.Workers.W24.PlaneForms
theorem OAI.Nagata.Workers.W24.homogeneousEvaluation_apply line 286
def OAI.Nagata.Workers.W24.restrictedPolynomialFunctions line 292
Source documentation
Restricted polynomial functions on the punctured affine cone of G. The source construction lands in this genuine image submodule.
```
def restrictedPolynomialFunctions (G : MvPolynomial (Fin 3) ℂ) (n : Nat) :
    Submodule ℂ (ConePoint G → ℂ) :=
…
```
Mentions: OAI.Nagata.Workers.W24.ConePoint

theorem OAI.Nagata.Workers.W24.homogeneousEvaluation_scale line 297

Source documentation

Every actual homogeneous lift has the standard degree-n scaling law.

theorem homogeneousEvaluation_scale {ι : Type*} (n : Nat)
    (a : ι → Fin 3 → ℂ) (u : ι → ℂ) (F : PlaneForms n) (i : ι) :
    homogeneousEvaluation n (fun i j => u i * a i j) F i =
      (u i) ^ n * homogeneousEvaluation n a F i := by
…

Mentions: OAI.Nagata.Workers.W24.PlaneForms, OAI.Nagata.Workers.W24.homogeneousEvaluation

def OAI.Nagata.Workers.W24.equationForm line 304
Source documentation
The curve equation itself is an element of its degree's homogeneous space.
```
def equationForm {k : Nat} (G : Nagata.W16.NonzeroHomogeneousForm k) : PlaneForms k :=
…
```
Mentions: OAI.Nagata.Workers.W24.PlaneForms
theorem OAI.Nagata.Workers.W24.equationForm_ne_zero line 308
Source documentation
A nonzero curve equation supplies a genuinely nonzero kernel vector.
```
theorem equationForm_ne_zero {k : Nat} (G : Nagata.W16.NonzeroHomogeneousForm k) :
    equationForm G ≠ 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.equationForm
theorem OAI.Nagata.Workers.W24.equationForm_in_evaluation_kernel line 314
Source documentation
Evaluation of the equation is zero at every selected point on its cone.
```
theorem equationForm_in_evaluation_kernel {ι : Type*} {k : Nat}
    (G : Nagata.W16.NonzeroHomogeneousForm k) (a : ι → ConePoint G.polynomial) :
    equationForm G ∈ (homogeneousEvaluation k (fun i => (a i).val)).ker := by
…
```
Mentions: OAI.Nagata.Workers.W24.ConePoint, OAI.Nagata.Workers.W24.equationForm, OAI.Nagata.Workers.W24.homogeneousEvaluation
theorem OAI.Nagata.Workers.W24.degreeZeroForm_eq_constant line 322
Source documentation
Degree-zero homogeneous plane forms are actual constants.
```
theorem degreeZeroForm_eq_constant (F : PlaneForms 0) :
    F.val = MvPolynomial.C (F.val.coeff 0) := by
…
```
Mentions: OAI.Nagata.Workers.W24.PlaneForms
theorem OAI.Nagata.Workers.W24.degreeZeroForm_evaluation_constant line 329
Source documentation
The leading coefficient's common scalar follows from its actual degree-zero lift, without a general theorem about all global functions on a projective curve.
```
theorem degreeZeroForm_evaluation_constant {ι : Type*} (a : ι → Fin 3 → ℂ)
    (F : PlaneForms 0) (i : ι) :
    homogeneousEvaluation 0 a F i = F.val.coeff 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.PlaneForms, OAI.Nagata.Workers.W24.homogeneousEvaluation
theorem OAI.Nagata.Workers.W24.degreeZeroForm_constant_ne_zero line 336
Source documentation
A nonzero degree-zero lift gives a nonzero common scalar.
```
theorem degreeZeroForm_constant_ne_zero (F : PlaneForms 0) (hF : F ≠ 0) :
    F.val.coeff 0 ≠ 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.PlaneForms

theorem OAI.Nagata.Workers.W24.exists_vector_outside_range line 356

Source documentation

A genuine linear map with smaller domain dimension misses a vector.

theorem exists_vector_outside_range {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V] [Module.Finite K V]
    [AddCommGroup W] [Module K W] (f : V →ₗ[K] W)
    (hdim : finrank K V < finrank K W) : ∃ c : W, c ∉ f.range := by
…