The Lane–Emden and Hénon–Lane–Emden conjectures

1 · The essentials

The question is whether two everywhere-positive quantities can satisfy a pair of linked equations throughout all of space. Each equation describes how one quantity varies in space using a power of the other, multiplied by a factor depending on distance from the origin. The manuscript establishes that no such pair exists when a particular inequality involving the dimension, powers, and distance factors holds. This applies in every dimension of at least two. The quantities must be continuous at the origin and sufficiently smooth to satisfy the equations everywhere else. They do not have to look the same in every direction, and no restriction is imposed on their behavior far away. Under additional restrictions, combining this result with an existing existence theorem gives an exact dividing line between existence and nonexistence.

A picture to help (an imperfect image, not to be taken literally)

As an imperfect image, imagine two linked rules for laying out brightness across an unlimited sheet, with each rule using the other brightness and the distance from a central point. The result says that certain choices of the rules cannot be satisfied with both brightness levels positive everywhere, however unevenly the pattern is arranged.

Why it matters

The result settles the subcritical nonexistence question for both the Lane–Emden system and its weighted Hénon extension. Its scope is important: neither symmetry nor a condition at infinity is required. In dimensions at least three, with both weight exponents greater than $- 2$ , the result combines with known radial existence to give an exact existence criterion.

2 · Going further

The precise system is $- Δ u = ∣ x ∣^{A} v^{p}$ , $- Δ v = ∣ x ∣^{B} u^{q}$ on $R^{n}$ , with $n \geq 2$ , $p, q > 0$ , and real $A, B$ . Here $Δ$ is the Laplacian, and $∣ x ∣$ is distance from the origin. The main result excludes strictly positive entire solutions whenever $\frac{n + A}{p + 1} + \frac{n + B}{q + 1} > n - 2$ . Solutions are required to be continuous at the origin and classical elsewhere; no symmetry, growth bound, or other condition at infinity is assumed. Setting $A = B = 0$ gives the unweighted Lane–Emden case.

The source presents this as a resolution of the subcritical Hénon–Lane–Emden conjecture. For $n \geq 3$ and $A, B > - 2$ , it combines the nonexistence result with the radial existence theorem of Bidaut-Véron and Giacomini: a positive radial entire solution exists whenever the strict inequality fails. Thus, under these additional hypotheses, existence holds exactly when $\frac{n + A}{p + 1} + \frac{n + B}{q + 1} \leq n - 2$ . The manuscript describes this combination as settling Phan’s Conjecture C in full.

The supplied abstract does not describe the method establishing nonexistence, so an account of its argument cannot be given from this source. The logical combination behind the exact criterion is explicit: nonexistence on one side of the threshold and known radial existence on the other. Only the main manuscript is supplied, with no companion manuscripts described. The main result has a Lean formalization; the source does not specify whether the cited existence theorem or the combined criterion is also covered.

Useful notions

Powers and inequalities
Functions on multidimensional space
Second derivatives and the Laplacian
Continuity and classical solutions
Radial symmetry

What was known before / what is new

Before

The source cites a radial existence theorem of Bidaut-Véron and Giacomini. For $n \geq 3$ and $A, B > - 2$ , it supplies positive radial entire solutions whenever the strict subcritical inequality fails. The abstract identifies Phan’s Conjecture C as the conjecture settled by combining that theorem with the new nonexistence result.

New

The main result establishes subcritical nonexistence for every $n \geq 2$ , all positive powers $p, q$ , and all real weight exponents $A, B$ . It requires only continuity at the origin and classical satisfaction of the equations elsewhere, without symmetry or a condition at infinity. This main result has a Lean formalization.

Limits and assumptions

Nonexistence requires the strict inequality stated above and applies to strictly positive entire solutions with the specified regularity. The exact existence criterion is stated only for $n \geq 3$ and $A, B > - 2$ ; the source does not give a corresponding full classification outside that range. Equality is covered by the cited existence statement within that range, not by the subcritical nonexistence theorem. The main result is Lean-formalized, but the supplied text does not detail the formalization’s coverage of other claims. It identifies no further open problems and provides no argument details.

Mini glossary

Entire solution: A solution defined throughout all of the ambient space, with the specified regularity at and away from the origin.
Laplacian: The differential operator obtained by adding a function’s second derivatives in each coordinate direction.
Classical solution: A solution with sufficient differentiability to satisfy the differential equations point by point.
Radial solution: A solution whose values depend only on distance from the origin.
Subcritical: Here, the parameter regime in which $(n + A) / (p + 1) + (n + B) / (q + 1) > n - 2$ .
Weight: A position-dependent multiplier, here $∣ x ∣^{A}$ or $∣ x ∣^{B}$ , in one of the equations.

Keywords : Lane–Emden · Hénon–Lane–Emden · Subcritical nonexistence

AI-generated explanation based on the manuscript. Unofficial. Refer to the manuscript for the authoritative version.

3 · Technical details and sources

Claim made in the manuscript (source text)

Resolves the subcritical Lane–Emden conjecture and its weighted Hénon extension. For n ≥ 2, $p, q > 0$ and real A, B, the system $- Δ u = ∣ x ∣^{A} v^{p}$ , $- Δ v = ∣ x ∣^{B} u^{q}$ has no positive entire solution when $(n + A) / (p + 1) + (n + B) / (q + 1) > n - 2$ , with solutions continuous at the origin and classical elsewhere. No symmetry or growth assumption is needed. Known radial existence gives the exact existence criterion for n ≥ 3 and $A, B > - 2$ .

Verified by Lean: the Lean software checked the part of the reasoning described below, sometimes only part of the manuscript. This does not mean independent mathematicians have validated the result.

Scope of the Lean formalization (source text)

…

lean/docs/370.md

Manuscripts in this family

★

The Subcritical Hénon–Lane–Emden Conjecture

24/09/2026

Verified by Lean

We prove the subcritical Hénon–Lane–Emden conjecture: for every dimension n ≥ 2, positive powers p, q, and real weights A, B, the system has no strictly positive entire solution when $(n + A) / (p + 1) + (n + B) / (q + 1) > n - 2$ . Solutions need only be continuous at the origin and classical elsewhere, without a condition at infinity. For n ≥ 3 and $A, B > - 2$ , combining this result with the radial existence theorem of Bidaut-Véron and Giacomini proves Phan's Conjecture C in full: a positive radial entire solution exists whenever the strict inequality fails.

PDF GitHub folder Lean formalization