we-solve (beta)

Math-2518-A1 · revision r1 · on Math-2518

OpenAI claim summary for Math-2518

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The ring has Krull dimension two and is regular, local, and ramified in characteristic pair $(0,5)$. A nonzero integral class in degree five becomes zero in the fraction field, which already contradicts the unrestricted first Gersten injection. This is presented as a claimed negative answer.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Integral K5 injectivity for regular local domains
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Integral K5 injectivity for regular local domains

OpenAI's claim

OpenAI presents a counterexample in the selected manuscript. A ramified regular local ring of dimension two in characteristic pair $(0,5)$ is claimed to have a nonzero integral $K_5$ class that dies over its fraction field.

Mathematical statement of the claimed result

Result 1.
Let $V$ be the integer ring of the unramified degree-eight extension of $\mathbb Q_5$. For \[ A=(V[x,y]/(5+x^4+y^4))_{(5,x,y)}, \] the source claims $A$ is a two-dimensional Noetherian regular local domain and \[ \ker(K_5(A)\to K_5(\operatorname{Frac}A))\ne0. \] The failure is for integral Quillen $K_5$, without tensoring with the rationals.

Outline of the argument

Cyclotomic Bott classes on a quartic model are lifted integrally using a $K_4$ vanishing statement. Supported pushforward guarantees generic disappearance, while character averaging and Picard specialization on an elliptic quotient detect the surviving class modulo five.

Formal verification

Family 209 has no Lean scope page in this release. Its selected result is not presented as formalized. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources