Make the 246 bounded-prime-gap theorem unconditional

[kimihiro64]

Summary - upgrades the project to Lean 4.33.1 and the matching Mathlib revision; - pins the Lean 4.33.1 module-compatible PrimeNumberTheoremAnd fork at 0f15a38c619298b5cd786d39a84dd4bb8997324c; - adds the completed Bombieri--Vinogradov formalization at afbcbb5959ad22f86ede6b3a53d5d396142fd32b; - single-sources Real.primeCountingZMod and the exact BombieriVinogradov proposition from that dependency; - adds PrimeGaps.Unconditional246, proving the unconditional frequent-gap, threshold-prime, and enumerated-prime formulations; - keeps the existing conditional Challenge/Solution pairs, while adding set_option autoImplicit false to every configured boundary file. ## Proof chain BombieriVinogradov.PrimeCountingConversion.weighted_to_prime_counting proves the exact proposition already consumed by PrimeGapsLib. The new bombieriVinogradov theorem supplies that proposition to the existing bombieriVinogradov_implies_*_246 theorems, producing: - frequently_prime_gap_le_246; - prime_gap_le_246; - nth_prime_gap_le_246. All four new public results use only propext, Classical.choice, and Quot.sound. ## Verification - local full build: lake build — 5,472 jobs passed; - local full lint: lake lint — all three default libraries passed; - Challenge/Basic.lean, Solution/Basic.lean, ChallengeFast/Basic.lean, and SolutionFast/Basic.lean each typecheck directly; - fork CI passed at the exact head commit: https://github.com/kimihiro64/PrimeGapsLib/actions/runs/33966896968; - hosted pinned Comparator/NanoDa verification passed for both configured declaration pairs at the exact head commit: https://github.com/kimihiro64/PrimeGapsLib/actions/runs/33969757043. The three declaration-local @[nolint checkType] annotations are limited to generated-scale private certificate declarations that kernel-check successfully but deterministically exhaust the linter's 200,000-heartbeat budget under Lean 4.33.1. No linter is disabled globally.

[kimihiro64]

Hosted verification is complete at https://github.com/kimihiro64/PrimeGapsLib/actions/runs/33969757043 for exact PR head ff4fbdc. The workflow ran both Comparator/comparator_fast.json and Comparator/comparator.json. The log records two successful Comparator completions, two NanoDa kernel acceptances, and two Lean default-kernel acceptances.

[kimihiro64]

Follow-up release evidence for the Bombieri-Vinogradov dependency:

• Final release: https://github.com/kimihiro64/bombieri-vinogradov/releases/tag/v0.1.4
• Exact release commit: 7a1748306e026825ed6a5555516cc2f28989b2ac
• All-gates CI: https://github.com/kimihiro64/bombieri-vinogradov/actions/runs/33976826783

That run passed the full Ubuntu Lean build, explicit Lean lint, Challenge/Solution Comparator export matching, NanoDa replay, Lean default-kernel replay, metadata/provenance, paper, offline API documentation, licensing, and downstream release verification. The published release contains exactly three nonempty remotely downloadable assets (paper PDF, Linux Lean build archive, and offline docs ZIP). The v0.1.4 hardening commits do not change the mathematical Lean source or its reviewed dependency pins from the proof release.