Ctrl+K

Sources and clean-room provenance

Sources and clean-room provenance#

The arithmetic corpus uses external curricula as coverage maps, not as an unexamined pool of proof text. For each source the repository records its exact URL, revision where available, license, reuse mode, topic mapping, and known gaps.

Natural Number Game 4#

The Lean 4 Natural Number Game is pinned in the source register and licensed Apache-2.0. Its active worlds give a strong foundation in Peano equations, addition, multiplication, order, cancellation, nonzero products, and powers.

Its current game manifest does not supply a prime-number corpus: the prime, even/odd, and strong-induction worlds remain outside the active game, and the prime-world file is an empty work-in-progress stub. The final power-world FLT exercise uses a deliberately unsound teaching escape and is excluded from the lemma corpus. The source is therefore evidence for the early semiring/order coverage, not for primes or factorization.

The Mechanics of Proof#

Heather Macbeth’s The Mechanics of Proof supplies an excellent curricular map from structured proof through parity, modular arithmetic, division, the Euclidean algorithm, gcd, prime divisors, Euclid’s lemma, and infinitely many primes.

The associated source repository has no repository-wide reuse license and its relevant Lean files reserve rights. The policy here is reference-only, clean-room reconstruction: do not copy its prose, Lean code, exercises, or proof scripts. We independently state Peano formulas, construct Peano proofs, and require the local kernel check.

An Illustrated Theory of Numbers#

Martin Weissman’s programming resources provide a later computational roadmap: Euclidean algorithms, sieves, primality tests, factorization, modular exponentiation, primitive roots, totients, and cryptographic applications.

The companion Python notebooks are GPL-3.0. They remain external algorithm indexes; no notebook code is copied into this MIT/CC BY-SA project. The published AMS book is cited as a book, not mined for source or prose.

Mathlib FTA companion#

The independently checked FTA companion imports Mathlib’s natural-number prime-factor list development at the exact Apache-2.0 revision 37df177aaa770670452312393d4e84aaad56e7b6. It restates existence and permutation uniqueness as one explicit theorem in artifacts/lean-fta.

This is formal evidence, not curricular source material and not Peano theorem authority. Its dedicated verifier rejects sorryAx and requires the exact reported standard axioms propext, Classical.choice, and Quot.sound.

Published modular catalog#

The 26-record Peano modular catalog is pinned to integration commit 923f6816c8c5f17a9a276b9e767145f89aff2e09 under its retained MIT notice. Its unaltered validation report binds the original source commit, catalog hash, scripts, certificate hashes, and proof metrics.

Fourteen records coincide exactly with independently developed M20 entries. The reconciled runtime keeps the full source catalog for provenance but exposes each compatible theorem once, adding twelve unique residue and fourth-power capstones. A mismatched same-name record is an import error.

Reuse modes#

The source register uses explicit modes:

  • project_internal for this repository’s own material;

  • statement_adapted_proof_reconstructed where a licensed mathematical statement informs coverage but the Peano proof is rebuilt;

  • reference_only_clean_room for unlicensed or publisher-controlled sources;

  • algorithm_index_clean_room for GPL notebooks used only to identify future algorithms and examples;

  • checked_external_companion for a pinned formal-library theorem checked in a separate prover without importing it into Peano’s trusted base.

Mathematical facts are reusable; distinctive prose and source code are not silently treated as public domain. Provenance accompanies even independently proved facts because it explains why a lemma belongs in the curriculum.

Contents