PaperlayerView exact revision on arXiv

Source-linked AI summary

Exact rational certificates and a Lean formalization of the eleven-variable Vasc inequality

Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao

arXiv:2610.13463v1cs.SC

TL;DR

The paper proves nonnegativity of the cyclic Vasc sum for every strictly positive real eleven-tuple. It reduces the inequality to two polynomial sign conditions, certifies them exactly, and formally connects the certificates to the result in Lean; the verification relies in part on native evaluation/compiler mechanisms.

  • Problem

    The paper addresses whether the cyclic Vasc sum is nonnegative for every strictly positive real eleven-tuple.

    Source: §1 · p. 1

  • Method

    The proof uses exact polynomial certificates for a common-translation derivative and a boundary-face condition, then formalizes their connection to the inequality in Lean.

    Source: §1 · p. 1, §1.1 · p. 2

  • Results

    For every strictly positive real eleven-tuple, the Vasc inequality holds: C11(x) ≥ 0.

    Source: §1 · p. 1, §5.2 · p. 6

  • Takeaways & Limitations

    The proof supplies an explicit certificate-based route from finite algebraic checks to the real-valued inequality.

    Source: §9 · p. 10

    The formal result trusts the native evaluation/compiler mechanism as well as the Lean kernel and base axiom system.

    Source: §7.3 · p. 9

Abstract

from arXiv · show

We prove that the cyclic sum $\sum_{i=0}^{10}(x_i-x_{i+1})/(x_{i+1}+x_{i+2})$ is nonnegative for every strictly positive real eleven-tuple, with indices taken modulo eleven. Clearing denominators reduces the problem to a homogeneous polynomial. Subtracting the smallest coordinate then separates the proof into nonnegativity of a common-translation derivative and nonnegativity on a full boundary face. We supply exact rational polynomial certificates in Gram-matrix form for both statements. The derivative certificate uses a linear multiplier, centered monomials and cyclic averaging; the boundary certificate uses a strictly positive quadratic multiplier and uncentered monomials. Their verification requires 6,069 cyclic coefficient comparisons and 34,304 literal coefficient comparisons. All 606 certificate matrices are certified by integer congruences with strictly diagonally dominant images. A Lean 4 development formally verifies the certificate checks and their connection to the original inequality. The exact certificate data, replay programs, and formal sources are publicly available.

1 Introduction

The paper proves the eleven-variable Vasc inequality for positive real inputs using two exact rational polynomial certificates and a Lean formalization. It organizes the proof around a translation derivative and a boundary-face condition, distinct from the independently developed approach to the same case.

1 Introduction

  • For every strictly positive real eleven-tuple, the cyclic Vasc inequality satisfies C11(x) ≥ 0.The coordinates may have arbitrary order and ratios.Source: §1 · p. 1
  • Subtracting the minimum coordinate reduces the proof to a boundary-face polynomial condition and a derivative condition along common translations.The derivative controls the return from the boundary face to the original tuple.Source: §1 · p. 1
  • The derivative certificate uses centered monomials, a linear multiplier, and cyclic averaging, while the boundary certificate uses ordinary monomials and a quadratic multiplier.Both certificates are checked through finite integer coefficient equalities and strict integer inequalities.Source: §1 · p. 1
  • The Lean development verifies the certificate checks and their connection to the theorem, with large finite computations using native_decide.The stated trust boundary includes the native evaluation/compiler mechanism.Source: §1 · p. 2

1.1 Related work and contribution

  • Xu and Yu independently proved the eleven-variable case using rank regions, cumulative gaps, positivity circuits, and subdivision covers; this proof instead uses two global sign conditions and weighted Gram identities.The paper also formalizes the certificate checks and analytic connection in Lean.Source: §1.1 · p. 2
  • The construction addresses this inequality, while multiplier optimality, certificate minimality, and equality classification remain outside its scope.Reported replay timings were measured in one recorded environment.Source: §1.1 · p. 2

2 Reduction to two polynomial sign conditions

The reduction clears denominators to obtain a polynomial, then proves its nonnegativity by combining a boundary-face condition with a common-translation derivative condition. Subtracting the minimum coordinate places the tuple on the boundary, and integrating the derivative recovers the result for the original tuple.

2 Reduction to two polynomial sign conditions

  • The polynomials P, H, and B have degrees eleven, ten, and eleven, respectively; defining B requires no rational summand at a vanishing denominator.B is the boundary restriction P(z0, . . . , z9, 0).Source: §2 · p. 2
  • For positive tuples, D(x)>0, so P(x) ≥ 0 implies C11(x) ≥ 0 after clearing denominators.The polynomial relation is P(x)=D(x)C11(x).Source: §2 · p. 3
  • Subtracting the minimum coordinate gives y=x−t1 with nonnegative coordinates and at least one zero, which cyclic invariance places on the face x10=0.The boundary condition then gives P(y) ≥ 0.Source: §2 · p. 3
  • Integrating the polynomial derivative along y+s1 from s=0 to s=t transfers nonnegativity at the boundary point to P(x) ≥ 0.The translated coordinates remain nonnegative over this interval.Source: §2 · p. 3
  • The boundary certificate covers the entire closed face, including further subfaces where several coordinates attain the minimum.Positivity of the original denominators is used only after returning to the positive tuple.Source: §2 · p. 3

3 An exact certificate language

The paper represents polynomial certificates as nonnegative monomial factors times quadratic forms, reducing sign verification to matrix checks. Integer congruences with strictly diagonally dominant images certify positive definiteness exactly.

3 An exact certificate language

  • A certificate term pairs a nonnegative monomial factor with a quadratic form, so its sign follows from the quadratic form's sign.The vector contains monomials or monomial differences, and the matrix is rational and symmetric.Source: §3 · p. 3

3.1 Triangular polynomial coordinates

  • Triangular coordinates store the quadratic polynomial's coefficients, with off-diagonal coordinates doubled relative to the corresponding matrix entries.Entries are read in increasing column order, then increasing row order.Source: §3.1 · p. 3

3.2 Integer congruence certificates

  • An integer congruence whose image is strictly diagonally dominant certifies that the rational matrix is positive definite.Strict diagonal dominance gives positive definiteness of the image and invertibility of the congruence matrix.Source: §3.2 · p. 4

4 The common-translation certificate

The common-translation derivative is certified with centered monomial vectors and cyclic coefficient checks. Exact matrix and coefficient verification establishes the polynomial identity and the derivative's nonnegativity on the closed orthant.

4.1 Cyclic coefficient comparison

  • Centered vectors form the basis of the derivative certificate, whose coefficients are checked using cyclic orbit representatives.The check covers 6,069 representatives and verifies exact agreement for every listed orbit.Source: §4 · p. 4, §4.1 · p. 5

4 The common-translation certificate

  • All 93 derivative-certificate matrices are positive definite, verified through 5,975 strict integer row inequalities.Their dimensions sum to 5,975, with maximum dimension 184.Source: §4 · p. 4

4.2 The derivative sign on the closed orthant

  • The cyclic coefficient comparisons establish the certificate identity, and nonnegative monomial factors and quadratic forms give the derivative's nonnegativity on the closed orthant.For nonzero x, the positive linear multiplier permits division; the derivative polynomial vanishes at the origin.Source: §4.1 · p. 5, §4.2 · p. 5

5 The full boundary certificate

The boundary proof uses a certificate in ten nonnegative variables and verifies its matrix and polynomial coefficients exactly. Its strictly positive multiplier yields nonnegativity across the full closed face, including points with additional zero coordinates.

5 The full boundary certificate

  • The boundary certificate uses ten nonnegative variables and 55 quadratic monomials, with positive integer weights.The smallest weight numerator is 45,839,617,787.Source: §5 · p. 5
  • The 513 boundary matrices are positive definite, certified by 34,314 strict integer row inequalities.The 513 comprise the multiplier matrix and 512 Gram blocks.Source: §5 · p. 6

5.1 Literal coefficient comparison

  • The boundary polynomial is expanded directly and matches the certificate at all 34,304 listed degree-thirteen exponents.The literal coefficient check includes zero rows and requires no orbit representatives or stabilizer factors.Source: §5.1 · p. 6

5.2 Strict positivity of the multiplier

  • The multiplier is strictly positive at every nonzero point of the closed orthant, so dividing the nonnegative certificate product proves the boundary polynomial is nonnegative.At the origin, the degree-eleven polynomial vanishes.Source: §5.2 · p. 6
  • The boundary proof also covers points with additional zero coordinates, and together with the derivative condition it proves the original inequality for every positive tuple.The two sign conditions are certified independently.Source: §5.2 · p. 6

6 Construction and finite verification

The construction turns numerical Gram-matrix candidates into exact rational certificates, then verifies their polynomial identities and matrix conditions through finite checks. The derivative and boundary certificates use different representations, while sharing exact integer checking conventions.

6 Construction and finite verification

  • The six certificate arrays encode monomial frames, rational matrices, and integer congruences; their interpretation is fixed, so verification needs no numerical optimization.The same matrix test, coordinate convention, and integer coefficient arithmetic are used for both certificates.Source: §6 · p. 7, §6.2 · p. 8

6.1 From numerical candidates to exact data

  • Numerical Gram candidates are reconstructed and repaired over the rationals, with separate routines tailored to the derivative and boundary coefficient structures.The boundary multiplier combines a positive-coefficient quadratic part with a positive-semidefinite quadratic-form part; the recorded correction changes any Gram numerator by at most two units.Source: §6.1 · p. 7
  • Integer congruences certify strict row inequalities for the matrices; replay tests these conditions exactly rather than relying on approximate positivity.The congruence matrices are constructed using floating-point approximations, but are tested against the exact integral matrices; replay requires no Cholesky factorization.Source: §6.1 · p. 7

6.2 A complete checking procedure

  • The checker validates frames, matrices, multiplier conditions, and polynomial identities, including all 34,304 literal coefficient equalities for the boundary certificate.For the derivative, it expands centered Gram coordinates and checks cyclic representatives; the boundary check retains the literal ten-variable polynomial.Source: §6.2 · pp. 7–8
  • Support coverage and exhaustive checks ensure every generated term and every finite array, matrix row, and coefficient set is checked.Coefficient arithmetic is integral after multiplication by the specified denominators.Source: §6.2 · p. 7

7 Formalization in Lean

The Lean development links the finite certificate checks to the real-valued Vasc inequality, whose exported theorem assumes only strict positivity of the coordinates. Its staged formalization covers matrix and polynomial checks, certificate identities, and the analytic argument, while its large finite checks rely on native evaluation.

7 Formalization in Lean

  • The exported Lean theorem states the Vasc inequality for 11 real coordinates and requires only that every coordinate be strictly positive.Certificate, derivative, and boundary assumptions are discharged in intermediate interfaces.Source: §7 · p. 8

7.1 Semantic layers

  • The matrix layer proves that checked integer congruences imply nonnegativity of the associated real quadratic forms.It also handles array sizes and triangular polynomial coefficients, using a strict diagonal-dominance implication.Source: §7.1 · p. 8
  • The sparse-polynomial layer normalizes exponent-coefficient lists, and its soundness results connect successful equality checks to equal real evaluations.Normalization sorts exponents, combines equal exponents, and removes zero coefficients.Source: §7.1 · p. 8
  • Polynomial interfaces connect the certificate expressions to the article’s target polynomials, including denominator factors and the boundary substitution.The targets incorporate defining differences and excluded-index products.Source: §7.1 · p. 8
  • The analytic assembly formalizes cyclic invariance, minimum-coordinate subtraction, face nonnegativity, common-translation monotonicity, and clearing positive denominators.Monotonicity from a nonnegative derivative supplies the comparison used in the article’s polynomial integration argument.Source: §7.1 · p. 8

7.2 Checked caches and staged composition

  • Staged checks combine verified Gram-block expansions, target factors, matrix checks, and aggregate identities to establish the required real sign statement.Caches organize computation; the derivative’s cyclic rotations are included before the final equality comparison.Source: §7.2 · p. 9
  • Lean recomputes certificate conditions from checked-in source data, so compilation does not depend on the original Python optimizer or replay report.Provenance manifests record the JSON-to-Lean conversion, but the converters are not runtime dependencies.Source: §7.2 · p. 9

7.3 Trust boundary

  • Large finite checks use native_decide, so the result trusts native evaluation/compiler mechanisms in addition to Lean’s kernel and base axioms.The dependency audit reports 1,215 generated nativecomputation axioms and no sorryAx dependency or unrelated custom axiom; real-valued soundness and analytic assembly are ordinary Lean proofs.Source: §7.3 · p. 9

8 Reproducibility and computational evidence

The materials provide separate entry points for exact certificate replay and the Lean project, with pinned software environments and embedded certificate data. The replay checks completed without resource cutoffs, while the archived build records do not constitute a controlled cold-build benchmark.

8 Reproducibility and computational evidence

  • The reproducibility bundle provides standalone Python replay programs and a Lean project with embedded data, soundness proofs, concrete checks, and the final theorem.The two verification entry points use the same certificate construction but have different software dependencies.Source: §8 · p. 9

8.1 Exact arithmetic replay

  • Exact replay uses CPython and python-flint, and its programs use exact integer and rational arithmetic without a numerical solver or network access.The reported sequential runs verify already constructed certificates, not their discovery or the Lean build, and both completed checks without reaching a resource cutoff.Source: §8.1 · pp. 9–10

8.2 Building the formal project

  • The formal project is pinned to Lean and Mathlib revisions, and its rebuild does not invoke Python, a semidefinite solver, or the original JSON converters.Archived records document a successful full build, but provide no controlled end-to-end cold-build benchmark.Source: §8.2 · p. 10

9 Discussion

The proof organizes the universal inequality around two polynomial sign conditions tied to a common-translation argument. Its exact certificate construction has explicit structural requirements, and the discussion identifies certificate size and verification mechanisms as possible areas for further work.

9 Discussion

  • The proof certifies a translation derivative and a full boundary face; the supplied derivative certificate uses a linear multiplier, while the boundary certificate uses a quadratic multiplier.The boundary multiplier combines positive-coefficient and positive-semidefinite parts.Source: §9 · p. 10
  • The certificate construction requires distinct centered and uncentered Gram expansions, a stabilizer correction for cyclic orbit compression, and a multiplier positive on nonzero boundary subfaces.The congruence test also certifies invertibility of its change of coordinates.Source: §9 · p. 10
  • Further work could reduce finite-data size, compare alternative exact matrix certificates, or replace native evaluation; each change requires new checks of the resulting proof objects.These are presented as possible directions rather than established improvements.Source: §9 · p. 10

Data and software availability

The article provides a prepared repository with exact certificate data, replay programs, and Lean sources. It supports checking the supplied data and formal sources, but not end-to-end regeneration or a verified fresh clean build.

Data and software availability

  • The repository contains finite rational data, a checksum manifest, replay programs, and a Lean project with sources and pinned dependency manifests.Manifests record source-to-certificate provenance.Source: Data and software availability · p. 11
  • The package supports verification of supplied exact data and formal sources, not end-to-end regeneration of the search or formal source files.A fully pinned numerical discovery pipeline and portable JSON-to-Lean converters are not included.Source: Data and software availability · p. 11
  • Selected producer scripts were syntax checked but not rerun during packaging.The package includes selected scripts and an input frame under generation/.Source: Data and software availability · p. 11
  • A fresh clean build of the exported repository was not performed during package preparation.Detailed instructions and the generation inventory are supplied in reproduce.md and generation_inventory.md.Source: Data and software availability · p. 11

Use of AI-assisted tools

The authors report using FL-Prover for the Lean formalization and NL-Prover for the other work, including the informal proof, certificates, literature research, and manuscript preparation.

Use of AI-assisted tools

  • FL-Prover was used for the Lean formalization, while NL-Prover was used for the other work, including the informal proof, computational certificates, literature research, and manuscript preparation.The authors identify the explicit certificates, exact checks, and formal theorem as the mathematical evidence.Source: Use of AI-assisted tools · p. 11
Loading 2610.13463v1…