feat(ForMathlib): per-scale count↔volume bridge (1/2)

[CBirkbeck]

Part 1 of 2 — the former whole-file PR #11, split into stacked slices. Stacked on the IndexImageCount stack (PR 4/4) — review that first; GitHub retargets this base to master as the parents merge.

Adds CebotarevDensity/ForMathlib/LatticePointCount.lean with the per-scale count↔volume bridge and the two private helpers it consumes (bundled because the bridge is the module's first public result — a pure-helper slice would be an all-private module):

• index_mem_image_frontier_of_box_meet_not_subset — a box meeting but not contained in s has its index in the frontier image.
• measureReal_biUnion_box — the real measure of a finite union of grid boxes is card · n⁻ᵈ.
• abs_card_inter_sub_volume_mul_pow_le — #(s ∩ n⁻¹·ℤ^ι) differs from vol(s)·nᵈ by at most the number of n⁻¹ℤ^ι grid cells meeting ∂s.

The O(nᵈ⁻¹) boundary-cell bound it consumes (ncard_index_image_frontier_le) lives in IndexImageCount.lean (the parent stack). The terminal export follows in part 2. Wired into the umbrella CebotarevDensity import.

Builds green on the v4.31.0-rc1 / mathlib-master pin (identical to master's pin).

🤖 Generated with Claude Code

---

• depends on: feat(ForMathlib): Lipschitz-frontier boundary-cell count (4/4) #16

[xroblot]

Merge and fix the conflicts

[CBirkbeck]

Merged idx-4 and resolved the conflicts: kept the LatticePointCount import in the umbrella, and took idx-4's IndexImageCount.lean (this branch was carrying a stale pre-reorder copy). Full build is green. (Note: idx-4 itself is a bit behind idx-3 — it doesn't yet have the abs_sub 0 < n fix from PR #15 — so that'll flow down the stack separately as the lower PRs land.)

[xroblot]

Merge with master

[CBirkbeck]

Done in 39c61fb — merged master into lpc-1 and retargeted this PR's base from idx-4 to master (idx-4 / #16 is now merged, so it's an ancestor of master).

The merge was clean (no conflicts); it bumps the toolchain v4.31.0-rc1 → v4.32.0-rc1 in line with master. Net diff vs master is the intended 2-file slice — the LatticePointCount import in CebotarevDensity.lean plus CebotarevDensity/ForMathlib/LatticePointCount.lean. lake build CebotarevDensity is green against v4.32 (LatticePointCount compiles clean; the only sorry warnings are the pre-existing headline-theorem placeholders inherited from master).

[xroblot]

That looks like a lemma that could be useful elsewhere. Can you make it non private and see if you can use it somewhere else

[CBirkbeck]

Done in 693cd09 — dropped private from index_mem_image_frontier_of_box_meet_not_subset and added a docstring. Searched the codebase for another box/frontier-membership argument it could replace (IndexImageCount.lean, Cyclotomic.lean's preconnectedness use); found no other current call site with this exact shape, so it's exposed for future reuse rather than swapped in anywhere. (Also on development in d190652.)

[xroblot]

Suggested change

	≤ ({ν : ι → ℤ | ((box n ν : Set (ι → ℝ)) ∩ s).Nonempty}.ncard : ℝ) := by
	have hnpow : (0 : ℝ) < (n : ℝ) ^ Fintype.card ι :=
	pow_pos (by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n)) _
	have hMeetSub : {ν : ι → ℤ | ((box n ν : Set (ι → ℝ)) ∩ s).Nonempty} ⊆ index n '' s := by
	rintro ν ⟨x, hxb, hxs⟩
	have hMeetSub : {ν : ι → ℤ | ((box n ν : Set (ι → ℝ)) ∩ s).Nonempty} ⊆ index n '' s := by
	rintro ν ⟨x, hxb, hxs⟩
	exact ⟨x, hxs, mem_box_iff_index.mp hxb⟩
	have hFin : {ν : ι → ℤ | ((box n ν : Set (ι → ℝ)) ∩ s).Nonempty}.Finite :=
	(setFinite_index_image_of_isBounded n hbdd).subset hMeetSub

This code is also used in a similar way L170-173. It should probably be a lemma

[CBirkbeck]

Done in dc87809 — extracted setFinite_setOf_box_meet_nonempty (only needs [Finite ι], so it lives above the variable [Fintype ι] line to avoid an unused-instance lint) and swapped it in at both call sites: hFin in measureReal_mul_pow_le_ncard_setOf_box_meet (dropping the now-redundant hMeetSub) and hMeetFin in abs_card_inter_sub_volume_mul_pow_le. (Also on development in a11de5b.)

[xroblot]

This docstring should say "index" instead of "tag"

[CBirkbeck]

Done in dd3c659 — the lemma concludes ν ∈ index n '' frontier s, so the docstring now says "its index lies in the image" instead of "tag". (Also on development in 8575c9d.)

[xroblot]

Suggested change

	have hcon' : (box n ν : Set (ι → ℝ)) ∩ frontier s = ∅ := by
	rw [Set.eq_empty_iff_forall_notMem]
	rintro x ⟨hxb, hxf⟩
	exact hcon ⟨x, hxf, mem_box_iff_index.mp hxb⟩
	have hcon' : (box n ν : Set (ι → ℝ)) ∩ frontier s = ∅ :=
	Set.eq_empty_iff_forall_notMem.mpr fun x ⟨hxb, hxf⟩ ↦ hcon ⟨x, hxf, mem_box_iff_index.mp hxb⟩

You should be able to do the same kind of golf at many places in this PR and elsewhere

[CBirkbeck]

Done in dd3c659 — hcon' is now the one-line Set.eq_empty_iff_forall_notMem.mpr fun x ⟨hxb, hxf⟩ ↦ hcon ⟨x, hxf, mem_box_iff_index.mp hxb⟩ as suggested. Will look for the same pattern elsewhere in a follow-up pass rather than bundling it into this reply. (Also on development in 8575c9d.)