A generative machine for the multiplicative number line: an exact machine-checked corpus and an elementary prime number theorem in Lean 4

The number line is, at bottom, a line of poles: abstract objects distinguished by order and nothing else, the line existing exactly to index them — every numeral system a display layer over this one structure. We formalize, in Lean 4 over Mathlib, a deterministic generative machine for the multiplicative structure that this bare index acquires under a single further commitment. On the succession of poles, waves are born at the least position not yet struck, and a wave born at coordinate q strikes every q-th position from its birth onward, so that period equals birth coordinate; from the seed pair {2,3} onward, the birth sequence is exactly the sequence of primes. The machine — the union of these waves under the birth rule — is one deterministic automaton, a finite rigid operator set generating a single run of the number line, and every theorem below is an exact observable of that run. In closed form each wave is a gear: a rotor of period q meshed to the successor line, itself the unit gear, so that multiplication enters as the meshing table of iterated succession. The classical sieve of Eratosthenes is this machine's boolean shadow: the machine retains what the sieve forgets — single-strike ownership, birth order, and phase — and the corpus below is a theory of that retained structure. The identification is proved rather than analogical — the machine's next birth coordinate equals the next prime, with completeness in both directions — and the generation rule is characterized extremally: the prime sequence is the unique lexicographically minimal admissible pattern, and the generation rule itself is proved as a stagewise iff. Around the machine we prove a corpus of exact finite theorems in which the multiplicative organization of the integers appears as the machine's output: a finite Mertens identity, exact at every cutoff; single-strike ownership and the dilation law of refinements; a "two-gear" conservation law equating the Chebyshev count with its Moebius-proportional companion up to a signed two- edge remainder ledger, exactly, on every integer window 1 <= A <= B <= N; a correlation calculus for squarefree combs — closed-form pair correlations and strictly sub-Poisson window variance at every squarefree period and positive window length — transferring to an unconditional mean-square envelope for prime counts in cones; and an operator representation of the centered von Mangoldt source with a closed-form kernel. On this base we give an elementary proof of the prime number theorem, apparently the first elementary route in Lean 4, whose dependency cone is audited mechanically: it consumes no Riemann zeta function, no L-series, no Tauberian theorem, and no prior formalization of the theorem — the audit ships with the artifact and fails the build on regression. A closing chapter states where the classical landscape lives in the machine's currency at recorded grades: statements settled here, classical constants recovered with no parameters (Mertens, Euler–Mascheroni), and exact machine formulations of open statements — the square-root fluctuation circle and the twin prime conjecture among them. Every theorem is sorry-free and depends only on Lean's three standard axioms, enforced by a build- time axiom guard. The development (40 modules plus an anchors module, some 24,000 lines) is frozen as a standalone, independently verifiable artifact.