feat(ForMathlib): Lipschitz-frontier boundary-cell count (4/4)

[CBirkbeck]

Part 4 of 4 of the index-image counting bounds (split from PR #10) — completes IndexImageCount.lean. Stacked on part 3; GitHub retargets the base to master as parents merge.

Adds:

• ncard_index_image_frontier_le — if ∂s is covered by m images φⱼ '' [0,1]ᵈ⁻¹ of M-Lipschitz maps, the number of n⁻¹ℤ^ι grid cells meeting ∂s is O(nᵈ⁻¹), with explicit constant m · (2⌈M⌉₊+1)ᵈ · 2ᵈ⁻¹.

Sums the single-chart count from part 3 over the cover. This is the boundary-cell input that the effective lattice-point count (the follow-up LatticePointCount.lean stack) consumes.

Builds green on the v4.31.0-rc1 / mathlib-master pin.

🤖 Generated with Claude Code

---

• depends on: feat(ForMathlib): single-chart boundary-cell count (3/4) #15

[xroblot]

Merge master into this PR

[CBirkbeck]

Done — merged master in and retargeted the base:

• Base idx-3 → master (idx-3 merged in feat(ForMathlib): single-chart boundary-cell count (3/4) #15; its branch wasn't deleted, so GitHub didn't auto-retarget this one).
• Merged master — brings in the v4.32.0-rc1 pin and the now-generalised ncard_index_image_chart_le (φ : (κ → ℝ) → (ι → ℝ) for any [Fintype κ], landed in feat(ForMathlib): single-chart boundary-cell count (3/4) #15).
• Adapted this slice's ncard_index_image_frontier_le to the merged file: it now carries an explicit [Fintype ι] (master generalised the section variable to {ι : Type*}), and a one-line Fintype.card_fin normalisation restores the (n+1)^(|ι|-1) factor after the chart bound comes back as (n+1)^|Fin (|ι|-1)|. The rest of the proof is unchanged.

lake build CebotarevDensity is green locally on the merge; the diff is back to just this slice's frontier lemma on top of master.