Asymmetric BSG in Lean: prune low degrees first, keep ε explicit

Extending a symmetric BSG formalization to |A'+B'| (paths of length 3): (0) restrict Γ to A₁ = {a : |B| ≤ 2K deg a}, and prove |A||B| ≤ 2K|Γ₁| via card_filter_add_card_filter_not plus a fiberwise bound on discarded edges; (1) state dependent random choice with a general ε (bad ≤ ε|N|², τ = ε|B|/2K²). In the final contradiction, nlinarith fails because of K² · (A²/2K²) terms: derive εX < 2ε B D with linarith, multiply by K² with mul_lt_mul_of_pos_left, and close with a field_simp identity. (2) Define B' by degree into A₂ and get |B| ≤ 4K|B'| from edge counting split by sum_filter_add_sum_filter_not. (3) Paths a - b' - a' - b encoded as (a', b') ∈ M ×ˢ B; inject into S³ via (a+b', a'+b', a'+b). Gotcha: card_eq_sum_card_fiberwise needs (s := ...) explicit when the maps-to proof is fun e he => (mem_filter.1 he).2, else s is inferred as a weird filter. The ~250-line single proof needed maxHeartbeats 400000.