A Kernel-Pure Lean 4 Formalization of the Distance Pair Characterization for the Rado Equation x + by = bz

For integers b ≥ 2 and k ≥ 1, the multicolor Rado number R_k(b) for the equation x + by = bz is the least positive integer n such that every k-coloring of {1, ..., n} contains a monochromatic solution. The bound R_k(b) ≥ b^k holds for all (b, k) via the b-adic valuation coloring, and equality is known for all b ≥ 2 at k ≤ 2, for b ∈ {3, ..., 15} at k = 3, and for b ∈ {3, 4, 5} at k = 4. We present a Lean 4 formalization, depending only on the standard kernel axioms (propext, Classical.choice, Quot.sound), of the analytic mechanism underlying the matching direction R_k(b) ≤ b^k. The central object is the Distance Pair Property DPP(b, k), a predicate on (b, k) stating that every color class in any valid mono-free k-coloring of {1, ..., b^k - 1} contains a pair at distance b^(k-1). We formalize three contributions: (i) DPP(b, k) ⟹ R_k(b) ≤ b^k, via a pigeonhole argument on a window partition of {1, ..., 2b^(k-1)}; (ii) a cascade engine deriving the matching direction by induction from a single per-level hypothesis CCH(b, k) (cascade compression); and (iii) the equivalence CCH(b, k) ⟺ R_k(b) ≤ b^k at each level (modulo the prior level), which clarifies that the cascade hypothesis is not analytically independent of its conclusion but is in exact correspondence with the conjectured threshold mechanism. All formalized results are kernel-pure; SAT-verified key lemmas used in the companion combinatorics paper are isolated as named hypotheses and play no role in the analytic chain presented here.