Metadata

slug: ggps2025
bibkey: garrappa2025mittagmodulus
doi: null
triage: theorem
motivation_gids:
  - D5/S3/Analytic/Asymptotics/MittagLefflerModulusRefutation.result
url: https://arxiv.org/abs/2410.11852v4

The reverse Mittag-Leffler modulus characterization is false

Problem

Garrappa, Gerhold, Popolizio and Simon, On some inequalities for the two-parameter Mittag-Leffler function in the complex plane, arXiv:2410.11852v4, p. 18, Conjecture 25 (journal DOI 10.1016/j.jmaa.2025.129588):

For every α ∈ (1, 2), one has The inequality (1.4) holds globally ⇐⇒ β ∈ [α − 1, α] ⇐⇒ 1/Eα,β(x) is CM on (0, ∞).

Here $β \geq 0$ , and (1.4) is $∣ E_{α, β} (z) ∣ \geq E_{α, β} (Re z)$ for every $z \in C$ . Equation (1.1), p. 1, defines $E_{α, β} (z) = \sum_{k = 0}^{\infty} z^{k} /Γ (α k + β)$ for $α > 0$ and every real $β$ . The reciprocal Gamma value at a pole is zero. Complete monotonicity means a smooth positive-valued function on $(0, \infty)$ whose signed derivatives of all natural orders are nonnegative.

Statement echo

Unqualified Lean names below belong to D5.S3.Analytic.Asymptotics.MittagLefflerModulusRefutation.

Source clause	Lean counterpart	Fidelity
Equation (1.1), all positive $α$ , real $β$ , complex $z$	`IsSourceSeries`	`HasSum` includes convergence; Gamma and ordinary complex division are Mathlib’s.
$1/ E_{α, β} (x)$	`reciprocal`	The real argument is embedded in $C$ and the real part reads the real series value.
Global inequality	First equivalence in `claim`	Every complex argument is quantified; its real part is embedded without rescaling.
$1 < α < 2$ , $β \geq 0$ , $α - 1 \leq β \leq α$	Parameter binders and interval in `claim`	Both endpoints and all domain restrictions are literal.
Positive smooth reciprocal with signed derivatives	Second equivalence in `claim`	Existing `D5.S3.Analytic.ExpRatioCM.Defs.CompletelyMonotoneOn` is used, with a separate positivity conjunct.
Existence of the source family	Leading existential in `claim`	Explicit convergence/existence requirement; it does not weaken the universal conjecture.
Negative answer	`result`	Exactly the negation of the complete claim.

Motivation

The settling declaration is D5/S3/Analytic/Asymptotics/MittagLefflerModulusRefutation.result. Its source note is D5/L/AnalyticClosure/garrappa2025mittagmodulus. A strict deficit at one nonreal argument disproves the claimed global lower bound even when the parameter interval holds.

Gap

The original finite certificate refutes the parameter-interval implication at $(α, β) = (3/2, 1/2)$ . The analytic extension now contains an uncompiled source proof route for every $1 < α < 2$ and a closed interval of beta values at the same finite nonreal point. This extension has no native elaboration, axiom-closure, admission or preregistration #22376 completion certificate.

Route

For each $1 < α < 2$ , set $η = π (2 - α) /4$ , $t = tan η$ and $w = - 1 + i t$ . The literal source series is identified with the Barnes integral on the one-half line using actual residues, horizontal decay and the moving-left limit. Shifting right through one and two gives $E_{α, α - 1} (z) = c_{α} / z^{2} + R (z)$ , where $c_{α} = α (α - 1) (α + 1) /Γ (2 - α) > 0$ . The first reciprocal-Gamma coefficient is zero. The actual five-halves-line integral bounds $R (r w)$ by a fixed constant times $r^{- 5/2}$ .

Consequently the scaled negative-axis real part tends to $c_{α}$ and the scaled ray norm tends to $c_{α} / (1 + t^{2})$ . Their strict gap supplies one finite positive radius $r$ . Only after choosing $z_{α} = r w$ does beta-continuity supply $0 < ϵ_{α} < 1$ , so that the strict deficit holds at that same point for every beta in the closed interval $[α - 1, α - 1 + ϵ_{α}]$ .

Falsifier

This source route would fail if the literal series identification, contour normalization, residue signs, principal-logarithm scaling, remainder limit, strict finite-radius selection or closed-interval continuity argument failed. No Barnes representation or sector asymptotic is assumed as a hypothesis. All these new Lean proof texts remain uncompiled.

Evidence

source_barnes_identity supplies the actual MBSeriesData and uses residue HasSum followed by the original source HasSum uniqueness. integral_right_step, source_endpoint_expansion, source_endpoint_scaled_limit, ray_parameters and source_endpoint_failure form the source chain into source_closed_beta_family. The current result : ¬ claim body calls this family at alpha=3/2 and beta=1/2. The original IsSourceSeries, claim, all-positive-alpha/all-real-beta/all-complex-z source existence and both global conjecture equivalences retain their full scope.

The original private finite estimates partial_axis, partial_point, tail_geometric, source_partial_bound and certified_failure are retained as inherited finite-instance source. They are no longer called by the current result body. Earlier finite-instance kernel evidence does not validate the new result proof path. The source and consumer mapping is in Library/Asymptotics/braams2026barnesmittagport.md.

Faithful public-target Reg evidence is unfinished in https://github.com/the-omega-institute/trureturing/issues/24571. Native elaboration of the complete inherited and new analytic chain, axiom and live proof-path inspection, faithful Reg bindings, canonical generated-state checks, review and regular PR gates remain outstanding. No source-stage admission, freeze, preregistration completion or merge is claimed.

The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Independent computation

Experiment directory at f1be70a8a80297f44ec7a3d651faf1e622920913. Program: check.py; SHA-256 c6baf5bbab39481e1235752ddd18164291344b7bcfa8a7e11c51fb62a56aa2ff. Command from the lane checkout: python3 .lake/scratch/stageb-ggps2025/check.py, exit 0, ALL_CHECKS_OK. The checked file was extracted from that immutable revision, rather than the experiments checkout’s current file. Exact rational enclosures certify the larger endpoint witnesses $z = r (- 1 + i /2)$ for $r = 1024, 1536, 2048$ ; both parity tails are below $1 0^{- 60}$ . The program also checks the source coefficients through $n = 80$ against the exponential and hyperbolic-sine specializations. It checks finite algebra, not a uniform parameter family or analytic identities. These computations are separate from the kernel certificate at $- 115 + 10 i$ .

Triage

Item	Status and evidence
$B \Rightarrow A$ fails at $(3/2, 1/2)$ ; the characterization is false	Inherited finite-certificate evidence; the current family-based `result` proof text is uncompiled.
The defining series exists for every $α > 0$ and arbitrary real $β$ , including reciprocal-Gamma pole values	Proved, kernel-checked private `source_norm_summable` and `source_exists`, retained in the current source path to `result`; the new path requires native validation.
Both selected arguments have 64-term truncation error at most $4/1 0^{13}$	Proved, kernel-checked private `source_partial_bound`, used at $- 115$ and $- 115 + 10 i$ in `certified_failure`.
Finite rational witness and independent larger endpoint witnesses	Computed: the independent experiment certifies exactly $r = 1024, 1536, 2048$ . The smaller finite witness has a separate kernel certificate in this module; the witness-search report alone is not proof.
All- $α$ family and same-point closed- $β$ neighbourhood	Written as `source_closed_beta_family` and consumed textually by `result`; uncompiled and unadmitted.
$C \Rightarrow B$ and a corrected universal region	Open here. The source reports $A \Rightarrow B$ and $B \Rightarrow C$ as proved; this result targets $B \Rightarrow A$ and does not contest them.
New general Gamma identity, Mittag-Leffler asymptotic expansion, or exhaustive novelty	Open; none is claimed. Literature completeness is ASSUMED-UNVERIFIED.

What the settlement shows

Proved: the failure mechanism is a strict modulus deficit at a parameter pair lying in the proposed closed interval. The source series exists, so the refutation is not a consequence of an empty class of realizations. The inherited finite witness addresses the universal characterization. The new source family additionally addresses an interval extending above each endpoint; its proof text has no native validation in this delivery.

The source’s proved implications $A \Rightarrow B$ and $B \Rightarrow C$ remain compatible with this counterexample. Uses of the equivalence $A \Leftrightarrow B$ cannot retain its false reverse direction; no further consequence or dependency of another source result is asserted here.

Literature reading: #22376 records a bounded screen of the source, author indexes, errata, arXiv searches and related papers. No settlement was identified in the read material. The publisher version of record, complete citation census and several full texts were unavailable; no exhaustive prior-art or novelty claim follows.

ASSUMED-UNVERIFIED

Literature completeness and absence of an earlier external settlement remain ASSUMED-UNVERIFIED. The source is the read arXiv v4 rather than the unread publisher text. The all- $α$ family and closed- $β$ neighbourhood have uncompiled Lean proof texts in this delivery. The sharp corrected parameter region is still open; no native or admission certificate is supplied for the new family.

Keyboard shortcuts

trureturing — Discovering truth