Add Lean-core mul and div rounding theorems for unpacked format words

[rbeauchamp]

Closes #2.

Adds the format-word forms of the Lean-core mul and div rounding theorems offered in #2. A user of Float or Float32 can now apply them with only a finite result (and a finite divisor for division), without proving the roundWithAccuracy and divCore premises of toReal_ofModel_mul_finite_eq_roundAt and toReal_ofModel_div_finite_eq_roundAt. No existing statement or proof changes.

• toReal_ofModel_mul_toModel_eq_roundAt and toReal_ofModel_div_toModel_eq_roundAt (new module Arithmetic/LeanModel/MulDiv, beside LeanModel/AddSub): for a conventional IEEE descriptor and a finite result, Lean core's unpacked mul and div of the values unpacked from two format words have the same independent nearest-even real semantics as Model.mul and Model.div. Division also needs a finite divisor; the finite result already gives finite factors, a finite dividend and a nonzero divisor.
• toReal_ofModel_div_finite_eq_roundAt_of_isFinite: the existing division theorem without its two divCore premises. A zero provisional quotient, as for the least positive subnormal over 1.5, is rounded from its sign, selected exponent and remainder accuracy.
• le_targetExponent_totalExponent_iff, add_le_targetExponent_totalExponent_mul, le_targetExponent_totalExponent_of_toModel_eq_finite and divCore_exponent_le_targetExponent: the roundWithAccuracy precondition holds exactly when the exponent is at or below the minimum exponent or the mantissa has at least as many bits as the precision, so it holds for finite nonzero values unpacked from format words, for their products, and for every divCore result on nonzero mantissas.
• toReal_ofModel_roundWithAccuracy_zero_eq_roundAt: the zero-mantissa case that toReal_ofModel_roundWithAccuracy_eq_roundAt excludes.
• isFinite_toModel and isFinite_ofModel_notANumber: for a conventional IEEE descriptor, Lean core's finiteness test agrees with isFinite, and packing Lean's NaN is not finite.

The multiplication theorem for arbitrary unpacked operands keeps its exponent premise: two operands .finite .positive 1 0 have exact product 1, but Lean's result packs to the least subnormal. accuracyRepresents_accuracyOfFraction in Arithmetic/LeanModel loses private so the new module can reuse it, and Semantics imports the module. Chapter 18 of the guide gains one paragraph with a kernel-checked example, and Conformance/BinaryInterchange/NativeModel gains three boundary regressions (a zero provisional quotient with either sign, and a subnormal product at a tie) with entries in the axiom audit.

Checked on top of 79b69ef with tests/verify.sh: the publication privacy check, version pins, build (4,183 jobs), tests including the axiom audit, lint, and the architecture, public API docs and trust surface checks all pass. The optional Arb check was not run. site/build.sh passes in strict mode (21 chapters), and the CI workflow passed on my fork at this commit: https://github.com/rbeauchamp/FloatLib/actions/runs/37551566050. I also ran the kernel replay and had the documentation reviewed against the statements.

The proofs were developed with AI assistance and are checked by Lean's kernel.