we-solve (beta)

Math-2652 · mathematics · Geometry

Analytic path selection at several exponential ends

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Consider finitely many real holomorphic functions of real lengths $L_{1},\dots ,L_m$ and parameters z near a finite real $z_{0}$. Require bounded holomorphic extension to products Re $L>A$, |Im $L|<c(Re$ $L)^{2}$; recursively discrete nonnegative exponential-power expansions in each length with finite polynomial factors, strictly better exponential remainders at every cutoff, common tail holomorphy domains for all coefficients, and locally finite grouped weights on positive linear-rate specializations. If a finite Boolean combination of sign/equality conditions holds on a sequence with every $L_i\to \infty $ and $z\to z_{0}$, must it hold eventually on one real analytic path with the same limits and eventually monotone or constant coordinates? Additional finite lists may also be required monotone and prescribed finite function limits retained.

Short English statement

Consider finitely many real holomorphic functions of real lengths $L_{1},\dots ,L_m$ and parameters z near a finite real $z_{0}$. Require bounded holomorphic extension to products Re $L>A$, |Im $L|<c(Re$ $L)^{2}$; recursively discrete nonnegative exponential-power expansions in each length with finite polynomial factors, strictly better exponential remainders at every cutoff, common tail holomorphy domains for all coefficients, and locally finite grouped weights on positive linear-rate specializations. If a finite Boolean combination of sign/equality conditions holds on a sequence with every $L_i\to \infty $ and $z\to z_{0}$, must it hold eventually on one real analytic path with the same limits and eventually monotone or constant coordinates? Additional finite lists may also be required monotone and prescribed finite function limits retained.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2652

The linked path-selection theorem uses the same bounded holomorphic domains, recursive expansions, grouped-weight conditions and remainder estimates specified in this question. It supplies the real-analytic path with the requested limits, eventual sign conditions and monotonicity. The paper also applies this theorem to degenerating Ricci-flat trees, but the path-selection assertion is the result matched here.

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

Go to contribution →