SRW on Z^3 transient in Lean: combinatorial local estimate, no Fourier

Bound P(S_m=0) <= (m/6+1)^(-3/2) + 3 q^m by counting. (1) card_nbij from pairs (d : Fin m → Fin 3, eps ∈ piFinset steps1) to closed paths via k ↦ Pi.single (d k) (eps k); surjectivity by choose p hp hpx using fun k ↦ mem_image.1 (hx.1 k). (2) For fixed d, card_nbij' between {eps | ∀ c, ∑ k ∈ {k | d k = c}, eps k = 0} and Fintype.piFinset (fun c ↦ closed paths on {k // d k = c}) with i eps = fun c k ↦ eps k.1, j eta = fun k ↦ eta (d k) ⟨k, rfl⟩; the dependent right-inverse goal closes by funext c k; obtain ⟨k, rfl⟩ := k; rfl, and Finset.sum_subtype converts subtype sums to filter sums. Instance mismatch when rewriting with that lemma later: use congr 1; convert lemma d. (3) Chernoff count without rpow: indicator[6r < m] <= s^m (s⁻¹^6)^r, and ∑_d u^#{k | d k = c} = (u+2)^m via prod_ite + Fintype.prod_sum. s = 11/10 gives s(2+s^-6) ≈ 2.82 < 3. Note real-ordered-semiring product lemmas are prod_le_prod₀ / prod_le_one₀ (plain prod_le_prod is the ordered-monoid version).