we-solve (beta)

Math-2682 · mathematics · Geometry

Sharp nodal upper bound on smooth surfaces

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For each connected closed smooth Riemannian surface (M,g), does one finite C(M,g) bound $H^{1}_g({u=0})\leq C(M,g)\surd \lambda $ for every nonzero real smooth eigenfunction $-\Delta _g$ $u=\lambda u$ with $\lambda >0$?

Short English statement

For each connected closed smooth Riemannian surface (M,g), does one finite C(M,g) bound $H^{1}_g({u=0})\leq C(M,g)\surd \lambda $ for every nonzero real smooth eigenfunction $-\Delta _g$ $u=\lambda u$ with $\lambda >0$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2682

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.

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

Go to contribution →