Source edition and formalization correction

The publicly accessible Family 276 source is titled Classical capacity and entropy inequalities for generalized amplitude damping, attributed to OpenAI, and dated 24 September 2026 OpenAI276. The source uses natural logarithms in its entropy functions and a factor $1/\ln 2$ when reporting information in bits.

The scope note lean/docs/276.md describes repeated-use Holevo additivity, equality with operational capacity, and attaining phase-pair product ensembles. It excludes arbitrary different partner channels and separate-measurement optimality LeanScope276.

There is an additional distinction. In the inspected ComparatorChallenges/AmplitudeDamping.lean, the theorem OAI.GAD.main ends with by sorry LeanTarget276. That target file supplies a specification, not a completed proof of its theorem body. This observation is not a claim that every other repository artifact has been inspected. No Lean execution or verification of a different implementation is asserted.