fix(poly-fast): prove remainder capacities

[kim-em]

Closes #9748.

• record exact divisor sizes, root degree, and sibling capacities in point and general remainder trees
• eliminate EvalPlan's silent unreduced-parent fallback by supplying proved capacity bounds to every cached division
• add the tight RemainderTree.remainders?_isSome_of_capacity theorem for p.size ≤ rootDegree + capacity
• preserve direct Horner evaluation for inputs larger than the plan size
• document the newly proved invariant and public observations

Verification:

• lake build HexPolyFast.RemainderTree HexPolyFast.Multipoint
• lake build HexPolyFast.Interpolation
• full lake build (10,500 targets)
• fresh Claude Opus review; its root-bound, proof-robustness, tail-recursion, and documentation findings were addressed