we-solve (beta)

Math-2528 · mathematics · Algebraic geometry

All ordinary Kähler klt fourfold programs terminate

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 with effective rational klt boundary and rational Cartier canonical adjoint, does every maximal ordinary negative-ray program terminate on the original input, retaining klt and global Weil Q-factoriality, with projective contractions of relative Bott–Chern dimension one? A pseudo-effective input must end nef; otherwise the endpoint must have a projective lower-dimensional Mori fiber contraction. Global strong Q-factoriality, if imposed, must persist.

Short English statement

For a normal globally Weil-Q-factorial compact Kähler fourfold with effective rational klt boundary and rational Cartier canonical adjoint, does every maximal ordinary negative-ray program terminate on the original input, retaining klt and global Weil Q-factoriality, with projective contractions of relative Bott–Chern dimension one? A pseudo-effective input must end nef; otherwise the endpoint must have a projective lower-dimensional Mori fiber contraction. Global strong Q-factoriality, if imposed, must persist.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2528

Manuscript 1 (family 056, 2026-10-05): 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.

All ordinary Kähler klt fourfold programs terminate

OpenAI's claim

Every maximal ordinary negative-ray program for the stated rational compact Kähler klt fourfold pairs is claimed to terminate at a nef model or Mori fiber space according to pseudo-effectivity. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
Let $X$ be normal globally Weil rational-factorial compact Kähler of dimension four, and $\Delta\ge0$ rational with $(X,\Delta)$ klt. Global Weil rational-factoriality means every global Weil divisor has a positive Cartier multiple. Fix compatible canonical Weil representatives, or the intrinsic canonical rational line bundle. OpenAI claims every maximal ordinary negative-extremal-ray program beginning exactly on $X$ terminates in finitely many divisorial contractions and flips. Models remain in the same category; contractions are projective with relative line-bundle rank and Bott--Chern dimension one. For $D=K_X+\Delta$, \[ D\text{ pseudo-effective}\ \Longrightarrow\ D_n\text{ nef},\qquad D\text{ not pseudo-effective}\ \Longrightarrow\ X_n\to S\text{ a Mori fiber contraction}. \] The latter has connected fibers, normal compact Kähler base of dimension below four, relative Picard number one and relatively ample $-D_n$. In the first case no discrepancy decreases, while each original contracted prime has a strictly larger discrepancy on the endpoint, and the composite extracts no prime. Global strong rational-factoriality is also preserved when initially imposed.

Outline of the argument

Manuscript 1 (family 056, 2026-10-05): Auxiliary generalized programs supply the comparison with the ordinary sequence. Descent of numerically trivial actual lines preserves Cartier indices, while corrected discrepancy counts and analytic surface homology prove terminal fourfold termination even with real boundary, allowing arbitrary ordinary ray choices.

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 →