OpenAI claim summary for Math-2652

Analytic path selection at several exponential ends

OpenAI's claim

For finite admissible families of real-holomorphic functions with the specified exponential expansions, OpenAI claims that sign conditions occurring along a sequence at several infinite length ends also occur along a single real-analytic path. That path has the same limits and eventually monotone or constant coordinates. Additional finite admissible function lists and prescribed finite limits can be retained.

Mathematical statement of the claimed result

Mathematical claim 1.

Let $P_j(L_1,\ldots,L_m,z)$ be finitely many real-holomorphic functions, bounded on products $Q(A,c)=\{L:\operatorname{Re}L>A,\ |\operatorname{Im}L|<c(\operatorname{Re}L)^2\}$ near a finite ordinary-parameter point $z_0$. For each length and recursively extracted coefficient require expansions \[P\sim\sum_{d\in D_i}e^{-dL_i}\sum_{k=0}^{k_d}L_i^kP_{dk}(L_{\widehat i},z),\] where $D_i\subset[0,\infty)$ is locally finite, $k_d<\infty$, $k_0=0$, and removal of terms $d\le B$ leaves $O(e^{-(B+\epsilon_B)\operatorname{Re}L_i})$ with $\epsilon_B>0$ on smaller quadratic regions, uniformly on smaller parameter polydiscs. All recursively expanded coefficients must be holomorphic on one common tail band and ordinary-parameter neighborhood. For any subset $\operatorname{Re}L_i=c_iU+o(U)$, $c_i>0$, require locally finite grouped weights $\sum c_id_i$ and strictly better exponential remainders after every finite cutoff, on the same complex neighborhoods. If a finite Boolean combination of $P_j>0,P_j=0,P_j<0$ holds along $L_i^{(n)}\to+\infty,z^{(n)}\to z_0$, the claim gives a real-analytic path $u\mapsto(L(u),z(u))$ with those limits and the same sign conditions for all large real $u$. Each coordinate, and any additionally prescribed finite admissible list, is eventually monotone or constant; finite prescribed function limits can also be retained. Every extracted coefficient must itself obey each of the preceding requirements: boundedness, expansions in every remaining length, common holomorphic domains, and grouped-weight remainder estimates. One shrinking of the analytic neighborhoods suffices for the finite original family; constants and length thresholds in estimates may vary with the order of truncation.

Outline of the argument

Degenerating Ricci-flat tree inequality: Power-logarithmic expansions in exponential neck variables are kept with recursively compatible remainder estimates, rather than assumed to be convergent analytic series. A path-selection argument realizes finite sign conditions and prescribed limits along analytic paths in ordinary parameters. Applying this to the finite tree’s asymptotic geometry converts a failing elliptic estimate into an impossible selected path.

Formal verification

Degenerating Ricci-flat tree inequality: The pinned catalogue lists no Lean formalization for this result.

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

• OpenAI, Path selection and an elliptic inequality on degenerating Ricci-flat trees, 2026-09-24; citation key OAI:Path-selection-and-an-elliptic-inequality-on-degenerating-Ricci-flat-trees-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:path-selection.
• OpenAI catalogue entry.