we-solve (beta)

Math-2682-A1 · revision r1 · on Math-2682

OpenAI claim summary for Math-2682

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.

Nodal upper length on surfaces: The paper claims nodal length at most $C\sqrt\lambda$ for every real nonzero Laplace eigenfunction on a fixed smooth closed surface. Combined with the established lower estimate, this settles the two-dimensional smooth setting. The parameters, regularity assumptions and normalization in this question are retained in applying that assertion.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

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

Manuscript

Contents
  1. Sharp nodal upper bound on smooth surfaces
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Sharp nodal upper bound on smooth surfaces

OpenAI's claim

Nodal upper length on surfaces: The paper claims nodal length at most $C\sqrt\lambda$ for every real nonzero Laplace eigenfunction on a fixed smooth closed surface. Combined with the established lower estimate, this settles the two-dimensional smooth setting.

Mathematical statement of the claimed result

Mathematical claim 1.
Fix a smooth metric $g$ on a closed connected surface $M$. One finite $C(M,g)$ is asserted to work simultaneously for all nonzero real eigenfunctions solving $-\Delta_gu=\lambda u$, $\lambda>0$, satisfies \[\mathcal H_g^1(\{u=0\})\le C(M,g)\sqrt\lambda.\] The constant is shared by all eigenfunctions in all positive eigenspaces; the assertion is specific to surfaces.

Outline of the argument

Nodal upper length on surfaces: Subharmonic profile limits control local growth under affine subdivision. High-growth excursions along grid paths produce witness regions on which growth persists to terminal scale. A packing argument pays for witness regions outside their entry squares using summable collars, bounding the terminal average growth and hence nodal length.

Formal verification

Family 350 describes Lean coverage for the surface upper bound and the three- and four-dimensional fixed-metric violations; the five-dimensional power-law refinement is separate.

Nodal upper length on surfaces: The manuscript links NodalLength.lean, SmoothYau.lean (declaration OAI.YauCounterexamples.sphere_three), SmoothYau.lean (declaration OAI.YauCounterexamples.sphere_two_torus_two), YauCounterexample.lean (declaration OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources