GeometricCollision.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Collision for geometric section families and necessary sections

theorem OAI.Nagata.W20.source_collision_of_every_configuration line 26

Source documentation

The manuscript collision conclusion for the literal source section space and actual jet map. Finite basis and all analytic coefficient premises have been discharged. Only the universal necessary-W geometric input remains.

theorem source_collision_of_every_configuration
    {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (a delta x0 : ℝ) (d : ℤ) (m q : ℕ)
    (hs : (∑ i, marks i) = 9 * x0 - delta)
    (hd : 3 * (m : ℤ) < d)
    (hfirst : ∀ j : ℤ, 0 ≤ j → j ≤ (m : ℤ) →
      firstLower d (m : ℤ) j a delta ∉ Set.range (Int.cast : ℤ → ℝ))
    (hsecond : ∀ j : ℤ, (m : ℤ) < j → j ≤ d / 3 → 0 < d - 3 * j →
      secondLower d j a delta ∉ Set.range (Int.cast : ℤ → ℝ))
    {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
    (hEvery : ∀ p : Fin q → ℂ, Function.Injective p → (∀ i, p i ∈ U) →
      ∃ F : genuineSourceSections hτ hτone marks a d m, F ≠ 0 ∧
…

theorem OAI.Nagata.W20.genuineSourceJetMap_eq_mixed_derivative line 50

Source documentation

The actual source jet rows are the manuscript's mixed derivatives in one fixed covering frame. Row first coordinate is b, second is ell.

theorem genuineSourceJetMap_eq_mixed_derivative
    {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (a x0 : ℝ) (d : ℤ) (m q : ℕ)
    (F : genuineSourceSections hτ hτone marks a d m)
    (row : Nagata.Workers.W30.JetIndex q m) :
    genuineSourceJetMap hτ hτone marks a x0 d m q F row =
      iteratedDeriv row.2.val
        (fun x => iteratedDeriv row.1.val
          (fun y => localScalar F (tauPower τ x0) x y) 0) 0 := by
…

Mentions: OAI.Nagata.Workers.W30.JetIndex, OAI.Nagata.W20.localScalar

theorem OAI.Nagata.W20.source_necessary_W_of_cubic_geometry line 76

Source documentation

Genuine universal-support specialization, transported to the exact Wτ used by the source basis and collision map, with all scalar identifications discharged.

theorem source_necessary_W_of_cubic_geometry {q d m : ℕ} {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1)
    (hUniversal : Nagata.W13.UniversalSupport (9 + q) d (fun _ => m))
    (marks : Fin 9 → ℝ) (a x0 : ℝ)
    (hdisjoint : Pairwise (fun i j => ∀ k : ℤ,
      ((τ ^ marks i : ℝ) : ℂ) ≠ ((τ ^ marks j : ℝ) : ℂ) * (τ : ℂ) ^ k))
    (ξ : Fin q → ℂ)
    (hpP : ∀ i, (Nagata.W22.rayMarkedSection hτ hτone marks).val
      (tauPower τ x0 * Complex.exp (ξ i)) ≠ 0)
    (C : MvPolynomial (Fin 3) ℂ) (hC : C.IsHomogeneous 3)
    (X : Fin 3 → Nagata.W08.automorphicSections (τ : ℂ) 3
      (tauPower τ (((∑ i, marks i) + a) / 3)))
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W22.rayMarkedSection, OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.W20.source_markedPi_cover_eq line 150

Source documentation

Equality of the actual source marked section with the actual marked product on the common exponential chart.

theorem source_markedPi_cover_eq {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (x0 : ℝ) (x : ℂ) :
    (Nagata.W22.rayMarkedSection hτ hτone marks).val
      (tauPower τ x0 * Complex.exp x) =
    Nagata.W06.TorusConfiguration.markedPi τ marks
      (Nagata.Workers.W05.chartPoint τ x0 x : ℂ) := by
…

Mentions: OAI.Nagata.W22.rayMarkedSection, OAI.Nagata.W06.TorusConfiguration.markedPi, OAI.Nagata.Workers.W05.chartPoint

theorem OAI.Nagata.W20.source_marked_orbits_disjoint line 165

Source documentation

The actual marked ray lifts occupy pairwise disjoint period orbits.

theorem source_marked_orbits_disjoint {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (hinj : Function.Injective marks)
    (hb : ∀ i, 0 < marks i ∧ marks i < 1 / 2) :
    Pairwise (fun i j => ∀ k : ℤ,
      ((τ ^ marks i : ℝ) : ℂ) ≠ ((τ ^ marks j : ℝ) : ℂ) * (τ : ℂ) ^ k) := by
…

theorem OAI.Nagata.W20.source_collision_of_universalSupport_and_cubic_geometry line 190

Source documentation

Fixed-period source collision from genuine universal support and concrete cubic chart geometry. No finite basis, analytic section, Pi-nonvanishing, local multiplicity, or moving-sequence hypothesis remains.

theorem source_collision_of_universalSupport_and_cubic_geometry
    {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    (marks : Fin 9 → ℝ) (hmarks : Function.Injective marks)
    (hmbounds : ∀ i, 0 < marks i ∧ marks i < 1 / 2)
    (a delta : ℝ) (d m q : ℕ)
    (hs : (∑ i, marks i) = 9 * (1 / 2 : ℝ) - delta)
    (hd : 3 * (m : ℤ) < (d : ℤ))
    (hfirst : ∀ j : ℤ, 0 ≤ j → j ≤ (m : ℤ) →
      firstLower (d : ℤ) (m : ℤ) j a delta ∉ Set.range (Int.cast : ℤ → ℝ))
    (hsecond : ∀ j : ℤ, (m : ℤ) < j → j ≤ (d : ℤ) / 3 → 0 < (d : ℤ) - 3 * j →
      secondLower (d : ℤ) j a delta ∉ Set.range (Int.cast : ℤ → ℝ))
    (hUniversal : Nagata.W13.UniversalSupport (9 + q) d (fun _ => m))
…

Mentions: OAI.Nagata.W13.UniversalSupport