Refactor Bezoutian theorem layers

[PerAlexandersson]

Summary

• split the 2,402-line Bezoutian theorem monolith into six dependency-ordered semantic layers behind the existing compatibility facade
• preserve the complete 131-declaration API and narrow direct consumer imports
• reuse StrictPrecSameDegree.to_prec in the Wronskian bridge and make the complex-splitting dependency in Hadamard.Grace explicit
• document the architecture and record exact import-closure budgets

Verification

• lake-workspace build RealRooted (9,416 jobs)
• focused builds of all six layers, the facade, and direct consumers
• import-architecture live check and self-test
• proof-status live check and self-test
• root-import coverage (857 modules)
• exact declaration-stream comparison against bddc8f40 (131 = 131)
• representative axiom audits: only propext, Classical.choice, and Quot.sound
• changed-file width and git diff --check