docs: plan shared algebraic reflection

[kim-em]

This PR adds two planning documents.

SPEC/lean4-sym-arith.md proposes completing Lean.Meta.Sym.Arith as Lean's shared algebraic reflection service, running in SymM rather than under a dormant Grind goal. It sequences the work as a strict copy-switch-delete migration of the reusable machinery out of Grind, and defers every generalization (the standalone interface, batch operations, and the rational, additive, noncommutative, module and symbolic-exponent views) until that migration has landed and the duplicates are deleted. It also records what parity requires, including that core tests alone do not cover the numeral-recognition boundary and the migration should be validated against https://github.com/leanprover/downstream-lean4.

SPEC/Libraries/hex-tactics.md specifies the Hex side against that interface: a state transformer over the caller's symbolic monad owning computational providers, derived typed views, direct conversions, conditional results, proof provenance and budgets, with Lean's algebraic grammar left closed. It covers scalar and additive normalization, matrix determinant, rank and characteristic polynomial, univariate and multivariate factorization, the rational-expression transformations together, cancel and apart, and which pieces stay Mathlib-free versus moving to a *-mathlib companion.

Not ready to merge. The Lean half of this depends on what Leo wants to do with Sym.Arith, and that conversation has not happened yet. The Hex document is written against the proposed interface, so its assumptions move if his answer does. Staying a draft until that is settled.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CrYPRybNqBoZYzXHpGCwKZ

[kim-em]

Marked draft during repository cleanup. This is a 1,949-line architecture proposal, not a routine merge candidate; it needs a current design review against the substantial tactics/interval work merged since August before it can be considered ready.