the proof notes, §8.1, Lemma 8 (relaxed greedy): for a prime p ≥ 7 with 5n < p² and 3p ≤ 7n, if some allocation of the 3n picks bounds every nonzero coefficient of Q r n (GreedyBound, i.e. the proof notes, Lemma 4), then cost ≤ n ψ(p/n) + 3/4. Steps: (i) Relaxed.Basic.allocation_relaxation; (ii) Relaxed.Columns.sum_colVal(_sq) and Relaxed.Basic.padicValRat_scale_one_level; (iii)–(iv) the identity (8.1)+(8.2) in the combined form −norm_p − relax = n ψ(x) + E_p, E_p = (p − 12n − 8r₀ + 2s₀ − 1)/(4p); (v) E_p < 3/4.

theorem Zeta32.Arith.Relaxed.sum_range_div_block_real {p : ℕ} (hp : 0 < p) (q : ℕ) : ∑ i ∈ Finset.range (q * p), ↑(i / p) = ↑p * ↑q * (↑q - 1) / 2

Floor sum Σ_{i<K} ⌊i/p⌋ = K q − p q (q+1)/2 for K = q p + r, r < p. -- adapted from -- dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Base/MediumFloorSum.lean

theorem Zeta32.Arith.Relaxed.sum_range_div_real {p K q r : ℕ} (hp : 0 < p) (hr : r < p) (hK : K = q * p + r) : ∑ i ∈ Finset.range K, ↑(i / p) = ↑K * ↑q - ↑p * ↑q * (↑q + 1) / 2

theorem Zeta32.Arith.Relaxed.scale_val_real {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)

v_p(scale n) as a real number, one Legendre level.

theorem Zeta32.Arith.Relaxed.psiL_eq (n p : ℕ) (hp : 0 < p) : ArithSum.psiL (↑p / ↑n) = have a := ↑(n % p) / ↑p; have b := ↑(5 * n % p) / ↑p; have g := ↑(3 * n % p) / ↑p; have m := ↑(min (n % p) (5 * n % p)) / ↑p; 6 + ↑p / ↑n * g * (1 - g) - 3 * (4 * a - b) + ↑p / ↑n / 4 * (16 * a + b - 8 * m - (4 * a - b) ^ 2)

ψ(p/n) through the residues n mod p, 5n mod p, 3n mod p.

theorem Zeta32.Arith.Relaxed.relaxed_algebra (n p A L M r₀ s₀ t₀ μ cst alloc v : ℝ) (hp : 0 < p) (hn : 0 < n) (eA : n = p * A + r₀) (eL : 5 * n = p * L + s₀) (eM : 3 * n = p * M + t₀) (hs : s₀ < p) (hr : 0 ≤ r₀) (hcost : cst ≤ -(v + alloc)) (hv : v = 3 * n * L - 12 * n * A - 2 * (3 * n * M - p * M * (M + 1) / 2)) (hrelax : (3 * n) ^ 2 / p + 3 * n * ((p * (4 * A - L - 2) + 4 * r₀ - s₀ + 1) / p - 1) + (p * (4 * A - L - 2) + 4 * r₀ - s₀ + 1) ^ 2 / (4 * p) - (p * (4 * A - L - 2) ^ 2 + 2 * (4 * A - L - 2) * (4 * r₀ - s₀ + 1) + 1 + 16 * r₀ + s₀ - 8 * μ) / 4 ≤ alloc) : cst ≤ n * (6 + p / n * (t₀ / p) * (1 - t₀ / p) - 3 * (4 * (r₀ / p) - s₀ / p) + p / n / 4 * (16 * (r₀ / p) + s₀ / p - 8 * (μ / p) - (4 * (r₀ / p) - s₀ / p) ^ 2)) + 3 / 4

The algebraic core of the proof notes, §8.1 (iii)–(v), over free real symbols with the relations n = pA + r₀, 5n = pL + s₀, 3n = pM + t₀: identities (8.1), (8.2) and E_p < 3/4.

theorem Zeta32.Arith.Relaxed.relaxed_per_prime (r : ℚ) (n p : ℕ) (hp : Nat.Prime p) (h7 : 7 ≤ p) (hsq : 5 * n < p ^ 2) (hQ : Q r n ≠ 0) (h73 : 3 * p ≤ 7 * n) (hG : GreedyBound r n p) : cost r n p ≤ ↑n * ArithSum.psiL (↑p / ↑n) + 3 / 4

the proof notes, §8.1, Lemma 8 (per prime, relaxed greedy).