The HIGH-case clearing: when the floor N lies below q^j (the scale of the top oversized base-q digit), a fresh LowDigits p window number drawn from [q^j, 2·q^j) is automatically good at every base-q index ≥ j and exceeds N — no carry control is needed. This discharges the high case of the clearing dichotomy; the low case is the μ-measure machine in MuFinish.

theorem Egrs75.Probe.good_above_of_mem_window {q j m : ℕ} (hq : 3 ≤ q) (hlo : q ^ j ≤ m) (hhi : m < 2 * q ^ j) (i : ℕ) : j ≤ i → m / q ^ i % q ≤ (q - 1) / 2

Goodness of the high block: if q^j ≤ m < 2*q^j and q ≥ 3, then every base-q digit of m at index ≥ j is ≤ (q-1)/2 (digit at j is 1, digits above are 0).

theorem Egrs75.Probe.clearing_high {p q : ℕ} (hp3 : 3 ≤ p) (hpo : Odd p) (hq3 : 3 ≤ q) (N : ℕ) {j : ℕ} (hjN : N < q ^ j) : ∃ (n' : ℕ), LowDigits p n' ∧ N < n' ∧ ∀ (i : ℕ), j ≤ i → ¬RepairPaperfaithful.BadAt q i n'

Clean branch of egrs_clearing: when q^j > N. If the top bad base-q index j of n satisfies q^j > N, then a LowDigits p number drawn from the window [q^j, 2*q^j) is > N and good at every base-q index ≥ j — no carry control needed. KERNEL-CLEAN.