# The entropy photon-number inequality

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The entropy photon-number inequality](../../preprints/The-entropy-photon-number-inequality-September-24-2026/paper.pdf)

## Scope

The formalization proves the entropy photon-number inequality for two independent bosonic inputs with finite mean energy and any finite positive number $n$ of modes. Write $N(\rho)=g^{-1}(S(\rho)/n)$, where $S$ is von Neumann entropy and $g(x)=(x+1)\log(x+1)-x\log x$ is the thermal entropy per mode. For a beam splitter of transmissivity $0\le\eta\le1$, its output satisfies $N(\rho_C)\ge\eta N(\rho_A)+(1-\eta)N(\rho_B)$.

Entanglement among modes within either input is allowed. The thermal-attenuator minimum-output-entropy and broadcast-capacity consequences in the paper are outside this selected inequality.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Entropy photon-number inequality for finite-energy bosonic inputs | [EntropyPhotonNumber.lean](../ComparatorChallenges/EntropyPhotonNumber.lean) |