feat(verify): algebraic-equivalence z3-UNKNOWN escalation (track B)

Standalone algebraic arm of the GEMM-rewrite z3-UNKNOWN escalation, plugging
into the _async_barrier_plan / _gemm_rewrite_proof interfaces. Three layers:

  (1) PRIMARY  z3-concrete-tiles: prove k=kt*tile_k+kk is a Presburger BIJECTION
      onto [0,K) on CONCRETE tiles (injective + covering ForAll + no-overshoot),
      plus per-term scale/mask identity. Decidable because tiles are concrete.
  (2) SECONDARY egglog: decide the product-multiset obligation EXACTLY by sorted
      kept-index equality (total, terminating), WITNESSED by a real egglog
      e-graph that comm+assoc soundly re-order a small representative spine.
      (A full K=64 comm/assoc saturation is combinatorial and does NOT
      terminate, so the e-graph witness is representative-bounded, labelled.)
  (3) DESIGN-ONLY Lean4/Mathlib sketch via finProdFinEquiv (text, not built).

RULE #1: every result bounded=True with a concrete scope (never forall-N); an
unresolved obligation returns proved_by="unproven" (never silently passed); a
missing egglog backend RAISES AlgebraicBackendUnavailable with the install cmd
(never a fake proof). NON-VACUOUS: gap/overshoot/non-injective/mismatched-scale/
mismatched-mask rewrites are REFUTED with concrete witnesses, locked by tests.

20/20 tests pass in 0.21s (z3 4.15.4 + egglog present).

Author: apstenku123