[kim-em]

This PR uses guarded polynomial expansion in HexReflect, so term budgets apply to collected intermediate polynomials. For example, (x+y)^20 produces 21 terms and fits the default budget, but the existing estimate rejects it by counting over a million uncollected products.

Conversion uses the session's remaining term budget and literal exponent limit. It charges the final term count cumulatively, including across batch entries; cache hits are charged once. The coefficient-size check remains necessary because the shared expansion does not bound coefficient growth. Conversion proofs continue to use the existing soundness theorems and kernel evaluation of the pure polynomial computation.

Conformance tests cover the binomial power, numeric powers above the reification threshold, cumulative term exhaustion, cache accounting, and excessive coefficient growth. The new successful conversions have kernel-checked proofs. The existing core, scope, and residue conformance suites pass, including the Mathlib bridges.

This draft requires the guarded-expansion API already available in Lean's October 3 nightly. Hex's root toolchain is still rc3, so ordinary monorepo CI cannot build this change until its toolchain update. The isolated experiments/HexReflectNightly package pins that nightly and matching Mathlib revision and builds the production sources and all three reflection conformance suites without a whole-monorepo toolchain upgrade. It reads the production files directly and contains no alternative implementation.