fix(IEANTN): index Buthe_theta primes from 1

[Chessing234]

Summary

• Index Buthe_theta over Icc 1 ⌊x⌋₊ instead of Icc 0, consistent with the π*/ψ indexing cleanup in fix: π* index, CMS closed interval, Goldbach/PT–JY blueprints #1713.
• Factor the shared prime-filter equality into prime_filter_Icc_zero_eq_one (used by both comparison lemmas).

AI disclosure

Assisted with Cursor (ai / cursor labels per PULL_REQUEST_STYLE.md §13.1).

Test plan

• CI Build project

[Chessing234]

awaiting-review

[teorth]

Thanks for the follow-up to #1713 — indexing convention consistency is a good target. A few requested tweaks before merge:

1. De-duplicate the hset block. The seven-line filter-equality proof is currently pasted verbatim into both Buthe_theta_le_theta and eventually_Buthe_theta_eq_theta. PULL_REQUEST_STYLE.md §4 (the "Parallel proofs of parallel computations" cheat-sheet entry) asks that we extract it. Something like:

   private lemma prime_filter_Icc_zero_eq_one (n : ℕ) :
       (Finset.Icc 0 n).filter Nat.Prime = (Finset.Icc 1 n).filter Nat.Prime := by
     ext p
     simp only [Finset.mem_filter, Finset.mem_Icc]
     exact ⟨fun h => ⟨⟨h.2.one_le, h.1.2⟩, h.2⟩,
            fun h => ⟨⟨Nat.zero_le p, h.1.2⟩, h.2⟩⟩

   then each call site is rw [prime_filter_Icc_zero_eq_one].
2. AI-assistance disclosure. PULL_REQUEST_STYLE.md §13.1 (added in docs(PULL_REQUEST_STYLE): general-purpose tables (§5) + AI disclosure labels (§13) #1726) asks contributors using AI tooling to apply the ai umbrella label plus a company-specific label (cursor, etc.) and to note it in the PR body — please add whichever apply.
3. CI checkbox. The [ ] CI Build project box in the test plan is unchecked while the PR is awaiting-review — please tick it once lake build is green.

Substantive math is correct (both Icc 0 and Icc 1 filter to the same prime set), and the blueprint statement remains accurate. Happy to merge once the above are addressed.

[Chessing234]

extracted prime_filter_Icc_zero_eq_one, tagged ai/cursor, and checked the ci box (build was already green).

[Chessing234]

also: i don't have permission to add the ai/cursor labels from here — if you can slap those on, that covers §13.1 (already noted in the pr body).

[teorth]

All requested changes addressed (dedup extracted, AI disclosure added, CI green). Thanks!