Six Birds for Incompleteness: Fixed Packages, Package Change, and Conditional Arithmetic Lift

Gödel's theorems tell us that no consistent, effectively axiomatized theory containing enough arithmetic can settle every arithmetic truth, so mathematics grows by adding axioms. They do not, by themselves, say how to describe that growth or how to compare different ways of growing. This paper studies theory growth through two ideas. A package is a fixed closure rule (an idempotent map) and a frozen ledger is a fixed way of scoring candidate extensions. The first idea yields exact statements about growth. Applying one idempotent package repeatedly changes nothing after the first step. If a second package moves the result of the first, the two packages provably differ at that result. Along any run of idempotent packages, the number of steps that change the state is at most one plus the number of times the package is switched. The bound is sharp: two computable, monotone, inflationary closures on the natural numbers, applied alternately, climb 0, 1, 2, … forever. The second idea yields exact statements about comparison. When the ledger cannot tell apart operators that agree on a support set (the cone), Pareto efficiency passes from an operator to any operator in the comparison domain that agrees with it on the cone. A designated family of canonical operators, contained in the comparison domain, supplies efficient representatives under every such ledger exactly when it meets every agreement class of the domain. Combining these results with an explicit three-part contract gives the main conditional theorem. Let the ledger be invariant under agreement on the cone. Suppose the canonical family lies in the comparison domain and consists of computable monotone maps, and that it contains a member agreeing on the cone with the computable, monotone, efficient input under study. Then the input has an efficient, computable, monotone canonical representative that agrees with it on the cone. A Lean counterexample shows that the admissibility clause cannot be dropped. We also give a concrete arithmetic case in elementary arithmetic EA. A guarded consistency extension, φ ∧ (Con(EA) → ConEA(φ)), is provably equivalent to the ordinary consistency extension on a true cone and differs from it outside the cone. Under a nonconstant invariant ledger it is efficient and the identity is dominated. A theorem of Walsh yields the same kind of agreement for a restricted class of operators. All internal results are checked in Lean 4 with mathlib. The second incompleteness theorem and Walsh's theorem are cited results and enter the formal statements as explicit hypotheses. Descriptive measurements from an earlier simulation study are reported for context only and support none of the theorems.