the proof notes, §8.1 (i), (ii-norm): the scale valuation with one Legendre level, the reduction cost ≤ -(v_p(scale) + allocCost), and the real relaxation of the allocation cost (completed square + Cauchy–Schwarz).

theorem Zeta32.Arith.Relaxed.padicValRat_finset_prod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) (f : ι → ℚ) (hf : ∀ i ∈ s, f i ≠ 0) : padicValRat p (∏ i ∈ s, f i) = ∑ i ∈ s, padicValRat p (f i)

theorem Zeta32.Arith.Relaxed.padicValRat_factorial_one_level {p m : ℕ} [Fact (Nat.Prime p)] (hm : m < p ^ 2) : padicValRat p ↑m.factorial = ↑m / ↑p

theorem Zeta32.Arith.Relaxed.padicValRat_scale_one_level {p n : ℕ} (hp : Nat.Prime p) (hsq : 5 * n < p ^ 2) : padicValRat p (scale n) = 3 * ↑n * (5 * ↑n / ↑p) - 12 * ↑n * (↑n / ↑p) - 2 * ∑ i ∈ Finset.range (3 * n), ↑i / ↑p

theorem Zeta32.Arith.Relaxed.cost_le_of_coeff_lower (r : ℚ) (n p : ℕ) (C : ℝ) (hpoly : Qtilde r n ≠ 0) (hC : ∀ (i : ℕ), (Qtilde r n).coeff i ≠ 0 → C ≤ ↑(padicValRat p ((Qtilde r n).coeff i))) : cost r n p ≤ -C

theorem Zeta32.Arith.Relaxed.cost_le_of_scaled_greedy (r : ℚ) (n p : ℕ) (hp : Nat.Prime p) (hQ : Q r n ≠ 0) (hG : GreedyBound r n p) : cost r n p ≤ -(↑(padicValRat p (scale n)) + ↑(allocCost n p (Classical.choose hG)))

theorem Zeta32.Arith.Relaxed.sum_sq_lower_range (p : ℕ) (hp : 0 < p) (f : ℕ → ℝ) : (∑ b ∈ Finset.range p, f b) ^ 2 / ↑p ≤ ∑ b ∈ Finset.range p, f b ^ 2

theorem Zeta32.Arith.Relaxed.allocation_relaxation (p h : ℕ) (hp : 0 < p) (c : ℕ → ℤ) (k : ℕ → ℕ) (hk : ∑ b ∈ Finset.range p, k b = h) : ↑h ^ 2 / ↑p + ↑h * ((∑ b ∈ Finset.range p, ↑(c b)) / ↑p - 1) + (∑ b ∈ Finset.range p, ↑(c b)) ^ 2 / (4 * ↑p) - (∑ b ∈ Finset.range p, ↑(c b) ^ 2) / 4 ≤ ∑ b ∈ Finset.range p, (↑(k b) * ↑(c b) + ↑(k b) * (↑(k b) - 1))

the proof notes, §8.1 (i): real relaxation of the allocation cost, with S = Σ c_b, Q₂ = Σ c_b² (so h(c-1) - Var/4 = h(S/p-1) + S²/(4p) - Q₂/4).

theorem Zeta32.Arith.Relaxed.allocCost_real (n p : ℕ) (k : ℕ → ℕ) : ↑(allocCost n p k) = ∑ b ∈ Finset.range p, (↑(k b) * ↑(colVal n p b) + ↑(k b) * (↑(k b) - 1))