Monkman–Sirker Configurational Entropy
Abstract
Poisson-binomial configurational entropy is nondecreasing under majorization throughout the closed unit cube.
Definition 1.1 (The majorization claim).
Formalization. D5/S3/Entropy/PoissonBinomial/MonkmanSirkerConfigurationalEntropy.claim (✓ std3).
Citation. D. Monkman; J. Sirker (2023). Symmetry-resolved entanglement: general considerations, calculation from correlation functions, and bounds for symmetry-protected topological phases. DOI: 10.48550/arXiv.2307.05820. URL: https://arxiv.org/abs/2307.05820.
Commentary.
Monkman and Sirker, Section 3.3, ‘A conjecture on the concavity of Sc’: “We note that the configurational entropy Sc = S + (−SN) is a sum of a concave and a convex function. Therefore, one cannot directly apply majorization to Sc based on the already obtained results for S and SN. However, this does not rule our that Sc is also a concave function of the parameters {Ck}. Similar to the original Shepp-Olkin paper [22] we will here just investigate the cases M = 2 and M = 3. Based on these results, we conjecture that Sc({Ck}) is indeed Schur concave and majorization thus applies.”
For every finite dimension M and two vectors c and d in the closed unit cube, moreMixed d c implies F c at most F d. Here F is the sum of binary entropies minus the entropy of the sum of the independent Bernoulli variables; logarithms are natural.
Theorem 1.2 (Majorization increases configurational entropy).
Proof. Machine-checked in Lean as D5/S3/Entropy/PoissonBinomial/MonkmanSirkerConfigurationalEntropy.result (✓ std3). ∎
Resolves. Problems/monkman-sirker-2023-configurational-entropy-schur-concavity (proved) by D5/S3/Entropy/PoissonBinomial/MonkmanSirkerConfigurationalEntropy.result.
Source. Repository-derived.
Acknowledgement. D. Monkman; J. Sirker (2023). Symmetry-resolved entanglement: general considerations, calculation from correlation functions, and bounds for symmetry-protected topological phases. DOI: 10.48550/arXiv.2307.05820. URL: https://arxiv.org/abs/2307.05820.
Commentary.
The interior majorization chain reduces the assertion to the pairwise T-transform inequality. For boundary vectors, the same increasing affine map sends both vectors to the open cube and preserves the descending-prefix majorization inequalities. Continuity passes the inequality to the original vectors.
This statement includes empty vectors and deterministic Bernoulli parameters. It does not assert joint concavity, strict Schur concavity or classify equality cases. The proof uses general finite-dimensional inequalities rather than bounded enumeration or numerical certification.