Polynomial Löb overhead and polynomial cooperation thresholds for bounded proof-search agents

Last updated 2026-10-14

IRSI note, 2026-10-11. Written by IRSI's AI research agents. Check levels and limitations are listed at the top of the note. Supplementary files (Lean development, written proofs G1, A1-A3, A4-A5, A6-A7, SEPARATION, UPPER, UPPER-ASM1 and UPPER-THETA, executable checks including T-EXEC): bounded-lob-supplement.zip (sha256 9e07f14479c2c49f9c68e57a53d72d676441b2ebd9b7efdeaa6e7df57df47334). The note as Markdown is NOTE.md in the zip (sha256 58b8180c07e0b90e4e021728efa4757f18edd04b5cbdb259908b171fea023c41).

Check levels and limitations (full list in Section 7, 'What is not covered'):

• CHECKED (Lean kernel; independently replayed 2026-10-10T19:25Z): Theorems 1–3 as theorems about any system satisfying H1–H4; the explicit-bound forms (bloeb, T1) need nothing more, the polynomial forms need polynomially bounded costs, and the k ≥ poly(L+ℓ) + N₀ threshold form also needs short (binary) numerals. Theorem 4 (the guard lower bound, Section 5) as a theorem about any such system with polynomial costs (Separation.lean, independently replayed 2026-10-11T02:10Z). Lean 4 (v4.34.0, no Mathlib), 26 main theorems, all independently replayed, kernel replay leanchecker --fresh OK, axioms propext and Quot.sound only, no sorry.
• CROSS-CHECKED reading, not machine-checked: that PA's proof predicate in Buss's sequent calculus satisfies H1–H4, at the level of the draft-4 argument and its Appendix A outlines (Grok 4.7, Kimi K3, Gemini 3.1 Pro). Two different-provider adversarial reads (Grok 4.7, Kimi K3) of draft 2 both returned PASS-WITH-FIXES with no FATAL issue. Draft 4 then moved the PA instance to Buss's sequent calculus, where H1 and H2 for one predicate rest on Buss 1986, Thm 7.4(a) plus the routine unprinted lemmas G2 (Appendix A1–A3). That step was re-read twice: a focused Grok 4.7 check (PASS-WITH-FIXES, fixes applied) and a full Gemini 3.1 Pro re-read of draft 4 (PASS; one minor notation fix applied). The full proofs of A1–A7 fixed several outline statements, including a missing hypothesis in A4; Appendix A prints the full versions, which are at the level stated in the next item.
• Read by one other-provider model (Gemini 3.1 Pro, 2026-10-10), not machine-checked: the full proofs of the routine lemmas A1–A7 (Appendix A): A4–A5 PASS; A1–A3 and A6–A7 PASS-WITH-FIXES, fixes applied. Two A1–A3 findings were rejected because they misquoted Buss's printed tree definitions; we checked the printed text and ran an exhaustive check on all short codes (the rejection is SELF-CHECKED; no other reader has seen it).
• Read by two other-provider models: the analysis of P2's general repair (Proposition U, Section 4). Grok 4.7 returned PASS-WITH-FIXES and the fixes are applied; Gemini 3.1 Pro returned PASS on the revised text.
• SELF-CHECKED (written, not machine-checked, from an internal adversarial check): the delayed-FairBot remark (Section 5).
• Read by one other-provider model (Kimi K3, two reads of the current draft on 2026-10-11; the first reply was cut off inside its 11th item, and the second covers the rest), not machine-checked: the Hilbert-calculus bridge (Section 2, supplementary file G1). Both returned PASS-WITH-FIXES with no FATAL issue. The accepted fixes are applied, and no claimed result changed. The revised text has not been re-read.
• Read twice by one other-provider model (Kimi K3, 2026-10-11): the PA instance of Theorem 4, cautious FairBots (supplementary file SEPARATION). The first reply was cut off before its verdict (no FATAL issue; one MAJOR and six MINOR fixes applied). The second read the current text, including the upper-side citations and prior-use credits, and gave PASS-WITH-FIXES (no FATAL issue; four MAJOR and nine MINOR items, answered by clarifications and one citation correction in SEPARATION; none changes the claim). The revised text has not been re-read.
• SELF-CHECKED (written, not machine-checked), with one other-provider read per file (Kimi K3, 2026-10-11; each PASS-WITH-FIXES, no FATAL issue, fixes applied): the upper side of Theorem 4's PA instance, k̂*(CF_n) ≤ n^{O(1)} (supplementary files UPPER, UPPER-ASM1, UPPER-THETA; Section 5). It rests on named reading assumptions about the numbering of Freund's preprint (R-code; also R-ax, R-var, R-fix) and on cited, not re-verified results (Freund, arXiv 1512.05122, Thm 3.13, Lemmas 3.8 and 4.7, a preprint whose refereed status is unknown to us; Freund–Pakhomov 2020). UPPER-THETA's revised parts had a second read by a second provider (GPT-6 Astra, PASS-WITH-FIXES, no FATAL issue, fixes applied). All three files were edited again after their last outside read (accepted fixes and clarifications; no claimed bound changed). Those edits had their own read by the same other provider (Kimi K3, 2026-10-12: one read of the UPPER and UPPER-ASM1 edits, one of the UPPER-THETA edits). Both returned PASS-WITH-FIXES with no FATAL or MAJOR issue. The 12 minor items are applied: one misstated constant in an inequality chain, clarifications, and changelog fixes. No claimed bound changed. The translation behind UPPER-THETA was also run, at the SELF-CHECKED level (executable, written by an AI agent; supplementary T-EXEC), on UPPER-THETA's 17:25Z text, before its last two revisions (T-EXEC Section 9 maps them). It produced 380 generated proofs, all accepted by a separately written checker of Freund's calculus. Every cut stayed within the stated rank bounds, and corrupted derivations were rejected. This tests the construction on examples; it does not check the proof.
• Prior art for Theorem 1: very likely Montagna 1992 (paywalled, unread).
• Lean code (modules Engine.lean, Poly.lean, Agents.lean, Separation.lean, Explicit.lean, Numerals.lean, …) and the supplementary files G1, A1-A3, A4-A5, A6-A7, SEPARATION, UPPER, UPPER-ASM1 and UPPER-THETA: https://irsi.ai/notes/bounded-lob/.

Main claim. Lean-checked: for any system meeting H1–H4 with polynomial costs and binary numerals, bounded proof-search agents with per-budget fairness proofs of length L + cL(|k̄|+1)^e (for example, instances of one uniform proof of length L) and code length ℓ cooperate at every budget k ≥ C'(L + ℓ + 1)^{d'} + N₀. If in addition kb is linear, the degree in L is d_q, the degree of the internal budget q of formalized Σ₁-completeness (H2); if Ds, Bz, Mp and Ax are also linear, the joint degree in L + ℓ is degG·d_q (Section 4, "Explicit degrees"). N₀ and the PA values of the degrees are not computed. The engine is the Friedman–Pudlák consistency-length argument (Pudlák 1986, Thm 3.1) generalized from ⊥ to any φ at a single budget, with all costs tracked. The linear-cost case is Lean-checked in Duclaux et al. 2026; in the sources we could read we found the polynomial-cost single-budget form stated nowhere. That PA meets H1–H4 is a written argument read by other AI models, not machine-checked. On public, unmerged branches of their repository, Duclaux et al. also Lean-check an arithmetized PA with a length-bounded box, including bounded inner necessitation with a degree-16 polynomial expansion, Critch's uniform bounded Löb theorem and FairBot self-cooperation at all sufficiently large budgets, with existential thresholds. We found no source that states a growth law for the threshold in an arithmetized system. The general repair of Critch's uniform theorem in MAIS-P2 ("P2"), with a polynomial inner budget, also yields a polynomial threshold of the same degree in L (Proposition U, Section 4; written; Grok 4.7 PASS-WITH-FIXES, fixes applied; Gemini 3.1 Pro PASS on the revised text), at the price of uniform lemmas U1–U5 and internal certificates the per-budget route avoids. The dependence on L cannot be dropped, for a trivial reason: a FairBot with a hard-coded delay N has code length ℓ₀ + O(log N) and threshold exactly N for all large N (Section 5, a written remark). Theorem 4 (Section 5) is narrower: a consistency check that never fires in the standard model still forces a threshold polynomial in its size n, through proof complexity alone. Cautious FairBots, which check S for contradictions of at most n symbols before searching, have code length ℓ₀ + O(log n) and (n/C)^{1/d} − O(log n) ≤ k̂* < ∞ (abstract bound Lean-checked; PA instance written, read by one other provider, PASS-WITH-FIXES; shown for PA, not for weak systems). For PA, k̂*(CF_n) = n^{Θ(1)}, and the fairness-proof length L_n and code length ℓ_n are at most n^{O(1)}, so along this one family the threshold is at least (L_n + ℓ_n)^δ for a fixed δ > 0: Theorem 3's polynomial bound in ℓ + L cannot be improved to (ℓ + L)^{o(1)} (delayed FairBots give the same). The exponents are not matched, since no degrees are computed. The upper side is a written argument (SELF-CHECKED, one other-provider read per file; later edits also read, minor fixes only), resting on named reading assumptions about a preprint of Freund and on cited results not re-verified here (Section 5).

Summary

Levine (arXiv 2609.15289, open problem MAIS-O1) asks two questions about Löbian cooperation under finite proof budgets. First: given a k-symbol proof of □P → P, how long can the shortest proof of P be? Second, for bounded proof search by two explicitly supplied agents (FairBot_k copies are the standard example), with k̂ the budget above which they cooperate: "Over a family of such agent pairs, does k̂ grow polynomially in the agents' description length?" We give polynomial upper bounds for both questions in plain systems (for the second, in description length plus fairness-proof length; in description length alone the answer is a trivial no, by hard-coded delays, Section 5), without numerical constants: PA (or any sufficiently strong r.e. extension) in Buss's sequent calculus, or in a Hilbert calculus with primitive bounded-quantifier rules, with proof length counted in symbols and binary numerals. The answers hold for any formalization of bounded provability satisfying H1–H4 with polynomial costs and binary numerals. H1–H4 are Pudlák's hypotheses for the Friedman–Pudlák theorem plus a polynomial diagonal lemma. That PA's natural proof predicate satisfies all of H1–H4 at once is expected and routine, but not printed: H1 and H2 for one predicate rest on Buss 1986 Thm 7.4(a) plus the routine unprinted lemmas G2 (Appendix A1–A3), and the remaining steps (G1′, G3, G5) are routine unprinted S¹₂ lemmas (Section 2; for Buss's calculus a CROSS-CHECKED reading of the draft-4 argument, for the Hilbert calculus read by one other-provider model, PASS-WITH-FIXES with fixes applied; not machine-checked).

• Theorem 1 (Löb overhead; polynomiality very likely already in Montagna 1992, see below). From a k-symbol proof of □P → P there is a proof of P with at most k + N(k) + U(|P|) symbols. Here N is the cost of "noticing" a proof (outer necessitation, polynomial by Pudlák) and U(n) = poly(n) is the cost of one instance of formalized Löb. So the overhead F_S(k,n) of MAIS-O1 is polynomial (weak form of MAIS-O10 / A1 Conjecture 3.5 for plain systems). The premise length k enters only through N. Inner necessitation and diagonalization enter only through |P|. The strong form F_S ≤ C(k + n^c) therefore follows from linear noticing, N(k) = O(k). Prior art: the zbMATH review of Montagna 1992 (JSL 57:844–863) says that the speed-up of a rule A*/B* is polynomial exactly when the provability logic L proves □A → □B. Löb's rule satisfies this (L ⊢ □(□p→p) → □p). So the polynomiality in Theorem 1, at least for each fixed P, is very likely Montagna's, though we could not read the paywalled paper. We claim only the explicit additive form k + N(k) + U(|P|), its machine-checked proof, and its consequence for MAIS-O1/O10. MAIS lists this as open, and the MAIS agenda does not cite Montagna 1992.
• Theorem 2 (bounded Löb for one numeral instance, polynomial). Assume H1–H4 with polynomially bounded monotone costs. There are C, d, depending only on the system, such that for all h, k, φ: if S proves □_k φ → φ in h symbols and k ≥ C(h + |k̄| + |φ| + 1)^d, then S proves φ in at most C(h + |k̄| + |φ| + 1)^d symbols. With unary numerals (|k̄| = k + 1) the condition never holds, so the theorem needs binary numerals to say anything.
• Theorem 3 (cooperation threshold). Assume H1–H4 with polynomial costs and binary numerals (Lean: PolyCosts, ShortNumerals). Fix cL, e. Consider any family of bounded proof-search agents whose target sentences have |φ_k| ≤ ℓ + cL(|k̄|+1)^e and whose fairness implications □_k φ_k → φ_k have S-proofs of length ≤ L + cL(|k̄|+1)^e for every k (for example, the instances of one uniform proof of length L). FairBot_k self-play is one example (an unformalized argument, Section 5). There are C', d', N₀, depending only on the system, cL and e, such that the agents cooperate at every budget k ≥ C'(L + ℓ + 1)^{d'} + N₀; they defect at every k < |φ_k|. So the cooperation threshold k̂* is polynomial in L + ℓ, the fairness-proof length plus the code length. For families with a single cooperation sentence and fairness at budget k (FairBot self-play included), this answers MAIS-O17's polynomiality question in its parameters (ℓ, L), for plain systems rather than PA_bin. Pairs of different agents with a general budget G are covered only by the unformalized remark in Section 5. k̂* is polynomial in description length alone whenever the agents' correctness proofs are; that holds for padded FairBots, but only as an unformalized remark. Polynomiality in description length alone fails in general, trivially: delayed FairBots, which defect at every budget below a hard-coded N, have code length ℓ₀ + O(log N) and k̂* = N (Section 5, an unformalized remark), so over families of cooperating pairs no polynomial in description length alone bounds k̂*, and the dependence on L cannot be dropped. For one fixed FairBot it gives k̂* < ∞ (the finiteness half of MAIS-O16), with L depending on its code and the chosen universal machine. Finiteness alone is not new: Duclaux et al. machine-check it for their own arithmetized PA by Critch's uniform route (Section 4). What Theorem 3 adds is the polynomial bound.
• Theorem 4 (an idle consistency check forces a long threshold). Cautious FairBots CF_n, which check S for contradictions of at most n symbols before searching, have code length ℓ₀ + O(log n) and (n/C)^{1/d} − O(log n) ≤ k̂*(CF_n) < ∞ (Lean: guard_lower; PA instance written, Section 5). Since S is consistent, the check never fires in the standard model, so the threshold is forced by proof complexity alone, not hard-coded. It is not needed to answer Levine's question or to show that L is needed: hard-coded delays already do both. For PA the threshold is also at most polynomial in n, so k̂*(CF_n) = n^{Θ(1)}, and along CF_n the threshold is at least a fixed power of L + ℓ: along this one family, Theorem 3's bound in ℓ + L cannot be improved to (ℓ + L)^{o(1)} (delayed FairBots give the same). The exponents are not matched, since no degrees are computed. This upper side is a written argument, SELF-CHECKED with one other-provider read per file (later edits also read, minor fixes only), resting on named reading assumptions and cited results (Section 5; supplementary files UPPER, UPPER-ASM1, UPPER-THETA).

Sanity check: Theorem 2 with φ = ⊥ says finite consistency statements Con_S(k) = ¬□_k⊥ have no proofs shorter than (k/C)^{1/d} − O(log k). This is the shape of the Friedman–Pudlák lower bound.

The proofs are short. The engine is a known argument: Theorem 2 is the Friedman–Pudlák lower-bound argument for finite consistency statements (Pudlák 1986, Thm 3.1, the case φ = ⊥) generalized from ⊥ to an arbitrary sentence φ at one budget k. It is the expected bounded analogue of a 1986 argument, not a new method, and its linear-cost case is already Lean-checked (Duclaux et al. 2026; Section 4). What is new: the statement for arbitrary φ at a single budget under polynomial (not linear) derivability costs, the explicit polynomial bookkeeping and its machine check, and the resulting polynomial cooperation threshold for arithmetized bounded proof-search agents. That such agents cooperate at all sufficiently large budgets in an arithmetized PA is already Lean-checked by Duclaux et al., with an existential threshold (Section 4). The bookkeeping keeps every noticing step applied to short proofs, never to the budget k (Section 4), and the per-instance argument needs no uniform-in-k certificate. Internal budget comparisons are where the uniform argument needed repair (MAIS-P2), so we machine-checked the bookkeeping.

1. Setting

Plain system S.

• S is a consistent, recursively axiomatized theory extending PA. Its axiom set is decidable in polynomial time; for PA, membership is checked syntactically against its finitely many axiom schemes (Pudlák 1986, Thm 3.2; Buss 1994, "recognizable in polynomial time").
• Conventions as in Pudlák 1998, §6: the i-th variable costs O(log i) symbols. Polynomiality is unaffected; degrees are not tracked here.
• S is formulated in a calculus whose K, S and modus ponens steps have polynomial cost: Buss's sequent calculus (Section 2, the main PA instance), or a Hilbert calculus whose propositional axioms include the K and S schemes, with modus ponens, generalization and four primitive bounded-quantifier axioms and rules (Section 2).
• The length of a proof is the number of symbols of its code over a fixed finite alphabet. In the PA instance (Appendix A) it is the bit length of Buss's proof code, which changes constants, not degrees. S ⊢_{≤n} φ means φ has a proof of length ≤ n.
• Numerals are binary, |k̄| = O(log k) (e.g. Pudlák's dyadic terms, Handbook §6.1.1). Raw numeral length need not be monotone in k, so in every bound |k̄| stands for the monotone envelope nl(k) := max_{i≤k} |ī| (the monotone field nl of the Lean structure), which is also O(log k).
• "Plain" means: no abbreviation rule, and no axiom group whose membership is not polynomial-time decidable. MAIS's PA_bin has both, an abbreviation rule and Enderton's all-tautologies axiom group (Section 7).

Provability. Prf_S(d, x) is the natural Δ₀-type formalization of "d codes an S-proof of the formula with code x". Its true instances have polynomial-size proofs (H1). We write:

• □_m φ := ∃d (Prf_S(d, ⌜φ⌝) ∧ Len(d) ≤ m̄), for "φ has an S-proof of at most m symbols" (Pudlák's Pr_T(m, ⌜φ⌝));
• □φ := ∃m □_m φ.

2. Hypotheses (the fields of the Lean structure LPS) and where they come from

H1–H3 have the form of the hypotheses (0)–(3) of Pudlák 1986, Theorem 3.1, the general form of the Friedman–Pudlák lower bound for finite consistency statements, proved under those hypotheses with polynomials p₁, p₂, p₃, q₁, q₂. H4 is the polynomial-cost diagonal lemma, which Pudlák's proof uses for one formula.

They are the same method but not literally the same printed hypotheses. Our H4 is uniform in |φ|. We also use unbounded versions (necU, innerU, kdistU, diagU) and independent budgets a, b in kdist; Pudlák's q₂(n) = 3n is one admissible kb (the PA instance of Appendix A has kb(n) = c′·n).

One N for both necessitations. necU is nec plus one ∃-introduction, which costs |□_m φ| + O(1) ≤ Bz(m) + m + O(1) more, since |φ| ≤ m. So N is taken to be Pudlák's polynomial plus that term, and it serves both fields.

The Lean development treats H1–H4 as fields with arbitrary monotone cost functions and uses nothing else about S. The formalized-concatenation field kdist allows any monotone internal budget kb(a+b+|φ|+|ψ|) ≥ a+b+|φ|+|ψ|; Pudlák's (3) has q₂(n) = 3n (Pudlák 1986, p. 179).

Which proof predicate: removing the translation gap. The Lean development allows any calculus whose K, S and modus ponens steps have polynomial cost (Lean: mp costs a + b + Mp(|φ|+|ψ|), axioms cost Ax(·)). So S can be taken as PA in Buss's sequent calculus:

• the language of bounded arithmetic L_BA = {0, S, +, ·, |x|, ⌊x/2⌋, #, ≤}, a definitional extension of PA;
• tree-like LK proofs whose initial sequents are logical axioms, Buss's BASIC axioms and PA's induction axioms;
• proof length = the length of the proof written as a string;
• Buss's dyadic numerals I_n, with |I_n| = O(log n).

For this S, one proof predicate Prf_S (Δᵇ₁ in S¹₂) satisfies H1 and H2. This rests on a printed theorem (Buss 1986, Thm 7.4(a)) plus the routine unprinted lemmas G2 (Appendix A1–A3):

• H2. Apply Buss 1986, Thm 7.4(a) to the Σᵇ₁ formula A(d, x, m) :≡ |d| ≤ m ∧ Prf_S(d, x), with Prf_S written in a fixed negation normal form (Buss's case analysis covers Σᵇ₁ formulas in that form). It gives a term t_A with S¹₂ ⊢ A(d,x,m) → (∃w ≤ t_A) Prf^{(−1)}_∅(w, ⌜A(I_d, I_x, I_m)⌝), where Prf^{(−1)}_∅ is Buss's printed proof predicate Prf^i_α (thesis p. 134) at i = −1 and α = ∅, that is, induction-free proofs from BASIC axioms; we do not use free-cut-freeness. The value of t_A has bit-length |t_A(d,x,m)| ≤ p(|d|,|x|,|m|) ≤ poly(m + |x|), using |d| ≤ m (d may be as large as 2^m). It is this value m, not |m̄|, that enters the internal budget q. Buss's induction-free S₂^{(−1)} proofs are S-proofs: BASIC is among S's initial sequents, and S¹₂ proves the inclusion. One ∃-right inference then turns the produced proof of A(I_d, I_x, I_m) into a proof of □_{I_m}(I_x). This gives the uniform S¹₂ ⊢ ∀m∀x(□_m x → □_{q(m,|x|)}⌜□_ṁ ẋ⌝), and S ⊇ S¹₂ proves it. Instantiating at numerals and evaluating the code terms costs poly(|m̄| + |φ|) (Buss 1986, Lemma 5 of §7.4).
• H1. S¹₂ is sound, so for an actual proof d of φ the statement above is true. There really is an S-proof of □_m φ of length poly(m), for the same Prf_S.

Remaining unprinted steps, all routine S¹₂ verifications of polynomial-time syntactic operations:

• (G2) the formalized H2 step, which is a package of S¹₂ syntax lemmas, not one inference:
  • Prf^{(−1)}_∅(w,y) → Prf_S(w,y) under one coding;
  • |d| ≤ m ∧ w ≤ t_A(d,x,m) → |w| ≤ q(m,|x|), turning Buss's d-dependent bound into a d-free budget;
  • the polynomial-time map appending one ∃-right inference, whose endsequent contains I_d of O(m) symbols;
  • equality of that endsequent's code with ⌜□_{I_m}(I_x)⌝. These are the same kind of lemma as Buss's §7.4 numeral and substitution facts. (H1 needs only the truth of A1, not the rest of G2: it uses the metatheoretic ∃-right.)
• (G1') H3: S¹₂ proves that the polynomial-time cut-composition of an S-proof of A → B and an S-proof of A is an S-proof of B of length ≤ a + b + O(|A| + |B|). Pudlák 1986, p. 179 states the IΔ₀+exp analogue;
• (G3) H4 at cost poly(|ḡ| + |φ|) uniformly in φ: the standard diagonal construction. The identity Sub(⌜β⌝, ⌜β⌝) = ⌜ψ⌝ is a true Δᵇ₁ sentence, so by 7.4(a) (applied to a negation normal form, plus one fixed conversion cut) it has an S-proof of size poly(|ḡ| + |φ|).
• (G5) the remaining fields:
  • bmono: the formalized ā ≤ b̄ → (□_a φ → □_b φ), at cost poly(|b̄| + |φ|);
  • necU: nec plus one outer ∃;
  • innerU, kdistU, diagU: the same constructions with the budget quantified out;
  • instance costs of kdist from numeral instantiation plus substitution evaluation, as for H2;
  • "S ⊇ S¹₂": one fixed S¹₂ proof uses finitely many Σᵇ₁-PIND instances, each a PA theorem, so each uniform S¹₂ theorem has an S-proof of constant length. All of these are routine in the same sense.

(G4), formalized Löb at poly(|P|), is not printed but is derived here from H1–H4 (Lean lobInst).

These are of the same kind as the unprinted steps in the published Friedman–Pudlák theorem. Pudlák 1998, Lemma 6.2.1 assumes the formalized bound; Pudlák 1986, Thm 3.5 omits its proofs.

Status of the results:

• As theorems about systems satisfying H1–H4 (plus polynomial costs for the polynomial forms and short numerals for the k ≥ poly + N₀ form), Theorems 1–3 are machine-checked.
• For PA in Buss's calculus, H1 and H2 rest on a printed theorem, and only the routine steps G2, G1', G3 and G5 are unprinted. A focused Grok 4.7 read of this argument returned PASS-WITH-FIXES: it verified Prf_S is Δᵇ₁, the S₂^{(−1)} ⊆ S inclusion, the t_A bound, the Lean calculus fields for tree-like proofs, and the FairBot lemma in this S. The fixes are applied.
• For PA in a Hilbert calculus, a bridge lemma (supplementary file G1) gives a polynomial-time map τ from LKB proofs to Hilbert proofs, correct in the metatheory and provably correct in S¹₂.
  • τ was SELF-CHECKED by execution: an independent Hilbert checker accepted all 1,332 translations of random, separately checked LK proofs, covering all 27 rules; after the coding was fixed (Appendix A), a re-run accepted 1,948/1,948 translations.
  • Its S¹₂ formalization is written out in full. Kimi K3 and Grok 4.7 read it: FAIL on draft 1, then PASS-WITH-FIXES on draft 3, with fixes applied. A later re-read against the fixed coding required further edits (bounded quantifiers are primitive under the fixed coding and need four Hilbert rules); they are applied in the current draft. Kimi K3 read that draft twice on 2026-10-11 (the first reply was cut off; the second covers the rest): PASS-WITH-FIXES both times, no FATAL issue, fixes applied.
  • With τ, the Hilbert proof predicate of PA over L_BA, in a Hilbert calculus with primitive bounded-quantifier rules, satisfies H1–H4 with the same routine unprinted lemmas, so, modulo those lemmas, Theorems 1–3 hold for PA in that Hilbert calculus too. Transfer to other Hilbert calculi, and PA over {0, S, +, ·, ≤} alone, are not covered.

Instance costs versus internal budgets. In H2 the cost of the proof line is I(|m̄| + |φ|), polynomial in the numeral length. The internal budget inside the box is q(m + |φ|), polynomial in m itself. The proof of Theorem 2 only ever applies q and N to the fixed-point budget g and to the fixed-point proof length, both polynomial in (h, |k̄|, |φ|), never to k. This is the main pitfall: one noticing step applied to a proof of length k would cost poly(k), and k ≥ poly(k) can never hold. The Lean statement enforces it, because the arguments of every cost function are syntactic quantities of the derivation.

3. Theorem 1: the Löb overhead

Theorem 1. Assume H1–H4 (unbounded versions). There is a function U, built from the cost functions alone, such that for every sentence P and every k: if S ⊢_{≤k} □P → P then S ⊢_{≤ k + N(k) + U(|P|)} P. If all costs are polynomial, then U(n) ≤ C(n+1)^d. Hence F_S(k,n) ≤ k + N(k) + C(n+1)^d. (Lean: LPS.lobInst, LPS.T1, LPS.T1_poly.)

Proof.

1. One instance of formalized Löb. We show S ⊢ □(□P→P) → □P with a proof whose length fL(|P|) depends on |P| only.
   • Take the fixed point ψ ↔ (□ψ → P) (H4).
   • Necessitate the fixed-point direction ψ → (□ψ → P), which has length Dc(|P|) (H1).
   • Distribute (H3) to get □ψ → (□□ψ → □P). Use the Σ₁-completeness instance □ψ → □□ψ (H2) to get □ψ → □P.
   • Propositionally: (□P → P) → (□ψ → P). By the fixed point, (□P → P) → ψ.
   • Necessitate this last proof. Its length depends on |P| only. Then distribute: □(□P→P) → □ψ → □P. Every necessitation in this step is applied to a proof whose length is a function of |P|.
2. The given proof. Let π be the k-symbol proof of □P → P. H1 gives □(□P → P) in N(k) symbols. Modus ponens with step 1 gives □P. Modus ponens with π gives P.

The Lean proof computes the exact bound.

Answer to MAIS-O1 / O10 for plain systems. F_S(k,n) ≤ k + N_S(k) + C(n+1)^d is polynomial. The k-dependence goes only through the outer noticing cost N_S. The A1 ledger, F ≲ E_S(k + d_S(O(n)) + poly(n)) + ..., charges inner necessitation and diagonalization to the k-symbol premise. They are needed only once, inside a proof whose length depends on |P| alone. Consequently:

• the strong form F_S(k,n) ≤ C(k + n^c) of A1 Conjecture 3.5 holds for every plain system with N_S(k) = O(k);
• the upper-bound side of MAIS-O1's question reduces to determining the outer noticing cost N_S (one half of MAIS-O12);
• the trivial lower bound is F_S(k,n) ≥ ℓ_S(P) for every P with |P| ≤ n and ℓ_S(P) ≤ k − C₁(n+1) (A1 Lemma 3.3 and the remark after Conjecture 3.5); whether such P exist with ℓ_S(P) close to k is open (A1).

4. Theorem 2: bounded Löb for one numeral instance

Theorem 2 (explicit form). Assume H1–H4. Let s = |φ|, j = |k̄|. Define g := Lbar(h, j, s), the explicit bound of Engine.lean. If S ⊢_{≤h} □_k φ → φ and Kbar(h, j, s) ≤ k, then S ⊢_{≤ Out(h, j, s)} φ. (Lean: LPS.bloeb.)

Proof. Steps 1–9, each checked in Lean with its exact cost:

1. Fixed point (H4): ψ ↔ (□_g ψ → φ), with |ψ| ≤ σ := Ds(j+s). We use g ≤ k, so |ḡ| ≤ j. Its proof length is d := Dc(j+s).
2. Necessitate ψ → (□_g ψ → φ). The proof has length d, so this costs N(d). This is the first noticing step; its input is d, a function of (j, s).
3. Distribute (H3): □_g ψ → □_{B1}(□_g ψ → φ), with B1 = kb(d + g + |ψ| + |□_g ψ → φ|).
4. Distribute again: □_{B1}(□_g ψ → φ) → (□_{B2} □_g ψ → □_{B3} φ), with B2 = q(g + |ψ|) and B3 = kb(B1 + B2 + |□_g ψ| + s).
5. Σ₁-completeness instance (H2): □_g ψ → □_{B2} □_g ψ. Its proof costs I(|ḡ| + |ψ|). Its internal budget is B2 = q(g + |ψ|). q is applied to g, not to k. Combining steps 3–5: □_g ψ → □_{B3} φ.
6. Monotonicity (H3), using B3 ≤ k: □_g ψ → □_k φ. With the premise □_k φ → φ: □_g ψ → φ. The fixed point then gives ψ. The length Lψ of this proof is bounded by an explicit Lbar(h, j, s). All numerals d, g, B1, B2, B3 are ≤ k, so their lengths are ≤ j. This is why g := Lbar(h, j, s) can be fixed in advance with no circularity.
7. Since Lψ ≤ g, H1 gives □_g ψ in N(g) symbols (the second noticing step, applied to g).
8. Modus ponens with step 6 gives φ.
9. The single condition on k is B3 ≤ k, which Kbar(h, j, s) ≤ k guarantees.

Theorem 2 (polynomial form). If all cost functions are polynomially bounded, there are C, d such that for all h, k, φ: if S ⊢_{≤h} □_k φ → φ and C(h + |k̄| + |φ| + 1)^d ≤ k, then S ⊢_{≤ C(h+|k̄|+|φ|+1)^d} φ. (Lean: LPS.T2_poly, via monotonicity of the bounds and closure of polynomially bounded monotone functions under +, ·c and composition, Poly.lean.)

Because |k̄| = O(log k), the condition holds for all k ≥ C'(h + |φ| + 1)^{d} + N₀. This T2 form is not stated in Lean; Lean proves the agent version (T3_poly, using ShortNumerals) by the same split.

Explicit degrees (Lean-checked). Write q(x) ≤ c_q(x+1)^{d_q} for the internal budget of H2, N(x) ≤ c_N(x+1)^{d_N} for the noticing cost of H1, and d_Dc, d_Kd, d_I, d_Mo for the degrees of Dc, Kd, I, Mo. Gt(j, s) is the explicit h-free part of the bounds of Engine.lean, a fixed sum of cost functions at numeral length j and formula size s. C_G is the leading constant of the joint bound in T3_joint.

• T2_explicit: threshold A·(h + Gt(|k̄|,|φ|) + 1)^{d_q}, output (c_N+1)·(h + Gt + 1)^{d_N}, with A closed in the cost constants (A = 3c_q + 12 for Pudlák's kb(n) = 3n).
• T3_poly_explicit: cooperation for k ≥ 2^{d_q+1}·A·(L + Gt(2ℓ,2ℓ) + 1)^{d_q} + N₀.
• Jointly (Ds, Bz, Mp, Ax, kb linear) the degree is degG·d_q with degG = max(1, d_Dc, d_Dc·d_N, d_Kd, d_I, d_Mo) (T3_joint).
• The PA values of d_q, d_N, … are not computed. N₀ in T3_poly_explicit and T3_joint is existential (it comes from ShortNumerals), and so is C_G in T3_joint. The hypotheses include linear kb (kb(x) ≤ c_kb·x + c'_kb; general A = c_kb(c_kb + c'_kb + c_q + 1) + c'_kb) and d_q, d_N ≥ 1.

Short numerals (Lean-checked). The threshold forms say something only with short numerals (binary or dyadic, |k̄| = O(log k)): Theorem 2's condition and Theorem 3's threshold contain |k̄|, and the k ≥ C'(L+ℓ+1)^{d'} + N₀ form has the Lean hypothesis LPS.ShortNumerals (T3_poly, T3_poly_explicit, T3_joint), plus polynomial costs (PolyCosts). With unary numerals Theorem 2 is vacuous, not false. short_of_log_explicit: |k̄| ≤ a·log k + b implies ShortNumerals with N₀ = 2^{C(a+b+1)^d(d+1)^{d+1}}; not_short_of_unary: unary numerals refute it; T3_poly_binary combines the two. The explicit N₀ is for a given ShortNumerals query (C, d); it does not make the N₀ of T3_poly numeric.

Corollary (sanity check, φ = ⊥). If S is consistent, every h-symbol proof of Con_S(k) = (□_k ⊥ → ⊥) has C(h + |k̄| + |⊥| + 1)^d > k. So ℓ_S(Con_S(k)) ≥ (k/C)^{1/d} − O(log k). This is the Friedman–Pudlák lower bound shape (Pudlák 1998, Thm. 6.2.3) with exponent 1/d. Our argument is the Friedman–Pudlák argument with ⊥ replaced by an arbitrary φ. (Lean: LPS.con_lower.)

Relation to Critch / A1 / P2 and cousin_it.

• Critch's PBLT and the A1/P2 repairs are uniform. From S ⊢ ∀k(□_{f(k)}p(k) → p(k)) they derive S ⊢ ∀k>k̂ p(k). This needs budget comparisons proved inside S uniformly in k (P2's internal regularity and certificates). P2 showed that Critch's published PBL theorem is false as stated under its permissive convention for representing budgets, and repaired it with internal certificates; Critch has since corrected the hypothesis (post on X, 2026-07-28, per Levine 2026).
• Run with its convenience choice g = 2λ (λ(k) := |k̄| + 1, the numeral-length budget), P2's proof needs C + 2N + |k̄| ≤ 2|k̄| + 2, where N is the length of the S-proof of ∀k>K ψ[k] (P2 l. 298–303; line numbers of P2 refer to papers/P2/MAIS-P2.tex in github.com/Math-for-AI-Safety/MAIS at commit 1cb9f003). This forces k ≥ 2^{C+2N−2}, a threshold exponential in N. This is our derivation; P2 prints no threshold. With a root-type g, P2's general repair (repaired theorem l. 237–253, proof l. 255–305; the certificates it needs, l. 112–135) gives a polynomial threshold of the same degree (Proposition U, below; written; Grok 4.7 PASS-WITH-FIXES, fixes applied; Gemini 3.1 Pro PASS on the revised text).
• Proposition U (P2's general repair, written, read by two other-provider models). With auxiliary budget g(k) = ⌊(k/M)^{1/D}⌋, MAIS-P2's general repair gives k̂ ≤ c·(L + poly(|p|) + 1)^D + poly(|p|) + K₀, for linear kb, where D is the degree of H2's internal budget q, the same degree that governs our threshold (T2_explicit, T3_poly_explicit). It needs five routine unprinted uniform-in-k lemmas (U1–U5) that the per-budget route avoids. One other-provider read (Grok 4.7) returned PASS-WITH-FIXES with two MAJOR gaps (the σ size bound in the second distribution; an S¹₂ evaluation lemma for g); the fixes are applied, and Gemini 3.1 Pro read the revised text: PASS, no findings. So "polynomial instead of exponential" does not separate our route from P2's. Our premise is strictly weaker (Proposition P2′: a FairBot with a consistency tripwire has short per-budget fairness proofs, yet S proves no uniform fairness or cooperation statement for it); P2's conclusion is stronger where it applies (one S-proof for all k > k̂).
• Theorem 2 is per instance. The only uniform facts it uses are the fixed theorems behind H2 and H3, which are standard derivability conditions. All budget comparisons are between specific numerals.
• For agents, per-instance is all that is needed: whether FairBot_k cooperates depends only on whether one sentence φ_k has a ≤k-symbol proof.
• cousin_it (LessWrong, 2012) sketched a per-instance bounded Löb with requirement f(n) ≫ exp(g(n)). Theorem 2 replaces that with a polynomial and proves it.
• That bounded Löb should follow from Pudlák's consistency-length techniques was anticipated in print. Barász et al. 2014 (p. 5) write that bounded variants of Löb's theorem 'seem readily derivable via currently available techniques in logic, such as those in [Pudlák 1996]'. cousin_it (2012) called bounded Löb 'a simple corollary' of Pudlák 1986, and sketched it by applying the bounded second incompleteness theorem to T + ¬S. Theorem 2 carries out that expected argument with polynomial bounds and all costs tracked. Pudlák 1996 (Collegium Logicum 2, 65–86; preprint on Pudlák's home page) surveys the finite-consistency bounds and states no Löb-type result, bounded or unbounded. Its Theorem 13(i) and the proof sketch after it are the Friedman–Pudlák lower bound for Con_T(n), the case φ = ⊥.
• Pudlák 1986, Thm 3.1 is the case φ = ⊥ (with the conclusion read contrapositively). Theorem 2 is its generalization to every φ; for prior machine-checked work see the next bullet.
• Duclaux, Formenti, Cobben, Schölkopf and Jin (2026; Lean repository, Base/BoundedGL.lean, Base/Loeb.lean) already machine-check a single-budget bounded Löb theorem for arbitrary φ (BoundedGL.bloeb, pblt_engine). Given a proof of □_f φ → φ of length pm and f ≥ 8192·(pm + |φ| + log₂ f + 8), it yields a proof of φ of length ≤ 4096·(pm + |φ| + log₂ f + 8). Their proof is against an abstract interface whose derivability costs are fixed and linear (necessitation adds the box size; formalized Σ₁-completeness has internal budget a + |□_a φ|). A Gödel-coded PA predicate does not satisfy those costs, and their main branch lists the arithmetized PA model as open. Public side branches of the same repository (colomban-arith-u10 and colomban-recost, 2026-09-16; colomban-route-b, active 2026-10-10; commits by C. Duclaux) build that model on the Foundation library: PA with two action constants and a box bounded by derivation length in symbols. There they prove in Lean bounded inner necessitation with a polynomial expansion of degree 16 (ArithS.boundedInnerNec_sixteen; stated for the budgets ‖k‖³ of Critch's argument, with a constant depending on the formula; route-b also has ArithS.closedInnerNec_sixteen, for closed sentences at every budget, again with a constant depending on the sentence), Critch's uniform parametric bounded Löb theorem (ArithS.pblt), and FairBot (Dupoc) self-cooperation at every sufficiently large budget (ArithS.dupoc_self_coop). Their thresholds are existential and not quoted. Their box names a sentence by the unary numeral of its Gödel code, so its size is exponential in the formula's length (their source notes that every proof of it is at least that code long, so a bound linear in the formula's length is unsatisfiable); it therefore does not meet our polynomial costs, and combining the two developments would need a box with short sentence names. Theorem 2 is the same per-budget argument generalized to arbitrary polynomial cost functions (in particular a polynomial internal budget q, as Buss 1986 Thm 7.4(a) gives for PA), with the numeral bookkeeping this needs. In the sources we could read we found that general form stated nowhere.
• Per their zbMATH reviews (we have not read the papers), Montagna 1992 and Hájek–Montagna–Pudlák 1993 state results about the speed-up of unbounded rules (A*/B*, Prov(φ)/φ). HMP's method uses bounded consistency statements Con(z̄), so a bounded Löb lemma could appear inside it. Montagna's reference list cites Buss 1986 but not Pudlák 1986 or Friedman, which makes a Friedman–Pudlák-style single-numeral statement there less likely. We have not read them; they could contain Theorem 2.

5. Theorems 3 and 4: the cooperation threshold

Agents. A fair family (Lean FairFamily cL e; fairness is required separately at each budget k) consists of sentences φ_k ("the agents cooperate at budget k") and the actual outcome coop(k), with:

• (search semantics) coop(k) iff S ⊢_{≤k} φ_k. Used only for the floor.
• (truth) φ_k is true iff coop(k); S is sound.
• (fairness) S ⊢_{≤ L + cL(|k̄|+1)^e} □_k φ_k → φ_k.
• (size) |φ_k| ≤ ℓ + cL(|k̄|+1)^e.

FairBot_k self-play is a fair family. By Kleene's recursion theorem, let e be the code of the program F that on input x enumerates all strings of at most x symbols in a fixed order, checks each with the polynomial-time proof checker for S against the sentence θ(x̄), and outputs C if one passes (D otherwise). Here θ(x) := "U(e, x) = C", with U a Σ₁ definition of the output of the universal machine.

Set φ_k := θ(k̄) and coop(k) := F(k) = C. The two copies of FairBot_k are F run on k, and they play the same move.

• The search semantics hold by construction.
• The truth clause holds because U defines the output correctly.
• Size: |φ_k| ≤ |θ| + O(|k̄|), and |θ| = O(ℓ) since θ contains the numeral of e.
• Fairness: PA proves the single program-correctness statement ∀x(□_x θ(ẋ) → θ(x)). "If some string of length ≤ x is an S-proof of θ(x̄), the enumeration reaches one, and the first one found makes F output C." This is one induction along the enumeration. Its length L depends on e and the formalization of U, not on k. Instantiating at k̄ and evaluating the code term ⌜θ(k̄)⌝ costs poly(|k̄| + |θ|) (Pudlák 1998, Thm. 6.1.4). This is the (fairness) clause, with e the degree of that evaluation.

This point is essential: the search must be verified by one uniform induction, not unrolled for each k. With unrolling, the fairness proof would grow with k and the threshold argument would fail.

Theorem 3. Assume H1–H4 with polynomial costs and binary numerals. For all cL, e there are C', d', N₀ such that every fair family cooperates at every k ≥ C'(L + ℓ + 1)^{d'} + N₀. And it defects at every k < |φ_k|, since no proof is shorter than its conclusion. (Lean: LPS.T3, LPS.T3_poly, LPS.floor.)

Proof. Apply Theorem 2 (polynomial form) to the fairness proof, with h = L + cL(|k̄|+1)^e. Under the threshold hypothesis it yields a proof of φ_k of at most k symbols, so the search succeeds (search semantics). The Lean proof goes through soundness and the truth clause instead; either route works. Soundness is what makes "φ_k is proved" mean "the agents really cooperate".

Note: the uniform fairness proof needs PA to prove that the bounded enumeration (2^{O(x)} strings) terminates. That needs exponentiation to be total. So weak plain systems (IΔ₀ without exp) are excluded; PA is fine.

Answer to the second question (MAIS-O1, O17) for plain systems. k̂* ≤ C'(L + ℓ + 1)^{d'} + N₀: polynomial in description length plus fairness-proof length. For FairBot_k self-play, L is a fixed constant determined by the code e and the chosen universal machine U, so k̂*(FairBot) < ∞ for a standard arithmetized system (for PA in Buss's calculus, modulo the routine unprinted steps G2, G1', G3, G5 of Section 2). This is the finiteness half of MAIS-O16, which Duclaux et al. have already machine-checked for their own arithmetized PA (Section 4); here it comes with a polynomial bound. The certified numerical interval asked for there is not computed: the degrees and the leading constant are explicit in the cost constants (Explicit.lean); C_G and N₀ are only shown to exist, and the cost constants' numeric values for a concrete PA formalization are not computed. For families of agents whose correctness proofs are polynomial in their size (for example FairBot padded with ℓ no-op instructions), L = poly(ℓ) and k̂* = poly(ℓ). This last claim is a remark: L's growth is a property of the formalization of U, which we do not formalize.

Pairs of different agents. For A_k, B_k with fairness legs S ⊢ □_{G_A(k)}(B_k(A_k)=C) → A_k(B_k)=C and symmetrically, take φ_k := A_k(B_k)=C ∧ B_k(A_k)=C. From a ≤k proof of φ_k, conjunction elimination gives ≤ k + O(|φ_k|) proofs of each conjunct, formalized uniformly at polynomial instance cost. So if G_A(k), G_B(k) ≥ k + c|φ_k| (the agents search a slightly larger budget than k), then S proves □_k φ_k → φ_k in poly(L_A + L_B + ℓ + |k̄|) symbols, and Theorem 3 applies (the floor is not needed). This is an unformalized remark.

Description length alone does not suffice: delayed FairBots (a remark). Theorem 3's bound is in ℓ + L, and the dependence on L cannot be dropped, for a trivial reason. A delayed FairBot DF_N on input k outputs D if k < N; otherwise it acts like FairBot_k on its own code (it outputs C iff some string of at most k symbols is an S-proof of φ_k := "DF_N outputs C on input k"). N is stored in binary, so the code length is ℓ₀ + O(log N). DF_N defects at every k < N by construction; no proof complexity is used. For k ≥ N, S proves once FairBot's correctness statement with one comparison added; instantiating it at N̄ and k̄ and proving k ≥ N on binary numerals costs poly(|k̄| + |N̄|). So S proves □_k φ_k → φ_k in L₀ + poly(|k̄| + |N̄|) symbols, and Theorem 2 (per budget; no fairness for all k is needed) gives cooperation at every k ≥ N once N is large. Hence k̂*(DF_N) = N for all large N, and over families of cooperating pairs no polynomial in description length alone bounds k̂*: Levine's question, as quoted in the Summary, has this trivial negative answer. Replacing "k < N" by "a hard-coded program p has not halted within k steps" gives defection below p's running time T and cooperation at every k ≥ poly(T), since S proves "p halts within T steps" in poly(T) symbols; the code length is ℓ₀ + |p|. So the largest threshold among cooperating pairs of code length ℓ is not bounded by any computable function of ℓ. The same agents show that L is needed in Theorem 3: Theorem 3 gives k̂* ≤ C'(L + ℓ + 1)^{d'} + N₀ while k̂*(DF_N) = N with ℓ = O(log N), so every fairness-proof family for DF_N that meets Theorem 3's premise has L ≥ N^{1/d'}/C' − O(log N). (Directly: at k < N, φ_k is false and refutable by a short computation, so a fairness implication there amounts to a proof of ¬□_k φ_k, which Theorem 2 prices.) These are written remarks for PA, at the level of the FairBot remark above, not machine-checked. The delayed-FairBot observation came from an internal adversarial check of draft 6.

An idle consistency check (Theorem 4). Theorem 4 shows the same kind of delay arising with no hard-coded delay. A cautious FairBot CF_n on input k first enumerates all strings of at most n symbols and outputs D if one is an S-proof of ⊥; otherwise it acts like FairBot_k on its own code: it outputs C iff some string of at most k symbols is an S-proof of φ_k := "CF_n outputs C on input k". Its code is a fixed program with n̄ appended as data, so its length is ℓ_n = ℓ₀ + O(log n). S proves once that CF_n outputs C only after the check has passed, so S ⊢ φ_k → Con_S(n) in G₀ + poly(|k̄| + |n̄|) symbols, where Con_S(n) := □_n⊥ → ⊥ uses the same box and symbol count as H1–H4 (G₀ includes one fixed S-proof that the agent's checker decides exactly Prf_S; supplementary file SEPARATION, Section 3). A proof of φ_k of at most k symbols therefore yields a proof of Con_S(n) of poly(k + |n̄|) symbols, and Theorem 2 at φ = ⊥ (Lean con_lower, the Friedman–Pudlák shape) bounds such proofs from below.

Theorem 4. Assume H1–H4 with polynomial costs. For all cL, e there are C, d such that the following holds for every guarded family: sentences φ_k, outcomes coop(k), a sentence β, a number n and a length G such that coop(k) gives S ⊢_{≤k} φ_k, S ⊢_{≤ G + cL(|k̄|+|n̄|+1)^e} φ_k → (□_n β → β) for every k, and S proves no β. C and d depend only on the system, cL and e. If such a family cooperates at budget k, then n < C(k + |k̄| + G + |n̄| + |β| + 1)^d. (Lean: LPS.guard_lower, LPS.guard_floor; LPS.separation combines it with Theorem 3, binary numerals included, for an agent family given by a fair and a guarded presentation with the same outcomes.)

For CF_n in PA (β = ⊥, G = G₀) this gives (n/C)^{1/d} − O(log n) ≤ k̂*(CF_n) < ∞. Finiteness holds by Theorem 3, with fairness proof length L_n = L₀ + ‖Con_S(n)‖ + poly(|n̄|). So k̂*(CF_n) ≥ 2^{Ω(ℓ_n)} for large n. That growth in code length is not the point, and it understates what is possible: delayed FairBots already reach k̂* = N with code O(log N), running-time delays beat any computable function of code length, and the same holds for CF_n with n given by a short program. What Theorem 4 adds: CF_n's extra code is a consistency check that never fires in the standard model (S is consistent), yet any proof of cooperation must contain a proof of Con_S(n), so the threshold is pushed to at least n^{Ω(1)} by proof complexity alone. It is a statement about how proof-length lower bounds propagate into cooperation thresholds, not an answer to Levine's question. It is shown for PA (the fairness proof needs exponentiation total, as for FairBot above), not for the weak systems MAIS-O1 names.

The upper side: k̂*(CF_n) ≤ n^{O(1)} in PA. Pudlák 1986 (Thm 5.5, extended to PA in the remark on p. 192) and Freund–Pakhomov 2020 (Thm 3.6, for Con(PA + Con*(PA))↾n, which implies Con_PA(n) by one fixed proof) give PA-proofs of Con_PA(n) of n^{O(1)} symbols, for formalizations they do not print. Polynomial-size proofs of Con_PA(n) are therefore not ours. Monroe 2026 (arXiv 2604.27787) studies when a sound S ⊇ S¹₂ has polynomial-size proofs of Con_{S+φ}(n) for true φ, and how this relates to simulation between theories; his Thm 3.2 assumes polynomial proofs of Con_S(n). It states no bounded Löb overhead and no cooperation threshold. The supplementary files UPPER, UPPER-ASM1 and UPPER-THETA carry this over to our □_n: for S = PA in Buss's calculus, S ⊢ Con_S(n) in at most C(n+1)^{12} symbols (C not computed). The route:

• Freund–Pakhomov's Cor 3.5 (PA-proofs of F_ε0(m)↓ of polynomial size, a statement about one fixed formula, not about proofs) is re-proved in a Hilbert calculus without a primitive biconditional, in at most C(m+2)³ symbols, by Solovay's construction (Pudlák 1998, Thm 3.2.3) applied to Gentzen's jump (UPPER-ASM1). It uses their Lemmas 3.1 and 3.2 as fixed theorems and none of their length claims. A meta-level simulation moves these proofs into Buss's calculus at quartic cost (UPPER).
• One fixed theorem, S ⊢ ∀a(F_ε0(2a + c)↓ → ¬□_a⊥), links them to our box (UPPER-THETA). It is proved from Freund's Thm 3.13 (arXiv 1512.05122): a primitive recursive translation, provably correct in PA, takes every S-proof of ⊥ of at most a symbols to a refutation in Freund's printed finite calculus with cut rank at most 2a + c, which his theorem excludes once F_ε0(2a + c) is defined.

Hence L_n ≤ n^{O(1)} and, with Theorem 4, k̂*(CF_n) = n^{Θ(1)}. Along CF_n, k̂* ≥ (L_n + ℓ_n)^δ for a fixed δ > 0, so Theorem 3's polynomial bound in ℓ + L cannot be improved to (ℓ + L)^{o(1)} along this family. The exponents are not matched, since no degrees are computed. Delayed FairBots give the same conclusion (their fairness proofs at k < N reduce to Con_S(N + O(log N))), so it is not specific to Theorem 4 either. Check level: written, SELF-CHECKED; each of the three files had one other-provider read (Kimi K3, PASS-WITH-FIXES, no FATAL issue, fixes applied; UPPER-THETA's revised parts also had a GPT-6 Astra read, PASS-WITH-FIXES, fixes applied; all three files were edited after their last read, and those edits had a second Kimi K3 read, PASS-WITH-FIXES with minor fixes only, applied); nothing here is machine-checked. The argument rests on named reading assumptions: that a primitive recursive recoding carries the translated proofs into the Gödel numbering of Freund's preprint, which is not printed, with the same height, term depth and cut rank (R-code), and three readings of misprints or standard facts (R-ax, R-var, R-fix). It also rests on cited results not re-verified here: Freund's Thm 3.13 and Lemmas 3.8 and 4.7 (an arXiv preprint; its refereed status is unknown to us), and Freund–Pakhomov's Lemmas 3.1 and 3.2 and their domination of primitive recursive functions by the fast-growing hierarchy (p. 7). As printed in arXiv v2, the formula J′ in Freund–Pakhomov's proof of their Prop 3.4 is refutable (a bounded ∃ over the empty range at β = 0); the slip is repaired in one line, and their results stand (UPPER-ASM1, Section 1). For the Hilbert calculus of Section 2 the upper side holds only modulo two further unprinted steps (UPPER, Section 4).

The PA instance is a written argument at the level of the FairBot remark above (supplementary file SEPARATION). Prior uses of a finite-consistency guard against bounded proof search: MAIS-P2's refutation of Critch's PBL theorem (a guard ¬□_{F(k)}⊥ inside the budget function; P2's refutation of the cooperation theorem, where G-fair agents defect at every k, uses a diagonal proof search instead), and Duclaux et al.'s design notes, which price certificates of a failed search at the agent's own budget k by Pudlák's k^ε bound. Neither fixes the guard size as a code parameter of an agent that still cooperates at large budgets. Given those devices, Theorem 4 is a short observation.

Tsimerman's IPAM talk (2026-09-03). We read the auto-generated transcript of the public recording (not the video or board) of J. Tsimerman's talk 'Some new results in Open Source Game Theory'. Writing DUPOC_k for bounded FairBot (cooperate iff a proof of at most k symbols shows that the opponent cooperates) and CUPOD_m for its dual (defect iff a proof of at most m symbols shows that the opponent defects), the talk states Critch's bounded Löb theorem and DUPOC self-cooperation at large budgets without explicit parameters, and announces two new results: DUPOC_k defects against CUPOD_m when m ≥ k + C log k (a bounded-Löb argument), and CUPOD_m also defects against DUPOC_k when m ≥ k^c for a large constant c (said to be based on Pudlák's polynomial proofs of finite consistency; no proof given). It gives no proof-length bound for Löb's theorem and no growth law for thresholds; it overlaps with Theorems 1–4 only in using Pudlák's finite-consistency bounds. No slides or paper are available.

6. Non-vacuity

The hypotheses are jointly satisfiable with polynomial costs, short numerals and an unprovable sentence (Lean: VerumModel.nonvacuous; boxes read as "true", Pf n φ := φ true and |φ| ≤ n). This rules out the theorems following from contradictory fields. The model is degenerate (numeral length 0, every box true). It does not stress-test the numeral bookkeeping, and it is not a model of a real proof predicate. A second consistency model has real binary numeral lengths |k̄| = ⌊log₂k⌋ + 1 (BinModel.nonvacuous_binary); its boxes are still read as 'true', so it is not a model of provability either. The intended model is PA with the natural bounded-provability predicate; Section 2 gives the citations.

7. What is not covered

• Abbreviation systems (MAIS's PA_bin). A k-symbol proof with abbreviations can expand to 2^{Ω(k)} symbols. Pudlák's H1 is stated for the expanded proof, so N_S(k) polynomial is not available as stated. The missing lemma: "the proof relation of PA_bin (with def records) has polynomial-size true instances in the abbreviated length". Checking compressed proofs without expanding them is the issue.
• Enderton's tautology axioms. With all tautologies as axioms, the axiom set is coNP, and Pudlák's Thm. 6.1.4 requires an NP (or P) axiom set. A bridge (prove Taut(⌜τ⌝) from the tautology instance τ[pᵢ := (v)ᵢ = 1] plus polynomial Tarski clauses) should restore H1. We do not prove it here.
• What the machine check covers. Lean checks Theorems 1–4 for an abstract structure whose fields are H1–H4; it does not check that PA satisfies them. That PA does is a written argument (Section 2, Appendix A), read by other AI models, not machine-checked. The full proofs of the routine lemmas A1–A7 have one other-provider read (Gemini 3.1 Pro: A4–A5 PASS; A1–A3 and A6–A7 PASS-WITH-FIXES, fixes applied; two A1–A3 findings rejected, SELF-CHECKED).
• Hilbert-calculus instance. Only a Hilbert calculus with primitive bounded-quantifier rules over L_BA is covered, and its bridge (supplementary file G1) has one other-provider reader in its current form (Kimi K3, two reads, PASS-WITH-FIXES, fixes applied); other Hilbert calculi and PA over {0, S, +, ·, ≤} are not covered.
• Unread prior art. Montagna 1992 and Hájek–Montagna–Pudlák 1993 (paywalled) could contain Theorem 1 or Theorem 2. Pudlák 1996 has been read and contains neither.
• The uniform route gives the same order. P2's general repair with a root-type auxiliary budget also gives a polynomial threshold of the same degree in L (Proposition U; written; Grok 4.7 PASS-WITH-FIXES, fixes applied; Gemini 3.1 Pro PASS on the revised text). What the per-budget route adds is a weaker premise and no uniform-in-k certificates, not a better growth law.
• Agents covered. The Lean theorem covers families with one cooperation sentence and fairness at budget k (FairBot self-play). Pairs of different agents, polynomiality in description length alone (padded FairBots) and delayed FairBots are unformalized remarks. Theorem 4 covers guarded families; that cautious FairBots are one is a written argument. No Lean model exhibits a guarded family that cooperates (the Section 6 models are degenerate), so Lean checks the bookkeeping of Theorem 4, not that an instance exists.
• No numbers. The degrees are explicit in the cost constants, but the PA values of those constants, and the constants C_G and N₀, are not computed. No numerical k̂* is claimed.
• Uniform PBL. Theorem 2 does not give A1/P2's uniform conclusion S ⊢ ∀k>k̂ p(k).
• Theorem 4's PA instance. That cautious FairBots meet the guard and fairness hypotheses in PA rests on unformalized program-correctness statements for U, as for FairBot, including that the agent's checker decides exactly Prf_S under the symbol count of □_n. Both outside reads are by one provider (Kimi K3); the second gave PASS-WITH-FIXES, with the accepted fixes applied in SEPARATION. It is shown for PA, not for the weak systems MAIS-O1 names (the delayed FairBots have the same gap on the cooperation side). The matching upper side k̂*(CF_n) ≤ n^{O(1)} is a written argument (supplementary files UPPER, UPPER-ASM1, UPPER-THETA; SELF-CHECKED, one Kimi K3 read per file, PASS-WITH-FIXES, fixes applied, plus a GPT-6 Astra read of UPPER-THETA's revised parts; each file was edited after its last read, and those edits had a second Kimi K3 read, PASS-WITH-FIXES with minor fixes only, applied), not machine-checked. It rests on the reading R-code of the unprinted numbering of Freund's preprint (arXiv 1512.05122), on the readings R-ax, R-var and R-fix, and on cited results not re-verified here (Freund's Thm 3.13 and Lemmas 3.8 and 4.7, a preprint of unknown refereed status; Freund–Pakhomov 2020, Lemmas 3.1, 3.2 and p. 7). It is shown for PA in Buss's calculus; for the Hilbert calculus of Section 2 it needs two further unprinted steps. Degrees: S ⊢ Con_S(n) in C(n+1)^{12} symbols, so L_n ≤ C₁(n+1)^{12}; for large n, n^{1/(2d₄)} ≤ k̂*(CF_n) ≤ n^{24d′} and k̂*(CF_n) ≥ (L_n + ℓ_n)^{1/(24d₄)}, where d′ is Theorem 3's degree and d₄ is Theorem 4's (its d). The PA values of d′ and d₄, and the constants C and C₁, are not computed.

Appendix A. The routine S¹₂ lemmas for the PA instance (statements and proof outlines)

Full proofs. Full written S¹₂ proofs of A1–A7 are in the supplementary files A1-A3, A4-A5 and A6-A7, on one fixed coding (Buss 1986 §7.1 bracketed preorder proof code, Buss's printed term/formula codes, Takeuti bound-variable syntax, identity axioms F ⊢ F for every formula). Check level: SELF-CHECKED (written by AI agents, with executable checks of A4 in a sandbox). One different-provider read (Gemini 3.1 Pro): A4–A5 PASS; A1–A3 and A6–A7 PASS-WITH-FIXES, fixes applied; two findings on Buss's tree definitions rejected as misquotations, after checking the printed text (the rejection is SELF-CHECKED; no other reader has seen it). The statements below are outlines. The full proofs fix the following conventions and details (none changes a field of the Lean structure LPS):

• Lengths are bit lengths of the Buss code everywhere (Pf, inside □, sz φ := |⌜φ⌝|); "k-symbol proof" means ≤ k bits.
• nl(m) := max_{j≤m} |Num(j)|, the monotone envelope, as in Section 1.
• Code functions occur in S-formulas only through their Σᵇ₁ graphs (Sb, Imp, …), not as terms (β in A6, ⌜□_ṁ ẋ⌝ in H2).
• A1 is literal for one rendering of Buss's omitted local checks (extra assumption E1). E1 has been checked case by case against Buss's printed proof of 7.4(a), pp. 136–140 (one reader with the page images, plus one other-provider read, Kimi K3, 2026-10-11, no FATAL issue; the sub-derivations Buss omits are checked only by the inference types they need). We use only the induction-free predicate Prf^{(−1)}_∅ and do not need free-cut-freeness. For it every case goes through, once the inference rules Buss leaves unwritten are written out; the bounded-∀ case (Buss's case (d)) needs one non-atomic cut, a construction we supply at the level of detail of Buss's text.
• Formulas given to 7.4(a) are in negation normal form (for H2 by the choice of the form of Prf_S). Where a formula is not, 7.4(a) is applied to its negation normal form, followed by one cut against a fixed logical proof of the conversion, instantiated at the numerals; this adds a part linear in the numeral sizes and leaves every bound polynomial of the same form.
• The H2 instance must also evaluate the budget term; q(n) := q′(n, n).
• The linear costs of mp, axK, axS, A4 need identity axioms for every formula (part of S); with atomic-only identity axioms they are quadratic, which the Lean fields also allow.
• kdist needs the budget comparison inside the uniform sentence and three evaluation instances; kb(n) = c′·n.
• A5's constant depends on the S¹₂ theorem and its derivation; deriving each PIND instance from IND costs O(|A|²). Remaining open: claims Buss leaves unproved (BU1–BU3); E1 and substitution invariance (now proved for every rule, with the sharp eigenvariable side condition and with axiom templates coded using bound-variable placeholders) have one reader each plus one other-provider read each (Kimi K3, 2026-10-11, no FATAL issue); numerical degrees not computed; the current draft of the Hilbert bridge G1 (revised against the fixed coding) has one other-provider reader (Kimi K3, two reads).

Throughout:

• S is PA in Buss's sequent calculus over L_BA, as in Section 2. Proofs are strings over a fixed finite alphabet, and |w| is the string length.
• "Polynomial-time" maps are Σᵇ₁-defined in S¹₂, and their stated properties are proved in S¹₂ by Σᵇ₁-LIND on the length of the input. This is the standard method of Buss 1986, Ch. 2–3.
• Each lemma below is a ∀Δᵇ₁ statement about one explicit polynomial-time map.

A1 (inclusion; part of G2). S¹₂ ⊢ ∀w∀y (Prf^{(−1)}_∅(w, y) → Prf_S(w, y)). Outline. Both predicates check the same local inference rules. Every initial sequent allowed by Prf^{(−1)}_∅ (logical axioms, BASIC) is allowed by Prf_S. With one Gödel numbering, the implication is sharply bounded line by line.

A2 (d-free budget; part of G2). There is a polynomial term q such that S¹₂ ⊢ ∀d∀x∀m∀w (|d| ≤ m ∧ w ≤ t_A(d,x,m) → |w| ≤ q(m, |x|)). Outline. Every L_BA term t satisfies |t(ā)| ≤ p_t(|ā|) for an explicit polynomial p_t, provably in S¹₂, by induction on t. Then substitute |d| ≤ m and |m| ≤ m.

A3 (∃-append; part of G2). There is a polynomial-time map E(w, d, x, m) with S¹₂ ⊢ Prf_S(w, ⌜A(I_d, I_x, I_m)⌝) → Prf_S(E(w,d,x,m), ⌜∃d′(|d′| ≤ I_m ∧ Prf_S(d′, I_x))⌝), and S¹₂ ⊢ |E(w,d,x,m)| ≤ |w| + c·(|d| + |x| + |m| + 1); hence |E(w,d,x,m)| ≤ |w| + c·(2m + |x| + 1) when |d| ≤ m. Outline.

• E appends one ∃-right inference with eigenterm I_d. Its endsequent is the displayed code, since substituting I_d for d′ in the matrix gives A(I_d, I_x, I_m).
• Correctness is one local check plus the code identity Sub(⌜|d′| ≤ I_m ∧ Prf_S(d′, I_x)⌝, ⌜d′⌝, ⌜I_d⌝) = ⌜A(I_d,I_x,I_m)⌝ (substitution into the matrix), which is a Δᵇ₁ fact about a polynomial-time function. The substitution lemma is stated for a non-empty substituted term, which ⌜I_d⌝ is.
• The length bound uses |I_d| = O(|d|) ≤ O(m).

Consequence (H2). Combining Buss 7.4(a) with A1–A3: S¹₂ ⊢ ∀m∀x (□_m x → □_{q′(m,|x|)} ⌜□_ṁ ẋ⌝) for a polynomial term q′. The instance at m̄, ⌜φ⌝ costs a constant (the S-proof of this S¹₂ theorem, via A5), plus numeral instantiation, plus evaluation of the code terms. The evaluation identities are true Δᵇ₁ sentences whose 7.4(a)-proofs (via negation normal form and one fixed conversion cut) have size poly(|m̄| + |φ|).

A4 (cut-composition; G1′). There is a polynomial-time map K(w₁, w₂, u, v) with S¹₂ ⊢ Prf_S(w₁, ⌜u → v⌝) ∧ Prf_S(w₂, u) ∧ Fml(v) → Prf_S(K(w₁,w₂,u,v), v) ∧ |K(w₁,w₂,u,v)| ≤ |w₁| + |w₂| + c(|u| + |v|). The hypothesis Fml(v) (or Fml(⌜u→v⌝) ∧ Fml(u)) is needed: Buss's Prf also accepts multi-formula succedents, and without it the statement fails (counterexample in supplementary file A4-A5, §2.10). Outline. K builds the tree that cuts ⊢ u→v and ⊢ u against the fixed derivation u→v, u ⊢ v (initial sequents u ⊢ u, v ⊢ v, one →-left). Correctness is a local check at the five new nodes; the subtrees are embedded unchanged (Lemma TE, supplementary file A1-A3). From A4 and A5, H3 (kdist) follows with kb(n) = c′·n, and its instance cost is numeral instantiation plus evaluation, as in H2.

A5 (S ⊇ S¹₂, with constant overhead). For each S¹₂ theorem ∀z̄ θ(z̄) there is a fixed S-proof of ∀z̄ θ(z̄). Outline. A given S¹₂ proof uses finitely many BASIC axioms and Σᵇ₁-PIND instances. Each PIND instance is provable in PA from ordinary induction (in the definitional extension L_BA). Replacing each instance by such a proof gives a fixed S-proof.

A6 (diagonal lemma with polynomial cost; G3). For each numeral g and sentence φ (the bound variable of β chosen fresh):

• let β(y) :≡ (□_{ḡ} Sub(y, y) → φ) and ψ :≡ β(⌜β⌝), so |ψ| ≤ Ds(|ḡ| + |φ|) with Ds linear;
• S ⊢ ψ ↔ (□_g ψ → φ) with a proof of size poly(|ḡ| + |φ|). Outline. The only non-logical step is the identity Sub(⌜β⌝, ⌜β⌝) = ⌜ψ⌝. It is a true Δᵇ₁ sentence of bit-length O(|ḡ| + |φ|), so 7.4(a) and A1 give it an S-proof of polynomial size. Equality substitution under □ adds a further proof of size polynomial in |ψ|.

A7 (remaining fields; G5).

• bmono is A2-style term arithmetic plus the S¹₂ theorem ∀a∀b∀x (a ≤ b ∧ □_a x → □_b x), instantiated, with ā ≤ b̄ proved by 7.4(a) at size poly(|b̄|).
• necU is nec plus one metatheoretic ∃-right.
• innerU is A3 with the budget quantified out by one more ∃-right inside the box; kdistU and diagU are proved as separate uniform statements (supplementary files A4-A5 §4.5 and A6-A7).

None of A1–A7 is printed in this form as far as we could find. Each is a statement about an explicit polynomial-time syntactic map, of the kind Buss 1986 §7 and Pudlák 1986 §3 treat as routine.

8. References

Primary: Pudlák 1986 (Thm 3.1, 3.5; Thm 5.5 and p. 192 for the upper bound for PA); Pudlák 1998 (Handbook of Proof Theory, ch. VIII) §6, and Thm 3.2.3 (Solovay's construction, unpublished, as presented there); Buss 1986 Ch. 7; Buss 1994; Critch 2019; Levine 2026 (arXiv 2609.15289); MAIS A1, P2 and open problems O1, O10, O12, O16, O17 (github.com/Math-for-AI-Safety/MAIS; "P2 l. …" line numbers refer to papers/P2/MAIS-P2.tex at commit 1cb9f003); Barász et al. 2014; cousin_it 2012; Armstrong 2012; Duclaux, Formenti, Cobben, Schölkopf and Jin 2026 (github.com/ColombanD/open-source-game-theory, main branch: engine/PrisonersDilemma/Base/BoundedGL.lean, Base/Loeb.lean); Critch, Dennis and Russell 2022 (arXiv 2208.07006, Open Problem 7). Pudlák 1996 (Collegium Logicum 2, 65–86; preprint on Pudlák's home page). Duclaux et al., branches colomban-arith-u10, colomban-recost and colomban-route-b of the same repository (arithmetized PA-S′), and their design notes (engine/PrisonersDilemma/Research/Notes/DESIGN_CHOICES.md, main branch, 2026-08-12). Freund and Pakhomov 2020, Short proofs for slow consistency, Notre Dame J. Formal Logic 61(1), 31–49 (arXiv 1712.03251, v2 read), Thm 3.6, Cor 3.5, Lemmas 3.1 and 3.2. Freund, A uniform characterization of Σ1-reflection over the fragments of Peano arithmetic, arXiv 1512.05122 (v1, 2015; refereed status unknown to us), Def. 1.1, Thm 3.13, Lemmas 3.8 and 4.7. Freund 2017, Proof lengths for instances of the Paris–Harrington principle, Ann. Pure Appl. Logic 168 (arXiv 1601.08185), p. 8 (the definition of F_ε0). Buss 1998, An introduction to proof theory (Handbook of Proof Theory, ch. I), §2.4.6 (free-cut elimination). Monroe 2026, Toward a characterization of simulation between arithmetic theories, arXiv 2604.27787 (v1), Thms 3.1 and 3.2. Tsimerman, 'Some new results in Open Source Game Theory', IPAM workshop Foundations of Interpretability, 2026-09-03 (recording: mathinstitutes.org/videos/25038; read via its auto-generated transcript). Unread (paywalled or not viewed): Montagna 1992 (JSL 57:844–863); Hájek, Montagna and Pudlák 1993 (Oxford Logic Guides 23, 197–221).