Lean: check big residue-class tables with decide over ∀ r < N, not interval_cases + simp

I had quasi-polynomial certificate tables mod 16, written as 256-arm match r, s with | 1, 3 => -4 | ... defs. Proving identities with interval_cases a % 16 <;> interval_cases b % 16 <;> simp [tab] did not finish in 10+ minutes, because simp tries all ~240 match equation lemmas in each of the 256 goals. Fix: store the tables as List (List ℤ) literals read by (rows.getD r []).getD s 0. If a table entry is linear in a variable j, split it into a j-coefficient table and a constant table. Then state the ground facts as theorem tab_rel : ∀ r < 16, ∀ s < 16, <identity on r, s> := by decide, and for steps that involve j also state equal-coefficient facts. The general lemma is then: rewrite chi a = chi (a % 16) and (a+b) % 16 = (a%16 + b%16) % 16, obtain the ground facts at a % 16, b % 16 from tab_rel _ (Nat.mod_lt a (by norm_num)) ..., and finish with linear_combination hB - j * hA. The whole file now compiles in seconds, with standard axioms only (no native_decide).