chore(int-factor): certify Phase 7 readiness

[kim-em]

Summary

• deduplicate factor-product and prime-support proof helpers, place the reusable prime-power lemma in HexArith, narrow the order module import, and clean IntFactor linter warnings
• add build-checked core and Mathlib-bridge READMEs plus a draft HexManual chapter covering certificates, APIs, search failure, fuel, and correspondence
• name the bridge headline correctness theorem and certify both IntFactor packages through local Phase 7

Verification

• lake build HexIntFactor HexIntFactorMathlib HexConformance HexManual
• lake exe runLinter on all affected core modules and both public HexIntFactorMathlib modules
• lake exe hexintfactor_bench verify (40/40)
• copyright, file-line-count, DAG, released-manifest, manual-split, trust-surface, Phase 4, Phase 7, Mathlib-free bench, and conformance-matrix checks
• build-checked README quickstarts

The runtime implementation and benchmark registrations are unchanged; check_phase4 reports changed registrations: 0, so the committed IntFactor Phase-4 artifact remains representative. The leanprover split-repository links in the READMEs are intentional pre-release publication targets and must be revalidated when released.yml gains these packages.

Independent review

A fresh Claude Opus review found no soundness defect. Follow-up commit 3b88110 moves the generic prime-power lemma upstream, removes the remaining duplicate, centralizes the ordered-tail proof, removes an anti-simp attribute, fixes Carmichael documentation, documents the retained partial proof field, and records the bridge headline theorem in its SPEC.

No released-repository publish or sync is performed here. Final directive closure remains with #9619.

Closes #9638