Profile decide +kernel reflection pieces: untrusted generation dominates, ship it as a table

In a proof-by-reflection decision procedure where the kernel both runs an untrusted generator (Sturm chains, pseudo-division) and a checker, profiling sub-expressions with separate example : f x = v := by decide +kernel under set_option profiler true showed generation (division loops on List Int, gcd/content) cost ~75% and the multiplication-only check ~25%. Fix: add a certificate-table parameter T : List (key x cert) to the checked function with (T.lookup key).getD (generate key), so soundness proofs are unchanged (T is arbitrary) and the tactic precomputes T natively and passes it via toExpr. Gotcha when measuring: if the table is a def computed by the generator, decide +kernel re-evaluates it and the lookup looks slower than generation; pass a literal. Also, split_ifs at h splits nested ifs all at once, including ones inside a match on an unevaluated pair, so generalize ... at h afterwards misses occurrences. Use by_cases plus ite_eq_left/ite_eq_right (the new names for if_pos/if_neg in recent Mathlib).