Closing FloatSpec Proof

[htlou]

Summary

This PR closes a large part of the FloatSpec proof gap and moves the repository toward a single, auditable Flocq translation target.

It:

• unifies FloatSpec so Core, Calc, Prop, Pff, IEEE754, ErrorBound, and support modules are all part of the same target
• removes the previous trust-tier split and treats remaining proof/spec gaps as repository-wide issues
• restores and proves many Flocq-aligned lemmas across Core, Prop, Pff, Pff2Flocq, and Double_rounding
• fixes mode-sensitive rounding behavior around round_to_generic
• adds pipeline tooling for placeholder audits, status reports, Codex-backed proof attempts, and attempt classification
• documents remaining exact Flocq revert targets in MISSING_INFRASTRUCTURE.md
• adds audit notes for existing spec misalignments, Flocq-vs-translation failure modes, and pipeline improvements

Current Status

The active missing-infrastructure list is down to 73 exact Flocq targets. The remaining gaps are documented explicitly in MISSING_INFRASTRUCTURE.md.