This repo contains AI generated proofs which may contain errors. To trust the claimed main result, and for it to be meaningful to have Lean check the actual proofs you must read, understand, and validate the content of Definitions.lean.

A Lean 4 formalization proving that symmetric log-concave functions on weak compositions are maximized on balanced vectors and minimized on concentrated vectors. This is a refactoring of Johannes Schmitt's balanced-vectors-blueprint, which formalized a proof discovered by GPT-5 for an open problem about psi-class integrals on moduli spaces of curves.

For any function D : WeakComposition n d → ℚ that is:

• Strictly positive
• Symmetric under permutations of indices
• Log-concave (satisfies D(e)² ≥ D(e⁺) · D(e⁻) for adjacent modifications)

There exist:

• A balanced vector b (entries differ by at most 1) maximizing D
• A concentrated vector c (all mass at one position) minimizing D

BalancedVectors.lean           -- Public API (imports ProofOfMainTheorem)
BalancedVectors/
  Definitions.lean             -- Core definitions (WeakComposition, IsBalanced, etc.)
  MainTheorem.lean             -- Statement: StatementOfTheorem
  ProofOfMainTheorem.lean      -- Proof: mainTheorem
  Proofs/
    helper_lemmas.lean         -- Supporting lemmas

The public API exposes exactly two declarations:

• StatementOfTheorem : Prop
• mainTheorem : StatementOfTheorem

API documentation is automatically generated and available at: https://e-vergo.github.io/Balanced_Vectors/docs/BalancedVectors/

lake exe cache get  # download Mathlib cache
lake build

Apache 2.0