The entropy photon-number inequality
From OpenAI Aftermath
The entropy photon-number inequality is a conjectured inequality for bosonic quantum states, proposed by Guha, Erkmen and Shapiro in 2007 as the quantum counterpart of the classical entropy power inequality for the mixing of light at a beam splitter. The entropy photon number of an n-mode state is the mean photon number per mode of the product of n identical one-mode thermal states with the same total entropy, and the conjecture states that this quantity is concave under beam-splitter mixing of independent inputs. A manuscript in OpenAI's public mathematics collection, dated 24 September 2026, states a proof for inputs of finite mean energy.
Background
- As recounted in the manuscript's introduction, except where noted:
- The conjecture and its uses. Guha, Erkmen and Shapiro formulated the inequality and explained its consequences for bosonic communication: the constrained minimum output entropy of thermal attenuators and the capacity region of bosonic broadcast channels. Earlier special cases included one-mode number-diagonal inputs with two nonzero probabilities and a vacuum second port.
- Quantum entropy power inequalities. König and Smith proved a quantum entropy power inequality, including a linear entropy bound for every transmissivity; De Palma, Mari and Giovannetti proved the exponential form for every transmissivity, and De Palma and Trevisan gave a rigorous finite-energy treatment. When the two input entropies differ, these bounds are weaker than the entropy photon-number inequality, which thermal inputs attain exactly.
- A discrete form. Guha, Shapiro and García-Patrón, in arXiv:1605.07853, proposed a discrete entropy power inequality for the photon-number distributions obtained by mixing number-diagonal states at a beam splitter, and state that it is a special case of the entropy photon-number inequality. The manuscript does not cite this paper.
- Partial results. The inequality was known for two independent Gaussian inputs, by De Palma. Giovannetti, Holevo and García-Patrón settled the unconstrained minimum-output problem for broad classes of Gaussian channels; De Palma, Trevisan and Giovannetti proved the sharp constrained bound for one-mode phase-covariant Gaussian channels and a multimode extension for inputs diagonal in a product basis; De Palma treated multimode entanglement-breaking Gaussian channels.
The original result
- The entropy photon-number inequality (24 September 2026). The entropy photon-number inequality states that for every finite number n of modes and every two independent n-mode bosonic states ρA, ρB of finite mean energy, the output ρC of a beam splitter of transmissivity η satisfies g−1(S(ρC)/n) ≥ η g−1(S(ρA)/n) + (1 − η) g−1(S(ρB)/n), where S is the von Neumann entropy and g(t) = (t + 1) log(t + 1) − t log t. Entanglement among the modes within either input is allowed, and thermal inputs give equality. The manuscript states that this resolves the conjecture in this finite-energy setting.
- Consequences, as stated: the exact minimum output entropy at fixed input entropy for every finite tensor power of an identical thermal attenuator, over finite-energy inputs that may be entangled across modes; and the exact classical capacity region of the degraded two-receiver pure-loss bosonic broadcast channel under a mean photon constraint.
- Method, as described: assuming a strict violation, the proof fixes thermal reference parameters and studies a regularized variational problem whose minimizers lead to a contradiction; an interpolation theorem for positive diagonal quadratic forms, with a Stieltjes representation as its essential analytic step, supplies the key comparison.
- Sources. Commit
7ef5c0cof the openai/math repository: The entropy photon-number inequality. - Formalization, as described by the repository. The scope note lean/docs/273.md states that the formalization proves the inequality for two independent bosonic inputs with finite mean energy and any finite positive number of modes, with entanglement among the modes within either input allowed; the thermal-attenuator and broadcast-capacity consequences are outside it. Its Comparator statement is EntropyPhotonNumber.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 31 October 2026; AI Proved What? row 31 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Photon-number entropy and bosonic communication, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains family 273: bosonic modes and thermal entropy; independent ports and the sharp inequality; compactness in an infinite-dimensional state space; a regularized negative minimum; entropy curvature and the thermal defect; stationarity, cancellation and rigidity; minimum output entropy; and a classical broadcast capacity region. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean theorem states the inequality on the untruncated Fock space with arbitrary entangled inputs. It notes that equality for thermal inputs is not separately stated, and as a caveat that the output state is specified only through an explicit hypothesis on its matrix elements, so the theorem would be vacuous if that formula were wrong or unsatisfiable. It lists the hand-written quantum-optics definitions as definitions to check, and records a sandboxed Comparator pass for EntropyPhotonNumber. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list EntropyPhotonNumber, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_271 | Review (AI-assisted audit) | Reports no gap, after reading Sections 0 to 5 line by line and checking the structure of Section 6. It records one minor issue: two steps in the proof of Lemma 2.2, the Stieltjes representation, are only sketched; the review states that they look correct and agree with numerical checks, but that a referee would want them written out. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-18 | AI Proved What?, episode 273 Light that mixes gently, proved at last?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of one OpenAI preprint, 32 pages, dated 24 September 2026: the inequality conjectured by Guha, Erkmen and Shapiro in 2007, for two independent inputs with finite mean photon number, in any finite number of modes and with any entanglement inside each input, with the corollaries on the least output entropy of identical thermal attenuators at a given input entropy and on the exact capacity region of the degraded lossy broadcast channel. The episode recalls that a 2018 survey and a paper of late September 2026 still called the inequality an open conjecture. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 30 October 2026: posted as a preprint: OpenAI, 32 pages, dated September 24, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem, not the corollaries. |
Notes
- The background summarizes the manuscript's own account of earlier work; the item on the discrete form cites Guha, Shapiro and García-Patrón directly.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
