The h₄ inequality behind Hunter's conjecture: an exact real relaxation, two errata, and the real-exponent conjecture of Brazitikos and Pandis

(H4Δ) Σ_cyc (dᵢ+2)²(dᵢ+dⱼ-dₖ)(dᵢ+dₖ-dⱼ) ≥ 0 for every (d₁,d₂,d₃) ∈ ℕ³, by a single sorted substitution whose two branches have non-negative integer coefficients

(H4Δ) is a lattice statement: it fails over ℝ³_(≥0) at (1/2,0,0), where F = -7/16, and the failure is located in the source's own d₃=0 branch factor (d₁+d₂)²+4(d₁+d₂)-4

CORRECTION to arXiv:2512.12254 Proposition 3.1: the printed rewriting of the first sum in the dᵢ ≥ 2 branch is -15 at (5,4,0) and -2117 at (20,19,2) where it is asserted ≥ 0; replacing one (d₁-d₂) by (d₁-d₃) makes it an exact identity, non-negative over the reals under d₁ ≥ d₂ ≥ d₃ ≥ 0

CORRECTION to arXiv:2512.12254 Proposition 3.1: the d₃ = 1 branch display is not an identity — it differs from F(d₁,d₂,1) by (d₁-d₂)²(d₁+d₂) - 1 (at (2,1,1): 64 against a printed 62); the repaired grouping doubles the middle term and drops one +1

The source's "after collecting the same terms" identity is CORRECT under the convention that Σ runs over the distinct index permutations (six ordered pairs on the left, three unordered on the right); a uniform cyclic reading makes it false at (3,2,2) (2 vs 4) and (4,3,2) (-4 vs 26). Under the same convention the whole three-sum splitting of Proposition 3.1 is an identity

The source's (LC) identity (d₂+2)²(d₂+d₃-d₁) + (d₁+2)²(d₁+d₃-d₂) = (d₁-d₂)²(d₁+d₂+4) + d₃((d₂+2)²+(d₁+2)²) and its consequence ≥ 0 for real d₁,d₂,d₃ ≥ 0

Controls for the h₄ family: F vanishes at (0,0,0) and (1,1,0) so 0 ≤ F cannot be improved to 1 ≤ F; and the shift 2 in (dᵢ+2)² is load-bearing — with shift 3 the lattice statement already fails at (1,0,0), where the value is -2

The step a² + b² ≥ 2/n asserted without proof in arXiv:2512.12254 Theorem 3.3, proved in a weighted real form: u ≥ v ≥ w ≥ 0, γᵢ > 0 real, γ₁ ≤ γ₂+γ₃, γ₁u+γ₂v+γ₃w = 1 ⟹ u+v ≥ 2/(γ₁+γ₂+γ₃)

Controls for BR8: dropping γ₁ ≤ γ₂+γ₃ breaks it at γ=(4,1,1), (u,v,w)=(1/4,0,0); dropping w ≤ v breaks it at γ=(1,1,1), (1/2,0,1/2); and 2/n is best possible, with equality at γ=(1,1,1), u=v=w=1/3

The algebra of arXiv:2512.12254 Proposition 4.10: g(1) = 0; the substitution x = eᵗ; and the exponential-sum coefficients A(1,q) = A(2,q) = 0, A(3,q) = q(q+1)(q-4) — the source's g"'(1) — with A(3,q) > 0 ⟺ q > 4 for q > 0

The source's unqualified "the numerator g has five sign changes in its coefficients" needs q > 2: ordered by exponent the sign vector is +,-,+,-,+,- (five changes) for q > 2 and +,-,-,+,+,- (three) for 1 < q < 2

The exact real relaxation of (H4Δ): for real d₁,d₂,d₃ ≥ 0, d₁+d₂+d₃ ≥ 2√2-2 implies F(d) ≥ 0, and the constant is sharp (F(t,0,0) = t²(t²+4t-4) < 0 for 0 < t < 2√2-2); certificate F = x²(s²+4s-4) + z·K with K a sum of four non-negative brackets, plus F = x²(x²+4x-4) + M above the threshold

Controls for BR12: the threshold hypothesis is necessary ((1/2,0,0) has s²+4s = 9/4 < 4 and F = -7/16), the conclusion cannot be strengthened to 0 < F (F(1,1,0) = 0 with the threshold met), and the constant cannot be raised (F(9/10,0,0) > 0 > F(8/10,0,0), bracketing 2√2-2)

E-A (the strategy journal's kill test) PASSES: Claim A's sign-change half holds on 14,713 exact-rational (γ₁,γ₂,q) cases with m = γ₁+γ₂ ≤ 24 (11,401 of them with q > 2), 0 deviations; its coefficient half holds symbolically in q for all 435 families with m ≤ 30, with deg P = m and deg Q = γ₂+1 exactly

Conjecture 1 of arXiv:2512.12254 holds for every n and every real q ∈ [0,5] (Borell log-concavity of Gₐ, Gₐ(0)=1, and the source's integer Theorem 4.4 at k=5, using minⱼ ρ(j,q)/Γ(1+q) ≡ 1 for q ≤ q* = 5.3197223558…)

Two-value reduction for real exponents: for p > 2, every minimiser of a ↦ E(Σ aᵢXᵢ)ᵖ on Sⁿ⁻¹ ∩ ℝⁿ₊ takes at most two distinct values on its support

CONDITIONAL on Claims A and B: Conjecture 1 holds for every n and every real q > n+2, hence (with BR15) for all real q when n ≤ 3; the residual for each n is the compact window q ∈ (5, n+2]

Mathlib gaps priced for this family: Borell's log-concavity of q ↦ E S^q/Γ(1+q) and Descartes–Laguerre for real-exponent generalised polynomials are both absent and both load-bearing; the residual window q ∈ (5, n+2] was deliberately not priced and no work was started on it

CORRECTION to row BR18: Descartes' rule of signs is in the pinned Mathlib (Mathlib/Algebra/Polynomial/RuleOfSigns.lean, Polynomial.roots_countPₚosₗeₛignVariations, roots counted with multiplicity); only the Laguerre extension to real exponents is absent, and row BR20 shows it is not needed. Adds the term-count bound signVariations P ≤ #P.support − 1, which Mathlib does not have

Descartes' rule of signs for generalised polynomials with rational exponents: if (n i: ℚ) = b(e i − e₀) are distinct naturals, b ≠ 0, and some c i ≠ 0, then every finite set of zeros of x ↦ Σ_(i<k) c i x^(e i) in (0,∞) has at most k − 1 elements

The critical-point relations E[(S+uE)^(q−1)] = u·E S^q for each block value u, E S^q = (q−1)E(S+αE+βE′)^(q−2), E(S+αE+βE′)^(q−1) = (q−1)(α+β)E(S+αE+βE′)^(q−2), and the Ψ-recursion Ψ_(γ₁,γ₂)(x;q) = log(q−1) + ((q−2)/2)log(1+c) + Ψ_(γ₁+1,γ₂+1)(x;q−2) at interior critical points

Window census at ten times the earlier q-resolution: 4686 cells of q ∈ (5, m+2], 4 ≤ m ≤ 8, q step 0.01, 200-node quadrature — 0 violations of Conjecture 4.8, Ψ' has exactly 1 or 3 zeros (1: 3674, 3: 1012), worst interior margin +0.40657 at (γ₁,γ₂,q) = (1,3,5.99); the inequality is tight only in the limit x → 0, for the family whose γ₂ is the argmin of ρ(·,q) (worst grid value +1.9e−07 at (2,2), q = 5.32)

(ES): E Sₐ^q ≥ ρ(1/maxᵢ aᵢ², q) for two-block a and q ∈ (5, m+2] — 1,411,410 points, 0 failures, equality at x ∈ 0,1,∞; implies E Sₐ^q ≥ 0.9446·min_(j≤n) ρ(j,q) throughout the window for every n; window-specific (first failures at q ≈ 11.25 for (1,3), q ≈ 12.25 for (2,2))

Two refuted routes for the window: "no extra critical points when q < m+2" (false — interior local minima in 2736 of 13,125 cells, independently 1012 of 4686 in the finer re-run) and the q ↦ q−2 induction with an endpoint bound (fails at 3752 of 3752 interior critical points, worst deficit −2.615)

The two open n = 4 window families instantiated at q = 27/4: the generalised polynomials with exponents 0,1,2,3,4,q+2,q+3,q+4 (split (γ₁,γ₂) = (1,3)) and 0,1,2,3,q+1,q+2,q+3,q+4 (split (2,2)) have at most 7 = m+3 zeros in (0,∞)

Claim A / A′ is dispensable: row BR17's Descartes step consumes only the *term count* m+4 of the critical-point numerator (γ₁+2 exponents in q−1+[γ₂, m+1] and γ₂+2 in [0, γ₂+1]), never the sign pattern, so #positive zeros of N ≤ m+3 holds unconditionally for rational q, and BR17 is conditional on Claim B alone

Controls for BR20: the bound #S + 1 ≤ k is attained (−1 + x vanishes at x = 1); dropping "some coefficient is nonzero" breaks it (c ≡ 0, S = 1,2); dropping distinctness of the exponents breaks it (x⁰ − x⁰ ≡ 0, S = 1,2,3)

Claim B in exact rational arithmetic: ordₓ₌₁ I = m−1, Ψ′(1) = 0 and Ψ″(1) = qγ₁γ₂(q−m−2)/(m²(m+1)) hold exactly in 126 cases — 14 splits (γ₁,γ₂) with m ≤ 10, each at 9 rationals q including q = m+2 (both sides 0, the excluded case) and q = 1/3 (outside the window)