# 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 complete proof package](three_prime_factors_complete.zip), with the [official license online](https://creativecommons.org/licenses/by/4.0/legalcode).

## Original verification material: MIT

Original Lean and Python sources, including generated proof sources,
certificate inputs and machine-readable verification records, are licensed
under MIT. The license text is supplied in [the complete proof package](three_prime_factors_complete.zip), with the [MIT license online](https://opensource.org/license/mit).
This includes the author's reused proof developments and the original
verification material in `formal/` and `publication/three_factors/`.

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.