NOTICE

The Zhang-Yeung Inequality

Copyright 2026 Christopher Boone

A Lean 4 formalization of the Zhang-Yeung conditional information
inequality, a non-Shannon-type bound on Shannon entropy that cannot
be derived from the Shannon inequalities alone.

This repository contains material under multiple licenses.

Project-authored substantive source code is licensed as follows:
  - Lean code (`ZhangYeung/**/*.lean`, `ZhangYeungTest/**/*.lean`,
    `ZhangYeung.lean`, `ZhangYeungTest.lean`) under the Apache License 2.0.
    See LICENSES/Apache-2.0.txt.
  - The `bin/bootstrap-worktree` shell script under the Apache
    License 2.0; the SPDX tag is inline per the skill's file-type
    matrix because it is substantive code.

Hand-authored infrastructure config — Makefile, lakefile.toml, YAML
(including CI workflows under `.github/workflows/`), JSONC,
.editorconfig, .gitignore, cspell word list, and VS Code editor
config — is licensed under the Apache License 2.0 via the
`REUSE.toml` config-group annotation. These files are not content
over which the project asserts substantive authorship; the
REUSE.toml glob keeps lint clean without per-file sidecars or
inline headers on every dotfile.

Project-authored prose — READMEs, agent configs, planning documents,
research notes, formalization reviews, and this NOTICE — is licensed
under Creative Commons Attribution 4.0 International (CC BY 4.0).
See LICENSES/CC-BY-4.0.txt. This material is covered by the
`REUSE.toml` prose-group annotation; per-file SPDX headers are not
required for prose.

CODE_OF_CONDUCT.md is adapted from the Contributor Covenant via the
Organization for Ethical Source and is licensed under Creative
Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0). See
LICENSES/CC-BY-SA-4.0.txt. Coverage is authoritative via a dedicated
`REUSE.toml` override annotation on that one file; the dual copyright
line is preserved verbatim from the upstream phrasing.

Files auto-regenerated by tooling — the Lake manifest
(`lake-manifest.json`) and the pinned Lean toolchain
(`lean-toolchain`) — are dedicated to the public domain under CC0
1.0. See LICENSES/CC0-1.0.txt. Content is mechanical output the
project does not originate; the CC0 dedication is covered via the
`REUSE.toml` generated-group annotation rather than per-file
headers.

Third-party bundled reference material under `references/papers/**`
and `references/transcriptions/**` is reserved for study,
verification, and scholarly context. It is covered under
`LicenseRef-Reference-Material`. See
LICENSES/LicenseRef-Reference-Material.txt. Copyright in those
materials remains with the original authors and publishers, as
identified per-file in the accompanying `.license` sidecars.
Per-publication attribution (IEEE, original authors) is preserved
via per-file sidecars rather than a REUSE.toml glob, because the
collection is small enough that per-work detail is more legible
than a uniform annotation. No license to modify, redistribute, or
republish is granted by this repository.

The following paths fall outside the authored-license sweep and are
not covered by SPDX tags in this repository:
  - LICENSES/ itself (tool convention)
  - Vendored dependency state (e.g. .lake/packages/**)
  - Build artifacts and caches that are gitignored

Per-file SPDX metadata together with the root REUSE.toml prose,
config, generated, and CoC annotations is authoritative for this
repository. This NOTICE is a summary; it does not override per-file
or per-glob tags. See https://reuse.software/ for the REUSE
specification and tooling.