feat(bz): migrate hot-path candidates after hex-primality release

[kim-em]

library: HexBerlekampZassenhaus
depends-on: #9891

Current state

Current main still contains the explicit 94-candidate trial-proved list. PR #9392 prepared a proof-carrying window over Hex.Nat.primeTable, but it was correctly parked because released HexBerlekampZassenhaus cannot import an unpublished HexPrimality library.

#9891 owns completing Phases 5–7 and publishing the HexPrimality split pair. This issue is not runnable until that prerequisite has produced a real released main SHA.

Deliverables

• Add the released HexPrimality pin ahead of HexBerlekampZassenhaus and the aggregate in scripts/release/released.yml.
• Rebase and adapt PR feat(bz): migrate hotPathCandidates onto the committed prime table #9392's table-window construction to the current Hex.ZMod64.Prime candidate shape.
• Replace the explicit hot-path lists with primeTable windows while preserving values, order, bundled bounds/primality evidence, deterministic tie-breaking, and the two coverage theorems.
• Update libraries.yml, Lake pins, factor-sweep freshness inputs, conformance, and affected performance evidence.
• Run the release sync dry-run before publication.

Verification

• lake build HexPrimality HexBerlekampZassenhaus HexFactorizationModules
• hot-path length/order/value and theorem conformance
• factor-sweep freshness and relevant benchmark checks
• release-manifest check and sync dry-run
• full CI

Out of scope

• Completing or publishing HexPrimality; chore(hex-primality): complete Phases 5–7 and publish the split pair #9891 owns that prerequisite.
• Hand-editing any released mirror.

[kim-em]

Claimed for implementation on branch issue-9849 by Codex session 01a055f2-ad7b-7f03-a35b-4d49342448be.

[kim-em]

Premise validation found that the release-layer blocker recorded on #9392 is still present, so I am stopping without changing source or weakening the requested migration.

Concrete evidence on current main (fe17b225b):

• libraries.yml records HexPrimality.done_through: 3 (lines 646–650), not Phase 7.
• scripts/release/check_released_manifest.py::check_phase_admission rejects a new source-bearing release entry below Phase 7: for an unpublished repo it raises “a new released.yml entry requires the completed phase pipeline. Finish Phase 7 or withdraw the entry until then” (lines 83–97).
• leanprover/hex-primality has no published branch or commit: the repository API reports size 0, and /branches returns [].
• scripts/release/released.yml still contains no hex-primality entry; hex-berlekamp-zassenhaus therefore has no legal released pin for it.
• HexBerlekampZassenhaus/PrimeSelection.lean still contains the explicit 94 trial-proved candidates, confirming the consumer migration has not independently landed.

Therefore adding HexPrimality.Table to the released BZ source now has only two outcomes, both invalid: adding the corresponding new manifest entry fails the Phase-7 admission guard, while landing the import without that entry publishes BZ with an unresolvable dependency. This is exactly the missing-infrastructure stop condition in the issue and repository instructions.

One secondary premise is also stale: conformance/HexPrimality/EmitFixtures.lean now says the hot-path migration is “tracked separately by issue #9849”; it no longer claims the existing segment cases consume the migrated view.

No files were changed, no PR was opened, and no release sync was dispatched. The issue can be retried after HexPrimality completes Phase 7 and its split repository has a real published main.