The Miró-Roig–Tran Strict-Sign Conjecture

Abstract

The literal Miró-Roig–Tran alternating integer coefficient is strictly negative for every natural n at least two.

The source conjecture appears immediately after Proposition 3.12. Its quantifier is every n>=2. The separate n>=4 assumption in Proposition 3.12(c) governs a preceding weak-Lefschetz implication and does not restrict the displayed conjecture. The formal target is the coefficient itself: no monotonicity suggestion, WLP consequence, bounded check, or non-strict proxy is substituted.

Definition 1.1 (The literal alternating integer coefficient).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ \mathrm{coefficient}\left(n\right)=\sum _{0\le k\le n}{\left(-1\right)}^k\times \mathrm{binom}\left(2n+2,k\right)\times {\left(2n^2-1-\left(2n-1\right)k\right)}^{2n-1}\\ \mathrm{coefficient}\left(n\right)\in \mathbb{Z}.\end{array}$$

Formalization. D5/S3/Combinatorics/Splines/MiroRoigTranStrictSign.coefficient (✓ std3).

Citation. Rosa M. Miró-Roig and Quang Hoa Tran (2020). On the weak Lefschetz property for almost complete intersections generated by uniform powers of general linear forms. DOI: 10.1016/j.jalgebra.2019.12.029. URL: https://arxiv.org/abs/2001.06143v1.

Commentary.

For natural n, coefficient(n) is the integer sum over k=0,…,n of (-1)^k binom(2n+2,k) times (2n^2-1-(2n-1)k)^(2n-1). The affine subtraction and exponentiation take place in the integers exactly as in the formal declaration.

Theorem 1.2 (Strict negativity for every n at least two).

$$\begin{array}{r}\forall n\in \mathbb{N},2\le n⟹\\ \mathrm{coefficient}\left(n\right)<0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Splines/MiroRoigTranStrictSign.result (✓ std3). ∎

Resolves. Problems/miro-roig-tran-strict-sign (proved) by D5/S3/Combinatorics/Splines/MiroRoigTranStrictSign.result.

Source. Repository-derived.

Acknowledgement. Rosa M. Miró-Roig and Quang Hoa Tran (2020). On the weak Lefschetz property for almost complete intersections generated by uniform powers of general linear forms. DOI: 10.1016/j.jalgebra.2019.12.029. URL: https://arxiv.org/abs/2001.06143v1.

Commentary.

For every natural n>=2, the literal integer coefficient is strictly negative. In particular n=2 is included; direct evaluation gives coefficient(2)=-26.

The proof sets m=2n+2 and x=(2n^2-1)/(2n-1). Terms with k>n have nonpositive positive-part arguments and vanish. Factoring the positive denominator from the remaining terms yields the exact normalization

$\mathrm{real}\left(\mathrm{coefficient}\left(n\right)\right)={\left(2n-1\right)}^{2n-1}\times \left(2n-1\right)!\times C\left(2n+2,\frac{2n^2-1}{2n-1}\right)$

where C is the normalized finite positive-part curvature from the recurrence owner. Since n>=2, m>=6 and x lies in the closed core [s_m,m-s_m]. The strict-curvature theorem therefore makes C_m(x) negative, while both scale factors are positive. For n=2 the point is x=7/3, the left closed-core endpoint of C_6, so endpoint strictness is essential. Casting the resulting real inequality back to the integers proves the stated sign.

References

• Truth anchor: D5/S3/Combinatorics/Splines/MiroRoigTranStrictSign.coefficient
• Truth anchor: D5/S3/Combinatorics/Splines/MiroRoigTranStrictSign.result
• Dependency: D5/S3/Analytic/Curvature/CardinalSplineStrictCurvature