we-solve (beta)

Math-2544 · mathematics · Algebraic geometry

Existence of a finite ordinary Kähler fourfold program

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For a normal globally Weil-Q-factorial compact Kähler fourfold X with rational klt boundary $\Delta $, does there exist an ordinary negative program starting exactly on X and ending nef for pseudo-effective $K_X+\Delta $, or in a projective relative-Picard-one Mori contraction otherwise, preserving klt and global Weil Q-factoriality and not extracting primes? The composite must not decrease discrepancies and must strictly improve those of contracted X-primes.

Short English statement

For a normal globally Weil-Q-factorial compact Kähler fourfold X with rational klt boundary $\Delta $, does there exist an ordinary negative program starting exactly on X and ending nef for pseudo-effective $K_X+\Delta $, or in a projective relative-Picard-one Mori contraction otherwise, preserving klt and global Weil Q-factoriality and not extracting primes? The composite must not decrease discrepancies and must strictly improve those of contracted X-primes.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2544-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2544

Manuscript 1 (family 056, 2026-09-24): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

Existence of a finite ordinary Kähler fourfold program

OpenAI's claim

For the stated compact Kähler klt fourfold pairs, at least one ordinary program is claimed to start on the supplied model, take finitely many steps, and finish nef or in a Mori fiber space. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
For a normal globally Weil rational-factorial compact Kähler fourfold $X$ with rational effective $\Delta$ and klt pair $(X,\Delta)$, OpenAI claims existence of a finite ordinary negative-extremal-ray program starting on $X$, using projective divisorial contractions and flips. With $D=K_X+\Delta$, its endpoint satisfies \[ D\text{ pseudo-effective}\Rightarrow D_n\text{ nef},\qquad D\text{ not pseudo-effective}\Rightarrow X_n\to S\text{ a Mori fiber contraction}. \] All models remain normal globally Weil rational-factorial compact Kähler and klt. The first composite extracts no divisor and increases discrepancies weakly for all primes and strictly for contracted original primes. The Mori contraction has connected fibers, normal compact Kähler base of dimension below four, relative Picard rank one and relatively ample $-D_n$. Each contraction has relative Bott--Chern dimension one; strong rational-factoriality is preserved when assumed. Unlike the later manuscript, this main theorem states existence of a finite program, not termination of every choice.

Outline of the argument

Manuscript 1 (family 056, 2026-09-24): A single initial Kähler form is tracked as a positive current on the comparison models. Real-boundary terminal termination and power-free descent of actual lines preserve a fixed positive intersection gap, so rational perturbations transfer an auxiliary construction into the required ordinary program.

Formal verification

Family 056 has no Lean scope page in this snapshot; no formalization of these manuscript results is listed.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →