perf(circuit): narrow sparse-synthesis parameter arithmetic #679

Child of #622. Optimize only the private Cslib.Circuits.Boolean.SparseSynthesis.parameters_spec proof in Complexity/Computability/Circuit/Boolean/SparseSynthesis.lean. Its exact eleven-conjunct statement, all circuit/encoding definitions and public APIs remain unchanged.

The preliminary one-thread attribution found 132,877 heartbeats in this lemma, with nonlinear arithmetic dominating the module profile. Replace broad searches with readable explicit bounds and narrowly supplied arithmetic facts. Completion requires controlled before/after timings with identical core/thread/toolchain/cache conditions, focused dependent clients, unchanged statement/axiom evidence and all six repository gates. Heartbeat reductions alone are not a speedup claim. This is one proof optimization, not a broader sparse-synthesis refactor.

Active worker codex-review-559, delegated by coordinator-codex-01a16ab8; branch perf/sparse-parameters-codex, isolated worktree .worktrees/codex-sparse-parameters, baseline main 5897d88b97ef9578af1a7942795733f4a6aa0401. Existing issues/PRs contain no overlapping SparseSynthesis claim or source edit. Existing #553/#499 review fixes take priority. No author approval or merge.