# Licensing

Copyright © 2026 Michael Schroeder.

## Paper and prose: CC BY 4.0

The PDF, TeX manuscript, embedded bibliography, citation metadata and prose
documentation in this edition are licensed under Creative Commons
Attribution 4.0 International. The license text is supplied in
[the compact proof package](nine-prime-support-1.0.1.zip); the [official license](https://creativecommons.org/licenses/by/4.0/legalcode) is also available online.

## Original verification material: MIT

Original Lean, Python and C++ sources, including generated proof sources,
certificate inputs and machine-readable verification records, are licensed
under MIT. The license text is supplied in [the compact proof package](nine-prime-support-1.0.1.zip); see also the [MIT license](https://opensource.org/licenses/MIT).
This includes the author's vendored proof developments and the original
verification material inside `lean_proof.tar.xz`.

These licenses apply to their respective components; they are not
alternative licenses for the entire deposit. Third-party material and
dependencies, including Lean and mathlib, retain their existing licenses,
copyrights and notices. No license over third-party material is purportedly
granted here. Dependency lockfiles identify upstream projects; dependency
sources and compiled caches are not included.