Metadata
slug: grunwald-pales-2024-gini-stationary-test
bibkey: grunwaldpales2024gini
doi: null
url: https://arxiv.org/abs/2408.07658v1
triage: theorem
motivation_gids:
- D5/S3/ArithSums/GiniStationaryTest/Result.result
Stationary characterization of Gini mean comparisons
Problem
R. Grünwald and Zs. Páles, Comparison of Gini means with fixed number of variables, arXiv:2408.07658v1, §4, state:
Conjecture 2. Assume that 0 = inf I · I⁻¹ and let n ≥ 3. Then ((r, s), (p, q)) ∈ Γ_n(I) if and only if, for all u₁, …, u_n ∈ ℝ₊ such that G^{[n]}{r,s}(u₁, …, u_n) = 1, ∃ρ ∈ ℝ such that χ′{p,q}(u_k) + ρχ′{r,s}(u_k) = 0 (k ∈ {1, …, n}) the inequality 1 ≤ G^{[n]}{p,q}(u₁, …, u_n) holds.
Here is a nonempty interval in and consists of the parameter pairs satisfying for every . The stationary test universally quantifies over positive normalized tuples satisfying the common-multiplier equations. It does not assert that every normalized tuple admits such a multiplier.
The formal reading is:
| Source object or condition | Lean encoding and meaning |
|---|---|
| , | n : ℕ, 3 ≤ n, x : Fin n → ℝ, and ∀ i, x i ∈ I |
| Nonempty positive interval | I ⊆ Set.Ioi 0, I.OrdConnected, and I.Nonempty |
sInf ((fun z : ℝ × ℝ => z.1 / z.2) '' (I ×ˢ I)) = 0; the set is precisely , rather than a product of two scalar infima | |
| , | Defs.giniMean delegates to GiniMeanEndpointComparison.giniMean, namely |
, the equal-parameter branch of Defs.giniMean | |
Defs.chi: for , and for | |
Defs.chiDeriv p q t := deriv (Defs.chi p q) t | |
Defs.Gamma n I: comparison for every tuple from | |
| Stationary criterion | Defs.stationaryTest n r s p q: positivity, , and existence of a common real multiplier imply |
| Claimed equivalence | Defs.claim: all the displayed interval conditions, all , and all real |
Motivation
The proposed criterion would certify global comparison on intervals with arbitrarily large coordinate ratios using only interior stationary tuples after normalization. The positive half-line is such an interval, so a failure there refutes the full equivalence.
Gap
The source proves the bounded-interval characterization in Theorem 7 and states Conjectures 1 and 2. Searches for the title, arXiv identifier 2408.07658, DOI 10.1007/s00025-025-02370-0, and the authors with “Conjecture 2”, “counterexample”, or “proof” found no settlement. Grünwald’s 2025 Debrecen–Katowice seminar report (Ann. Math. Sil. 39(2) (2025), 381–394) restates the question. Conjecture 1 of the same paper is refuted in the endpoint comparison dossier. Citation indexes were not checked exhaustively. Interior stationarity alone does not control escape toward the boundary of the positive normalized simplex.
Route
Fix any , take , and choose and . Normalization gives . The characteristic derivatives are
The multiplier equations therefore put every coordinate on one level of . Distinct positive points on that level satisfy , and the level contains at most two positive points. A nonconstant normalized tuple has values . Put and . Each coordinate satisfies and , hence
Since , one has . Thus
Consequently on every nonconstant stationary tuple. The constant normalized tuple has every coordinate one and gives equality. This proves the stationary test.
Falsifier
For , use and . Then
The identity
gives because all denominators are positive and cubing preserves order. In particular, and give and . The pair passes the stationary test but lies outside for every .
Evidence
The theorem D5/S3/ArithSums/GiniStationaryTest/Result.result has the unconditional type ¬ Defs.claim. Its axiom closure is exactly propext, Classical.choice, and Quot.sound.
Its mathematical dependencies are Result.counterexample_family, Stationary.stationaryTest_one_zero_two_negOne, Stationary.chiDeriv_parameters, Witness.not_mem_Gamma, Witness.witness_comparison, and Witness.witness_identity, together with the private stationary level, moment, and finite-sum helpers. The existing unequal-parameter mean and highTuple come from GiniMeanEndpointComparison; real-power, derivative, finite-sum, and conditional-infimum facts come from Mathlib. The family theorem supplies both the stationary criterion and nonmembership for the same and parameters, and result specializes both conjuncts at . The quotient set of equals , whose infimum is zero.
ChatGPT Pro supplied the counterexample route; the Lean evidence supports the first triage item.
Triage
-
PROVED — the stationary characterization fails in every dimension .
Result.counterexample_familyproves that passes the stationary test and is outside .Stationary.stationaryTest_one_zero_two_negOneproves the stationary part for every nonzero dimension.Result.resultrefutes the full universally quantified claim. -
PROVED in prose — every positive parameter scale. Fix and set . For either parameter pair or , and . The positive factor cancels from each multiplier equation, so normalization and stationarity transfer to . The proved stationary criterion and the increasing map give the scaled stationary criterion. Conversely, take for ; the same identity transfers the strict comparison reversal to .
-
PROVED in prose — boundary escape. For , the positive tuple with has mean one. Its objective is , which tends to as . Thus the objective has infimum on the positive normalized simplex, despite being nonnegative at all its stationary tuples.
-
PROVED in prose — comparison implies the stationary criterion. For any admissible and positive tuple , put and . The zero quotient infimum provides with . Set . Every lies between and , hence belongs to by interval connectedness. Comparison on and homogeneity give comparison at for all parameters, including equal parameters. If , the required inequality follows, whether or not is stationary.
-
COMPUTED — a rational three-variable instance. At , the cubed comparison is , equivalently . These exact arithmetic values illustrate the proved family.
-
OPEN — the comparison region. What is a correct characterization of when ?
ASSUMED-UNVERIFIED
The journal version’s text is unverified; the quotation and locators refer to arXiv:2408.07658v1. The literature scope does not establish an exhaustive literature or priority claim.
The positive-scale extension, boundary-escape limit, and general surviving implication are proved in prose above, not in the companion Lean modules. The Lean family fixes parameter scale and covers every .