Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Braun–Bruegge Conjecture 5.1

Abstract

Braun–Bruegge’s symmetric edge-polytope facet-sum conjecture

Definition 1.1 (The facet sum).

Formalization. D5/S3/Combinatorics/BinomialBases/BraunBrueggeFacetSumConjecture.F (✓ std3).

Citation. B. Braun, K. Bruegge (2023). Facets of Symmetric Edge Polytopes for Graphs with Few Edges. URL: https://arxiv.org/abs/2201.13303v4.

Commentary.

Proposition 4.4 states verbatim: “If all the m_i’s have the same parity, N(CB(m)) is given by F(m) = Σ_{j=0}^{m_t} C(m_t, j) [Π_{k=1}^{t−1} C(m_k, (m_k − m_t)/2 + j)].” The displayed Lean expression is its t=3 specialization, with Nat.choose and natural floor division.

Definition 1.2 (The sorted common-parity domain).

Formalization. D5/S3/Combinatorics/BinomialBases/BraunBrueggeFacetSumConjecture.Admissible (✓ std3).

Citation. B. Braun, K. Bruegge (2023). Facets of Symmetric Edge Polytopes for Graphs with Few Edges. URL: https://arxiv.org/abs/2201.13303v4.

Commentary.

The source orders the entries so that a≥b≥c, requires positive entries, and requires common parity. The conjunction records exactly those conditions.

Definition 1.3 (Conjecture 5.1).

Formalization. D5/S3/Combinatorics/BinomialBases/BraunBrueggeFacetSumConjecture.claim (✓ std3).

Citation. B. Braun, K. Bruegge (2023). Facets of Symmetric Edge Polytopes for Graphs with Few Edges. URL: https://arxiv.org/abs/2201.13303v4.

Commentary.

Conjecture 5.1 states verbatim: “For n = 2k and k ≥ 2 with x_1 + x_2 + x_3 = n + 1, F(x_1, x_2, x_3) is maximized at F(n − 1, 1, 1). For n = 2k − 1 and k ≥ 3 with x_1 + x_2 + x_3 = n + 1, F(x_1, x_2, x_3) is maximized at F(n − 3, 2, 2). Further, for any x_1 ≥ x_2 ≥ x_3 ≥ 3 all even or all odd positive integers, F(x_1, x_2, x_3) ≤ F(x_1 + 2, x_2, x_3 − 2) and F(x_1, x_2, x_3) ≤ F(x_1 + 2, x_2 − 2, x_3), when the subtraction by 2 will maintain the inequalities on the x_i’s.” The four conjuncts encode these assertions with the admissible domain and the stated endpoint conditions.

Theorem 1.4 (The four assertions hold).

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

Resolves. Problems/braun-bruegge-2022-symmetric-edge-polytope-facet-sum-conjecture-5-1 (proved) by D5/S3/Combinatorics/BinomialBases/BraunBrueggeFacetSumConjecture.result.

Source. Repository-derived.

Acknowledgement. B. Braun, K. Bruegge (2023). Facets of Symmetric Edge Polytopes for Graphs with Few Edges. URL: https://arxiv.org/abs/2201.13303v4.

Commentary.

The proof writes each facet sum as a weighted sum of centered binomial rows. A Vandermonde identity preserves the paired mass under each two-unit transfer. The transfer difference has one sign crossing, and the third centered row is antitone with distance from the center, so the weighted difference is nonnegative. Strong induction then reaches the endpoint triples in both parity classes. Finite computation checks 58,088 admissible triples for 4≤n≤200; the centered-row argument proves the inequalities for arbitrary admissible triples.

References