The parameter inequality of the halting verifier

Blueprint lem:lambda-bound (ledger node 1.6.4): for all C, C' ≥ 1, all λ ≥ 4 · max ((4C) ^ (8C)) (C · log₂ C') and all n ≥ 2,

C · (C' · λ · n) ^ C ≤ n ^ λ.

This is the arithmetic that makes a λ-boundedness accounting go through. Every verifier the pipeline produces has running times polynomial in the level and in λ — poly(n, λ), the shape MIPRE.GapCompression.decider_time and sampler_time state — while MIPRE.Verifier.IsBounded λ asks for n ^ λ. The inequality says that once λ is large enough in terms of the polynomial's degree alone, the second dominates the first at every level n ≥ 2; and λ large enough is what blueprint lem:lambda chooses. C is the degree and C' the coefficient, so the threshold is exponential in the degree and only logarithmic in the coefficient — which is what keeps λ polynomial in the description length rather than exponential in it.

log is Nat.log 2 throughout, so the hypothesis is the integer reading of the blueprint's; nothing below needs it to be the real logarithm, and reading it as Nat.log 2 makes the threshold no larger.

The proof is the obvious one made finite. Bound each factor of the left-hand side by a power of n — C' ≤ 2 ^ (log₂ C' + 1) and λ ≤ 2 ^ (log₂ λ + 1) and C ≤ 2 ^ C, with 2 ≤ n — so that the claim reduces to the linear statement 4C + C · log₂ C' + C · log₂ λ ≤ λ. Two of those three terms are a quarter of λ by hypothesis outright. The third, C · log₂ λ ≤ λ / 4, is the only one with content: it is λ < 2 ^ (λ / (4C)), which holds once λ / (4C) exceeds 8C + 4, because 2 ^ q overtakes q ^ 2 at q = 4 (Nat.sq_le_two_pow_of_four_le) and q ^ 2 ≥ q · (8C + 4) > 4C · (q + 1) there.

Two facts about powers of two

theorem MIPRE.Halting.sq_le_two_pow_of_four_le {q : ℕ} : 4 ≤ q → q ^ 2 ≤ 2 ^ q

q ^ 2 ≤ 2 ^ q from q = 4 on. The induction step is (q + 1) ^ 2 ≤ 2 q ^ 2, which is q ^ 2 ≥ 2 q + 1, true from q = 3.

theorem MIPRE.Halting.four_mul_succ_lt_two_pow {C q : ℕ} (hC : 1 ≤ C) (hq : 8 * C + 4 ≤ q) : 4 * C * (q + 1) < 2 ^ q

The crossover the parameter inequality runs on: for C ≥ 1 and q ≥ 8C + 4, the linear function 4C(q + 1) is already below 2 ^ q.

theorem MIPRE.Halting.log_lt_div {C lam : ℕ} (hC : 1 ≤ C) (hlam : 4 * C * (8 * C + 4) ≤ lam) : Nat.log 2 lam < lam / (4 * C)

C · log₂ λ is below λ / (4C), once λ is past the crossover. This is the only clause of the parameter inequality with content.

The parameter inequality

theorem MIPRE.Halting.lambda_bound {C C' lam n : ℕ} (hC : 1 ≤ C) (hn : 2 ≤ n) (hlam : 4 * max ((4 * C) ^ (8 * C)) (C * Nat.log 2 C') ≤ lam) : C * (C' * lam * n) ^ C ≤ n ^ lam

Blueprint lem:lambda-bound. For C, C' ≥ 1, every λ ≥ 4 · max ((4C) ^ (8C)) (C · log₂ C') and every n ≥ 2,

C · (C' · λ · n) ^ C ≤ n ^ λ.

The threshold is exponential in the degree C and logarithmic in the coefficient C'.

The blueprint also asks C' ≥ 1; the proof does not need it (C' < 2 ^ (log₂ C' + 1) holds at C' = 0 too), so it is not a hypothesis here. Dropping it only strengthens the statement.