MarkedCubic.lean`

42 declarations, 0 contain sorry, 0 declared as axioms

Marked cubic charts, multipliers, coordinate compatibility, and smooth geometry

theorem OAI.Nagata.W06.TorusConfiguration.rayPoint_zero line 21
theorem OAI.Nagata.W06.TorusConfiguration.rayPoint_add line 25
theorem OAI.Nagata.W06.TorusConfiguration.rayPoint_nat_mul line 30
theorem OAI.Nagata.W06.TorusConfiguration.rayPoint_sum line 36
theorem OAI.Nagata.W06.TorusConfiguration.piMultiplier_eq_neg_rayPoint_sum line 44
Source documentation
The nine-point theta multiplier is exactly -τ^(sum x_i) in the chosen frame.
```
theorem piMultiplier_eq_neg_rayPoint_sum (τ : ℝ) (xi : Fin 9 → ℝ) :
    piMultiplier τ xi = -(rayPoint τ (∑ i, xi i)) := by
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.piMultiplier
theorem OAI.Nagata.W06.TorusConfiguration.normalMultiplier_eq_rayPoint line 51
Source documentation
The normal-bundle multiplier is the literal cube τ^(3η).
```
theorem normalMultiplier_eq_rayPoint (τ η : ℝ) :
    rayPoint τ η ^ 3 = rayPoint τ (3 * η) := by
…
```
theorem OAI.Nagata.W06.TorusConfiguration.sourceAMultiplier line 56
Source documentation
Exact A multiplier from the source relation 3η=sum(x_i)+rhoStar.
```
theorem sourceAMultiplier (τ η rhoStar : ℝ) (xi : Fin 9 → ℝ)
    (hη : 3 * η = (∑ i, xi i) + rhoStar) :
    rayPoint τ η ^ 3 / piMultiplier τ xi = -(rayPoint τ rhoStar) := by
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.piMultiplier
theorem OAI.Nagata.W06.TorusConfiguration.sourceAMultiplier_eta line 65
Source documentation
The source's unreduced exponent eta satisfies the required multiplier identity.
```
theorem sourceAMultiplier_eta (τ rhoStar : ℝ) (xi : Fin 9 → ℝ) :
    rayPoint τ (((∑ i, xi i) + rhoStar) / 3) ^ 3 / piMultiplier τ xi =
      -(rayPoint τ rhoStar) := by
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.piMultiplier

def OAI.Nagata.W06.TorusConfiguration.actualMarkedVector line 83

Source documentation

Actual degree-three theta evaluation vector at each selected covering lift.

def actualMarkedVector {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) : Fin 3 → ℂ :=
…

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedVector_ne_zero line 88

def OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint line 95

Source documentation

The actual cubic-map point, with multiplier exactly τ^η.

def actualMarkedPoint {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) : PlanePoint :=
…

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint_eq_mk line 100

Source documentation

The actual selected evaluation vector represents the actual projective point.

theorem actualMarkedPoint_eq_mk {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) :
    actualMarkedPoint hτ hτone η x0 xi ξ t =
      Projectivization.mk ℂ (actualMarkedVector hτ hτone η x0 xi ξ t)
        (actualMarkedVector_ne_zero hτ hτone η x0 xi ξ t) := rfl

Mentions: OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint, OAI.Nagata.W06.TorusConfiguration.actualMarkedVector, OAI.Nagata.W06.TorusConfiguration.actualMarkedVector_ne_zero

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint_injective line 106

def OAI.Nagata.W06.TorusConfiguration.actualMarkedConfiguration line 113

Source documentation

Actual ordered distinct points with the cubic embedding premise discharged.

def actualMarkedConfiguration {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ)
    (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ)) : OrderedDistinctPoints (9 + q) :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

def OAI.Nagata.W06.TorusConfiguration.actualMarkedConfigurationOfEq line 120

Source documentation

Exact r=9+q reindexing of the actual cubic configuration.

def actualMarkedConfigurationOfEq {r q : ℕ} (hr : r = 9 + q)
    {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (η x0 : ℝ) (xi : Fin 9 → ℝ)
    (ξ : Fin q → ℂ) (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ)) :
    OrderedDistinctPoints r :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedConfigurationOfEq_apply line 127

Source documentation

Every indexed actual point has its specified homogeneous evaluation vector.

theorem actualMarkedConfigurationOfEq_apply {r q : ℕ} (hr : r = 9 + q)
    {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (η x0 : ℝ) (xi : Fin 9 → ℝ)
    (ξ : Fin q → ℂ) (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ)) (i : Fin r) :
    (actualMarkedConfigurationOfEq hr hτ hτone η x0 xi ξ hinj).val i =
      Projectivization.mk ℂ (actualMarkedVector hτ hτone η x0 xi ξ (Fin.cast hr i))
        (actualMarkedVector_ne_zero hτ hτone η x0 xi ξ (Fin.cast hr i)) := rfl

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W06.TorusConfiguration.actualMarkedConfigurationOfEq, OAI.Nagata.W06.TorusConfiguration.actualMarkedVector, OAI.Nagata.W06.TorusConfiguration.actualMarkedVector_ne_zero

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedVector_left line 134
theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedVector_right line 142
theorem OAI.Nagata.W06.TorusConfiguration.exists_actualMarkedCubicForm line 152
Source documentation
One actual nonzero cubic equation vanishes on all the marked evaluation vectors. The equation comes from the complete actual map, independently of q and its marks.
```
theorem exists_actualMarkedCubicForm {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (η : ℝ) :
    ∃ G : NonzeroHomogeneousForm 3, ∀ (x0 : ℝ) (xi : Fin 9 → ℝ)
      (q : ℕ) (ξ : Fin q → ℂ) (t : Fin (9 + q)),
      MvPolynomial.eval (actualMarkedVector hτ hτone η x0 xi ξ t) G.polynomial = 0 := by
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.actualMarkedVector

theorem OAI.Nagata.W06.TorusConfiguration.exists_actualMarkedConfiguration_disk line 161

Source documentation

Every real period supports every finite nearby configuration on the actual projective cubic map. No map, basis, dimension or embedding assumption is supplied.

theorem exists_actualMarkedConfiguration_disk {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η : ℝ) (xi : Fin 9 → ℝ) (hxi : Function.Injective xi)
    (hxi_bounds : ∀ i, 0 < xi i ∧ xi i < 1 / 2) :
    ∃ R : ℝ, 0 < R ∧ ∀ (q : ℕ) (ξ : Fin q → ℂ),
      Function.Injective ξ → (∀ j, ‖ξ j‖ < R) →
      ∃ p : OrderedDistinctPoints (9 + q),
        (∀ t, p.val t = actualMarkedPoint hτ hτone η (1 / 2) xi ξ t) ∧
        ∀ j, markedPi τ xi (chartPoint τ (1 / 2) (ξ j) : ℂ) ≠ 0 := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint, OAI.Nagata.W06.TorusConfiguration.markedPi

def OAI.Nagata.W06.TorusConfiguration.actualCoordinateSections line 190
Source documentation
The three actual holomorphic multiplier sections defining the genuine map.
```
def actualCoordinateSections {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (η : ℝ) :
    Fin 3 → automorphicSections (τ : ℂ) 3 (rayPoint τ η : ℂ) :=
…
```
def OAI.Nagata.W06.TorusConfiguration.actualCoordinateFunctions line 195
Source documentation
Literal covering-space coordinate functions; no representative choices enter.
```
def actualCoordinateFunctions {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (η : ℝ) :
    Fin 3 → ℂ → ℂ := fun a => (actualCoordinateSections hτ hτone η a).val
```
Mentions: OAI.Nagata.W06.TorusConfiguration.actualCoordinateSections
theorem OAI.Nagata.W06.TorusConfiguration.actualCoordinateFunctions_analyticAt line 198
theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedVector_coordinate line 203
theorem OAI.Nagata.W06.TorusConfiguration.exists_actualMarkedChart line 208

def OAI.Nagata.W06.TorusConfiguration.actualMarkedChart line 217

Source documentation

A genuine nonzero homogeneous coordinate is chosen at every actual marked point.

def actualMarkedChart {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) : Fin 3 :=
…

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedChart_nonzero line 221
theorem OAI.Nagata.W06.TorusConfiguration.actualNormalizedPoint_coordinates line 227

theorem OAI.Nagata.W06.TorusConfiguration.actualNormalizedPoint_eq line 241

Source documentation

The normalized point has precisely the actual projective image; any valid chart may be used, including a chart chosen later for a nonzero normal derivative.

theorem actualNormalizedPoint_eq {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) (c : Fin 3)
    (hc : actualCoordinateFunctions hτ hτone η c (coverTuple τ x0 xi ξ t : ℂ) ≠ 0) :
    chartPoint₂ c (planeCoordinate (normalizedCurvePoint (actualCoordinateFunctions hτ hτone η) c
      (coverTuple τ x0 xi ξ t : ℂ))) = actualMarkedPoint hτ hτone η x0 xi ξ t := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.actualCoordinateFunctions, OAI.Nagata.W06.TorusConfiguration.coverTuple, OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint

theorem OAI.Nagata.W06.TorusConfiguration.actualNormalizedConfiguration_injective line 251

def OAI.Nagata.W06.TorusConfiguration.actualCoverOfEq line 277

Source documentation

Exact covering lifts after the source equality r=9+q.

def actualCoverOfEq {r q : ℕ} (hr : r = 9 + q) (τ x0 : ℝ)
    (xi : Fin 9 → ℝ) (ξ : Fin q → ℂ) (i : Fin r) : ℂˣ :=
…

def OAI.Nagata.W06.TorusConfiguration.actualDisplacementOfEq line 283
Source documentation
The literal source displacement over each reindexed genuine torus point. This is an actual multiplier fibre, whose geometric normal identification is separate.
```
def actualDisplacementOfEq {r q : ℕ} (hr : r = 9 + q)
    {τ : ℝ} (hτ : 0 < τ) (η x0 : ℝ) (xi : Fin 9 → ℝ) (ξ : Fin q → ℂ) (i : Fin r) :
    QuotientFibre (positivePeriod τ hτ) (rayPoint τ η ^ 3) 9
      (torusPointMk (positivePeriod τ hτ) (actualCoverOfEq hr τ x0 xi ξ i)) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.QuotientFibre, OAI.Nagata.W06.TorusConfiguration.actualCoverOfEq
theorem OAI.Nagata.W06.TorusConfiguration.actualDisplacementOfEq_globalPi line 291
Source documentation
Full list compatibility with the genuine global Pi map, with the cubic's actual degree-three multiplier τ^η; this holds for every indexed point.
```
theorem actualDisplacementOfEq_globalPi {r q : ℕ} (hr : r = 9 + q)
    {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) (η x0 : ℝ) (xi : Fin 9 → ℝ)
    (ξ : Fin q → ℂ) (i : Fin r) :
    (actualDisplacementOfEq hr hτ η x0 xi ξ i).val =
      piQuotientMap hτ hτone (rayPoint τ η) xi
        (Quotient.mk _ (actualCoverOfEq hr τ x0 xi ξ i, (1 : ℂ))) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.actualDisplacementOfEq, OAI.Nagata.W06.TorusConfiguration.piQuotientMap, OAI.Nagata.W06.TorusConfiguration.actualCoverOfEq
theorem OAI.Nagata.W06.TorusConfiguration.actualNormalizedConfigurationOfEq_injective line 299

theorem OAI.Nagata.W06.TorusConfiguration.actual_source_configuration_for_every_period line 317

Source documentation

The actual source configuration exists for every period and every r≥9, with q=r−9, for every distinct tuple in a common disk. The source's literal eta and all homogeneous representatives are retained.

theorem actual_source_configuration_for_every_period {Δ τ : ℝ}
    (hΔ : 0 < Δ) (hhalf : Δ < 1 / 2) (hτ : 0 < τ) (hτone : τ < 1) (rhoStar : ℝ) :
    ∃ R : ℝ, 0 < R ∧ ∀ (r : ℕ) (hr : 9 ≤ r) (ξ : Fin (r - 9) → ℂ),
      Function.Injective ξ → (∀ j, ‖ξ j‖ < R) →
      ∃ p : OrderedDistinctPoints r,
        (∀ i : Fin r, p.val i =
          actualMarkedPoint hτ hτone (((∑ j, markedExponent Δ j) + rhoStar) / 3)
            (1 / 2) (markedExponent Δ) ξ (Fin.cast (by omega : r = 9 + (r - 9)) i)) ∧
        (∀ j, markedPi τ (markedExponent Δ) (chartPoint τ (1 / 2) (ξ j) : ℂ) ≠ 0) := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.actualMarkedPoint, OAI.Nagata.W06.markedExponent, OAI.Nagata.W06.TorusConfiguration.markedPi

theorem OAI.Nagata.W06.TorusConfiguration.actualMarkedChart_gradient line 346

Source documentation

The chosen containing chart has a genuine nonzero polynomial differential.

theorem actualMarkedChart_gradient {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous 3)
    (hzero : ∀ z : ℂ, z ≠ 0 → MvPolynomial.eval
      (fun i => actualCoordinateFunctions hτ hτone η i z) G = 0)
    (hgrad : ∀ z : ℂ, z ≠ 0 → ∃ j, MvPolynomial.eval
      (fun i => actualCoordinateFunctions hτ hτone η i z) (MvPolynomial.pderiv j G) ≠ 0)
    (t : Fin (9 + q)) :
    polynomialGradient (Nagata.W27.directChartHom (actualMarkedChart hτ hτone η x0 xi ξ t) G)
      (normalizedCurvePoint (actualCoordinateFunctions hτ hτone η)
        (actualMarkedChart hτ hτone η x0 xi ξ t) (coverTuple τ x0 xi ξ t : ℂ)) ≠ 0 :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.actualCoordinateFunctions, OAI.Nagata.W27.directChartHom, OAI.Nagata.W06.TorusConfiguration.actualMarkedChart, OAI.Nagata.W06.TorusConfiguration.coverTuple

theorem OAI.Nagata.W06.TorusConfiguration.actualMarked_smooth_chart_data line 365

Source documentation

The exact simultaneous chart package for actual normal specialization: nonzero denominator, distinct projective base points, nonzero actual differential.

theorem actualMarked_smooth_chart_data {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (η x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ)
    (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ))
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous 3)
    (hzero : ∀ z : ℂ, z ≠ 0 → MvPolynomial.eval
      (fun i => actualCoordinateFunctions hτ hτone η i z) G = 0)
    (hgrad : ∀ z : ℂ, z ≠ 0 → ∃ j, MvPolynomial.eval
      (fun i => actualCoordinateFunctions hτ hτone η i z) (MvPolynomial.pderiv j G) ≠ 0) :
    (∀ t, actualCoordinateFunctions hτ hτone η (actualMarkedChart hτ hτone η x0 xi ξ t)
      (coverTuple τ x0 xi ξ t : ℂ) ≠ 0) ∧
    Function.Injective (fun t => chartPoint₂ (actualMarkedChart hτ hτone η x0 xi ξ t)
      (planeCoordinate (normalizedCurvePoint (actualCoordinateFunctions hτ hτone η)
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W06.TorusConfiguration.actualCoordinateFunctions, OAI.Nagata.W06.TorusConfiguration.actualMarkedChart, OAI.Nagata.W06.TorusConfiguration.coverTuple

def OAI.Nagata.W06.TorusConfiguration.sourceCoordinateSections line 400

Source documentation

Actual coordinate sections, with the source's unreduced τ^η multiplier type.

def sourceCoordinateSections {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (a : ℝ) :
    Fin 3 → automorphicSections (τ : ℂ) 3 (tauPower τ (((∑ i, marks i) + a) / 3)) :=
…

theorem OAI.Nagata.W06.TorusConfiguration.sourceCoordinateSections_val line 407

theorem OAI.Nagata.W06.TorusConfiguration.markedNormalBase_eq_coverTuple line 413

Source documentation

Both finite indexing conventions list exactly the same nonzero covering lifts.

theorem markedNormalBase_eq_coverTuple {τ : ℝ} (hτ : 0 < τ)
    (marks : Fin 9 → ℝ) (x0 : ℝ) {q : ℕ} (ξ : Fin q → ℂ) (b : Fin (9 + q)) :
    markedNormalBase (fun i => ((τ ^ marks i : ℝ) : ℂ))
      (logarithmicPoints (tauPower τ x0) ξ) b = (coverTuple τ x0 marks ξ b : ℂ) := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.coverTuple

theorem OAI.Nagata.W06.TorusConfiguration.markedNormalBase_eq_coverTuple_fun line 431

Source documentation

Pointwise equality extends to the complete actual finite base list.

theorem markedNormalBase_eq_coverTuple_fun {τ : ℝ} (hτ : 0 < τ)
    (marks : Fin 9 → ℝ) (x0 : ℝ) {q : ℕ} (ξ : Fin q → ℂ) :
    markedNormalBase (fun i => ((τ ^ marks i : ℝ) : ℂ)) (logarithmicPoints (tauPower τ x0) ξ) =
      fun b => (coverTuple τ x0 marks ξ b : ℂ) :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.coverTuple

theorem OAI.Nagata.W06.TorusConfiguration.exists_actual_source_smooth_geometry line 453

Source documentation

One actual regular cubic and actual source-typed coordinate space supply all marked configurations. Distinctness is the only tuple condition; the fixed-period disk theorem proves it for every distinct tuple sufficiently near zero.

theorem exists_actual_source_smooth_geometry {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (a : ℝ) :
    ∃ C : MvPolynomial (Fin 3) ℂ, Prime C ∧ C.IsHomogeneous 3 ∧
      ∃ X : Fin 3 → Nagata.W08.automorphicSections (τ : ℂ) 3
          (tauPower τ (((∑ i, marks i) + a) / 3)),
        Nagata.Workers.W25.polynomialRelationIdeal (fun i => (X i).val) = Ideal.span ({C} : Set _) ∧
        ∀ (q : ℕ) (ξ : Fin q → ℂ),
          Function.Injective (torusTuple τ hτ (1 / 2) marks ξ) →
          ∃ chart : Fin (9 + q) → Fin 3,
            (∀ b, (X (chart b)).val
              (markedNormalBase (fun i => ((τ ^ marks i : ℝ) : ℂ))
                (logarithmicPoints (tauPower τ (1 / 2)) ξ) b) ≠ 0) ∧
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.Workers.W25.polynomialRelationIdeal, OAI.Nagata.W06.TorusConfiguration.torusTuple