we-solve (beta)

Math-2541 · mathematics · Algebraic geometry

Conditional good models for strongly Q-factorial Kähler fourfolds

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Assume full orbifold Iitaka subadditivity in Fujiki class C, the stated pseudo-effective klt fourfold MMP conditional on it, and abundance for nef klt fourfold adjoints after nonvanishing. For a normal connected globally strongly Q-factorial compact Kähler fourfold X with effective rational klt boundary B and Q-Cartier analytically pseudo-effective $K_X+B$, must there be a bimeromorphic good minimal model extracting no divisor, improving discrepancies strictly on contracted primes and having a globally generated positive Cartier adjoint multiple?

Short English statement

Assume full orbifold Iitaka subadditivity in Fujiki class C, the stated pseudo-effective klt fourfold MMP conditional on it, and abundance for nef klt fourfold adjoints after nonvanishing. For a normal connected globally strongly Q-factorial compact Kähler fourfold X with effective rational klt boundary B and Q-Cartier analytically pseudo-effective $K_X+B$, must there be a bimeromorphic good minimal model extracting no divisor, improving discrepancies strictly on contracted primes and having a globally generated positive Cartier adjoint multiple?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2541

Manuscript 1 (family 034, 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.

Conditional good models for strongly Q-factorial Kähler fourfolds

OpenAI's claim

Under explicit orbifold-subadditivity, fourfold-program, and abundance assumptions, good minimal models are claimed for the specified compact Kähler klt fourfold pairs. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
This is explicitly conditional on three global premises: $1$ orbifold Iitaka subadditivity in all dimensions for smooth compact manifolds in Fujiki class $\mathcal C$, namely $\kappa(X,K_X+\Delta)\ge\kappa(F,K_F+\Delta|_F)+\kappa(f\mid\Delta)$ for connected-fiber holomorphic fibrations with rational simple-normal-crossing boundary; $\kappa(f\mid\Delta)$ is the Kodaira dimension of the neat orbifold base, using infimum fiber multiplicities; $2$ existence and termination of every negative-extremal-ray minimal model program for pseudo-effective rational klt adjoints on globally strongly rational-factorial compact Kähler fourfolds, with projective divisorial contractions or log-canonical-positive flips and a nef endpoint; $3$ semiampleness of a nef rational klt fourfold adjoint already having nonnegative Iitaka dimension. Given these premises, take a normal connected compact Kähler fourfold $X$ with effective rational $B$, klt pair $(X,B)$, and rational Cartier analytically pseudo-effective $D=K_X+B$. Assume every global rank-one coherent reflexive sheaf has an invertible positive reflexive power. OpenAI claims a bimeromorphic contraction $\phi:X\dashrightarrow Y$ to a fourfold of the same category such that, writing $B_Y=\phi_*B$, \[ D_Y=K_Y+B_Y\text{ is nef and semiample},\qquad a(E;Y,B_Y)\ge a(E;X,B) \] for every prime divisor over the models, strictly for every prime on $X$ contracted by $\phi$. The map extracts no divisor. The three premises are part of the theorem, rather than conclusions proved without assumptions.

Outline of the argument

Manuscript 1 (family 034, 2026-10-05): Nonvanishing is obtained by fibrations when they exist and by minimal singular metrics in algebraic dimension zero. Spherical transverse structures, reduced-boundary models, gluing of pluricanonical sections, and multiplier-ideal extension address the remaining zero-dimensional-algebraic case before returning to the assumed nef endpoint.

Formal verification

Family 034 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 →