OAI/AlgebraicGeometry/PlaneCurves/BasisNoncancellation.lean
13 declarations, 0 contain sorry, 0 declared as axioms
Same-basis coefficient and polynomial noncancellation
- theorem
OAI.Nagata.Workers.W12.sourceBasis_localScalar_eq_thetaline 46Source documentation
All literal column expressions, including the degree-zero tip, agree with exactly the scalar basis used in the proved limiting matrix.
theorem sourceBasis_localScalar_eq_theta (col : Column d (m : ℤ) a delta) (x y : ℂ) : localScalar (polynomialBasisFromSourceBases (τ : ℂ) γL γP d m a delta P hd hP hPfin b col) z0 x y = basisCoefficient d (m : ℤ) a delta marks τ col x * Complex.exp ((col.val.1 : ℂ) * y) := by … - theorem
OAI.Nagata.Workers.W12.sourceBasis_actualJetMatrix_eq_thetaline 62Source documentation
Actual mixed derivatives in the assembled genuine basis are the literal finite theta matrix, without a separately assumed matrix identity.
theorem sourceBasis_actualJetMatrix_eq_theta (q : ℕ) (hz0 : z0 ≠ 0) : basisJetMatrix (K := ℂ) … - theorem
OAI.Nagata.Workers.W12.source_coefficient_bridge_contradictionline 90Source documentation
The analytic and finite-matrix estimates rule out the stated coefficient-kernel condition under the strict degree-ratio bounds.
theorem source_coefficient_bridge_contradiction (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m) (hlow : 3 < (d : ℝ) / m) (hupp : (d : ℝ) / m < Real.sqrt r) (hbridge : ∀ (n : ℕ) (delta : ℝ) (x : Fin 9 → ℝ), 0 < n → 0 < delta → delta < 1 / 2 → Function.Injective x → (∀ i, 0 < x i ∧ x i < 1 / 2) → (∑ i : Fin 9, sourceOffsets x i) = delta → (∀ j : ℤ, 0 ≤ j → j ≤ ((n * m : ℕ) : ℤ) → firstLower ((n * d : ℕ) : ℤ) ((n * m : ℕ) : ℤ) j (3 * (Real.sqrt r - 3)) delta ∉ Set.range (Int.cast : ℤ → ℝ)) → (∀ j : ℤ, ((n * m : ℕ) : ℤ) < j → j ≤ ((n * d : ℕ) : ℤ) / 3 → 0 < ((n * d : ℕ) : ℤ) - 3 * j → … - theorem
OAI.Nagata.Workers.W12.source_polynomial_geometric_bridge_contradictionline 136Source documentation
Single-witness source contradiction from concrete moving geometric data. There is no kernel, Taylor-jet, matrix-equality, or rank hypothesis in hgeometry.
theorem source_polynomial_geometric_bridge_contradiction (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m) (hlow : 3 < (d : ℝ) / m) (hupp : (d : ℝ) / m < Real.sqrt r) (hgeometry : ∀ (n : ℕ) (delta : ℝ) (x : Fin 9 → ℝ), 0 < n → 0 < delta → delta < 1 / 2 → Function.Injective x → (∀ i, 0 < x i ∧ x i < 1 / 2) → (∑ i : Fin 9, sourceOffsets x i) = delta → (∀ j : ℤ, 0 ≤ j → j ≤ ((n * m : ℕ) : ℤ) → firstLower ((n * d : ℕ) : ℤ) ((n * m : ℕ) : ℤ) j (3 * (Real.sqrt r - 3)) delta ∉ Set.range (Int.cast : ℤ → ℝ)) → (∀ j : ℤ, ((n * m : ℕ) : ℤ) < j → j ≤ ((n * d : ℕ) : ℤ) / 3 → 0 < ((n * d : ℕ) : ℤ) - 3 * j → … - theorem
OAI.Nagata.Workers.W12.source_actual_section_bridge_contradictionline 210 - theorem
OAI.Nagata.Workers.W12.source_every_configuration_bridge_contradictionline 255Source documentation
Source-facing interface with universal configurations in one open chart. Collision centers and section sequences are constructed internally. This remains conditional on the genuine geometric existence and theta-basis identification.
theorem source_every_configuration_bridge_contradiction (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m) (hlow : 3 < (d : ℝ) / m) (hupp : (d : ℝ) / m < Real.sqrt r) (hgeometry : ∀ (n : ℕ) (delta : ℝ) (x : Fin 9 → ℝ), 0 < n → 0 < delta → delta < 1 / 2 → Function.Injective x → (∀ i, 0 < x i ∧ x i < 1 / 2) → (∑ i : Fin 9, sourceOffsets x i) = delta → (∀ j : ℤ, 0 ≤ j → j ≤ ((n * m : ℕ) : ℤ) → firstLower ((n * d : ℕ) : ℤ) ((n * m : ℕ) : ℤ) j (3 * (Real.sqrt r - 3)) delta ∉ Set.range (Int.cast : ℤ → ℝ)) → (∀ j : ℤ, ((n * m : ℕ) : ℤ) < j → j ≤ ((n * d : ℕ) : ℤ) / 3 → 0 < ((n * d : ℕ) : ℤ) - 3 * j → … - def
OAI.Nagata.Workers.W12.genuineSourceSectionsline 321Source documentation
The genuine global section space at the actual nine marked ray lifts.
def genuineSourceSections := …
- def
OAI.Nagata.Workers.W12.genuineSourceBasisline 326Source documentation
The full actual section basis indexed by all literal manuscript columns.
def genuineSourceBasis : Basis (Column d (m : ℤ) a delta) ℂ (genuineSourceSections hτ hτone ξ a d m) := … - theorem
OAI.Nagata.Workers.W12.genuineSourceBasis_localScalarline 336Source documentation
Every basis column has the exact local scalar formula used in the matrix limit. No local-formula assumption remains.
theorem genuineSourceBasis_localScalar (col : Column d (m : ℤ) a delta) (x y : ℂ) : localScalar (genuineSourceBasis hτ hτone ξ a delta x0 d m hs hd hfirst hsecond col) (tauPower τ x0) x y = basisCoefficient d (m : ℤ) a delta (fun i => x0 - ξ i) τ col x * Complex.exp ((col.val.1 : ℂ) * y) := by … - def
OAI.Nagata.Workers.W12.genuineSourceJetMapline 347Source documentation
The actual linear jet map for the genuine source sections.
def genuineSourceJetMap (q : ℕ) : genuineSourceSections hτ hτone ξ a d m →ₗ[ℂ] (Nagata.Workers.W30.JetIndex q m → ℂ) := …Mentions: OAI.Nagata.Workers.W12.genuineSourceSections, OAI.Nagata.Workers.W30.JetIndex
- theorem
OAI.Nagata.Workers.W12.genuineSourceBasis_jetMatrixline 356Source documentation
Fully instantiated actual-basis-to-literal-matrix identity.
theorem genuineSourceBasis_jetMatrix (q : ℕ) : basisJetMatrix (K := ℂ) (V := genuineSourceSections hτ hτone ξ a d m) … - theorem
OAI.Nagata.Workers.W12.genuineSourceJetMap_injectiveline 369Source documentation
Matrix injectivity transfers to the actual global section jet map.
theorem genuineSourceJetMap_injective (q : ℕ) (hinj : Function.Injective (thetaJetMatrix d q m a delta (fun i => x0 - ξ i) τ).mulVec) : Function.Injective (genuineSourceJetMap hτ hτone ξ a x0 d m q) := by … - theorem
OAI.Nagata.Workers.W12.genuine_source_geometric_contradictionline 393