To Count a Stone with Six Birds: A Mathematics is A Theory

Abstract

Limits, completions, and analytic continuations are usually introduced as definitions. This paper asks an operational question instead: when does a large discrete protocol — a difference quotient, a cumulative sum, a truncated Euler product — admit a stable continuous closure, and how can that be tested without overclaiming? It instantiates Six Birds Theory as a closure-and-audit method for mathematics. A discrete object is staged by refinement, the cost of compressing it is tracked by an explicit defect ledger, and a packaged object is accepted only when the ledger is controlled under refinement and the relevant operations descend to the packaged layer. Formal core (Lean 4 / mathlib) The exact finite-difference product rule with its remainder term, over any field and nonzero step. A limit bridge: convergent factor quotients force the product quotient to converge to the Leibniz value. Bounded quotients alone do not suffice; the paper gives a counterexample and shows that they still yield a derivation with values in a quotient of bounded sequences. The classification of R-derivations of R[X] by their value on X, over any commutative semiring. The two contracts that make packaging well defined: vanishing distance in a pseudometric is an equivalence relation, and uniformly Lipschitz stage operators respect it. The 17 exported declarations use only Lean's three standard axioms. The bounded-quotient counterexample and the quotient-valued derivation are proved in the text and are not mechanized. Numerical exhibits Calculus. In a matched population of 300 candidate stencils, a refinement-stability gate alone retains identity-like, first-derivative, and second-derivative operators (100, 100, and 81 of 100 each); adding a shrinking Leibniz defect retains only the 100 first-derivative stencils. Cumulative sums converge to each other and to exact antiderivatives at their classical rates. Coordinate change. Two routes for computing a derivative after a change of variables approach each other under refinement (fitted exponent about 1.46 over four grids), with an identity-chart null control and checks against the exact derivative. Primes. Additive and multiplicative staged closures of ζ provably converge to a common limit for Re(s) > 1, and their route mismatch falls to 0.052 at cutoff 800 on the tested grid. On a critical-strip grid with symmetrized packaging, the same naive truncations drift apart (mismatch 5.0×1012). Positivity. In an Ising partition polynomial, shrinking the negative couplings to zero reduces the mean distance of the zeros from the unit circle from 0.87 to rounding level; the endpoint is an instance of the Lee–Yang circle theorem. The diagnostics prove no new theorem about ζ or its zeros. Every table, data figure, and generated number is regenerated from audited artifacts in the accompanying repository. Version 3 follows a full mathematical review of the statements, the Lean library, and the code, and a rewrite for readability. Appendix B of the paper lists the changes.