OAI.QuadricCounterexample.main_theorem
OpenThe theorem states that SourceMainTheorem holds, a defined proposition about algebraic rank-two bundles on the quadric surface P¹×P¹ (with P¹ modeled as ℂ with one point added at infinity). Such a bundle is given by finitely many principal affine charts, each indexed by a pair in {0,1}² and cut out by a polynomial equation in two variables, together with 2×2 matrix transition functions that are the identity on the diagonal, satisfy the cocycle rule on triple overlaps, and have entries that are rational functions regular in the affine coordinates; the charts must cover the whole surface. The claim is that there exist one such bundle G and a family of such bundles E(m), one for each positive integer m, such that: (1) for every m>0, E(m) is a power-pullback twist of G, meaning it has the same number of charts and the same chart indices, its chart equations are those of G with every variable X replaced by X^m, and its transition matrices equal G's transition matrices evaluated at the m-th power map (z,w)↦(z^m,w^m) on both factors, multiplied by the scalar polarization transition, which is the product of the two hyperplane-transition factors (1 if the indices agree, otherwise the relevant affine coordinate) for the two P¹ factors; (2) for every m>0, E(m) is ample, meaning that for some n>0 and finitely many sections of the n-th symmetric power (given by chart coefficients that are regular and compatible with the dual transition matrices, the transposes of the reversed transitions), the induced map on nonzero fiber vectors of the dual gives a closed projective embedding, defined by nonvanishing of the section vector, injectivity up to the fiber identification, a projective algebraic cone as image, and local rational inverse formulas; and (3) there is a threshold m₀>0 such that for every m≥m₀, E(m) admits no smooth Hermitian metric that is strictly Griffiths positive. Here a smooth Hermitian metric is a family of C^∞ positive definite dual matrices on the chart coordinate domains, compatible across overlaps by the rule H_j = Aᴴ H_i A with A the dual transition, and strict Griffiths positivity requires, at every point and for every nonzero tangent vector u, that the mixed second derivative of the metric in direction u minus the conjugate-transpose of its holomorphic derivative times the inverse metric times that derivative is positive definite.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/QuadricBundles.lean; bytes 8774..8828 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_QuadricBundles namespace OAI noncomputable section namespace QuadricCounterexample open Set Filter Topology Metric OnePoint open scoped Matrix.Norms.Elementwise ComplexOrder
theorem main_theorem : SourceMainTheorem := by sorry end QuadricCounterexample end end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.