[Vilin97]

The Hasse–Minkowski import in #513 retains file-level credit for its three HassePrinciple-derived modules, but the generated repository NOTICE has no corresponding secondary attribution. Preserve the pinned source repository's complete notice in NOTICE.extra.yml and regenerate NOTICE, including the original authors, Women in Numbers 7 collaboration, and derived-file mapping.

The source is NOTICE at 47f0e9b5cba6e6354b882bc5856a11962ba61f4a. The additional introductory sentence explains that its upstream paths are vendored beneath LeanPool/.

Validation: python3 -m lean_pool.notice --repo .. --check and git diff --check pass. This PR changes only attribution metadata and its generated notice; it is separate from #513 to respect content/non-content separation.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds upstream attribution notices for a vendored library.

The PR appears safe to merge on the reviewed changes, subject to confirming the claimed verbatim match with the pinned external notice.

Summary

Adds the pinned Hasse–Minkowski upstream notice to attribution metadata and the generated NOTICE, including the HassePrinciple-derived file mapping.

• The changed files are attribution metadata only.
• The claimed verbatim match to the external pinned notice was not independently verified.

_{Reviews (3) · Last reviewed commit: "Merge commit '99afd29ebded0c43ff30ad482a..."}

[Vilin97]

Reviewed exact head 58cf9284b79016d418ca0bfe3443146e95789a63. Recommendation: approve when required CI completes.

The two-file change adds the Hasse–Minkowski upstream NOTICE to the supplemental attribution registry and regenerates NOTICE. I independently checked that the full text from pinned upstream commit 47f0e9b5cba6e6354b882bc5856a11962ba61f4a is retained verbatim, including the HassePrinciple workshop authors and the three derived-file mappings. All prior supplemental entries are unchanged; this is exactly one new entry. No Lean content or gates are modified. The generator check, diff check, and Python CI pass. This completes the separately scoped attribution follow-up for merged #513.