feat(ForMathlib): Lipschitz cover of the normLeOne region frontier

[CBirkbeck]

Adds CebotarevDensity/ForMathlib/NormLeOneLipschitz.lean — a Lipschitz cover of the frontier
of the normLeOne fundamental region of a number field's canonical (mixed) embedding.
Self-contained (imports only mathlib's NumberField.…CanonicalEmbedding.NormLeOne); wired into the
umbrella CebotarevDensity import.

Contents

The headline results are normLeOne_frontier_lipschitz_cover and its mixed-space / index variants:
the boundary ∂(normLeOne K) is covered by finitely many Lipschitz images of the unit cube
[0,1]^{d-1} (d = #InfinitePlace K), with explicit Lipschitz constants. Supporting API: a
clampUnit retraction onto [0,1]^ι (1-Lipschitz), ContDiff charts of the region's faces
(expMapBasis / faceMap*), a phase-extraction Lipschitz bound (lipschitzWith_phase,
exists_phase_mem_Icc_mul_exp), and the liftToMixed assembly.

mathlib status (/mathlibable)

mathlib has the region NumberField.mixedEmbedding.normLeOne (which this file imports) but not
the Lipschitz structure of its frontier. That cover is exactly the geometric input the effective
lattice-point count (exists_card_inter_smul_lattice_sub_volume_mul_pow_le) consumes, so this is an
upstreaming candidate extending mathlib's canonical-embedding API. /generalise: maximal — the
clampUnit helpers are stated for an arbitrary Fintype ι, and the rest is intrinsically about a
NumberField K (already a variable).

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

🤖 Generated with Claude Code

[CBirkbeck]

Superseded by the stacked split #19 → #28 (10 slices of ~50 LOC each, per the review request for shorter PRs). Same NormLeOneLipschitz.lean, built up incrementally:

• feat(ForMathlib): clampUnit cube retraction (1/10) #19 clampUnit retraction · feat(ForMathlib): face-map charts of the normLeOne region (2/10) #20 face charts · feat(ForMathlib): frontier reduced to the box-boundary image (3/10) #21–22 boundary-in-faces · feat(ForMathlib): realSpace frontier Lipschitz cover (5/10) #23 realSpace cover · feat(ForMathlib): phase-extraction Lipschitz bounds (6/10) #24 phase bounds · feat(ForMathlib): lift the realSpace cover to mixedSpace (7/10) #25–26 mixed-space lift · feat(ForMathlib): bounded cover + fibre covering (9/10) #27 bounded/fibre cover · feat(ForMathlib): mixedSpace frontier cover + index variant (10/10) #28 mixed-space headline + index variant

Each slice builds green and is anchored by a public result. Closing this in favour of that stack.