feat: roadmap for arithmetic heights and Siegel's lemma

[rwst]

Adds TauCetiRoadmap/ArithmeticHeights/ — a seven-layer roadmap for heights of algebraic numbers,
polynomials, matrices and linear subspaces, with Siegel's lemma and its invariant refinement
Bombieri–Vaaler as the summit. The ultimate motivation is to have everything for a formalization
of the subspace theorems (a different roadmap).

The short version of the scope: Mathlib's Mathlib/NumberTheory/Height/ (M. Stoll) already has the
foundation, so this roadmap does not rebuild it. What is missing everywhere in Lean is the theory
that stands on it — the Arakelov normalization, the absolute height of a tuple, Northcott with
varying degree, Kronecker for the height, heights of polynomials and matrices, Schmidt's
Plücker-coordinate height of a subspace with its duality theorem, Minkowski's second theorem, and
both forms of Siegel's lemma over a number field.

Layers

0	Arakelov (ℓ²-at-infinity) height and its comparison with Mathlib's sup-norm height; extension invariance; the absolute height of a tuple
1	Northcott on projective space, the height ↔ Mahler-measure identity, Northcott's theorem with varying degree, Kronecker's theorem
2	Heights of polynomials (Gauss, Gelfond), linear forms, matrices
3	The Plücker point, Schmidt's subspace height, Cauchy–Binet, duality, submodularity, monotonicity
4	Successive minima and Minkowski's second theorem
5	Siegel's lemma over ℤ and over a number field; Bombieri–Vaaler; the auxiliary-polynomial form
6	Heights and units: the logarithmic-embedding dictionary, units of height one, S-units

Relationship to Mathlib

This is the part most worth reviewing. Mathlib already has, and the roadmap consumes rather than
restates: Height.AdmissibleAbsValues and the whole mulHeight/logHeight API, the projective
height, the number-field instance and its local formula, absMulHeight₁, the Northcott typeclass
and the fixed-field Northcott property, Siegel's lemma over ℤ, the Mahler measure, and
Dirichlet's unit theorem in full.

Two open Mathlib PRs cover named milestones. Per the README's never wait rule, both are built here
now under those PRs' own names and shapes, so adopting Mathlib's is a deletion plus an import:

• mathlib4#41606 — extension
  invariance, Layer 0.3 (mulHeight₁_pow_finrank, finrank_nsmul_logHeight₁, absMulHeight₁_eq).
• mathlib4#40791 — the S-unit
  theorem, Layer 6.5.

Two Mathlib TODOs are discharged rather than duplicated: Height/Northcott.lean asks for the
projectivization instances (Layer 1.1), and Height/Basic.lean asks for AdmissibleAbsValues on
finite extensions, for which Layer 0.3 supplies the arithmetic.

Boundaries

Canonical and naïve heights on elliptic curves stay in EllipticCurves (its Layer 6); effective
discriminant, class-number and regulator bounds stay in the completed EffectiveBounds, whose
TauCeti/NumberTheory/GeometryOfNumbers/ library Layer 4 extends; function-field heights stay in
AlgebraicCurves, and Layers 0–3 are stated at AdmissibleAbsValues generality wherever the proof
allows so that the function-field instance costs nothing here. Dirichlet's unit theorem itself is
Mathlib's and Layer 6 consumes it.

Two things to look at closely

The Layer 4 route. Bombieri–Gubler prove Siegel's lemma through the adelic Minkowski second
theorem; this roadmap pins the real route (restriction of scalars to a ZLattice in ℝ^{dN})
instead, to stay on the substrate Mathlib and EffectiveBounds already provide. Bombieri–Vaaler
§I.3 explains why they went adelic, and the roadmap records the residual cost explicitly: 4.1–4.3
and all one-vector statements are safe on the real route, while the basis statements (5.2
Theorem 2 and 5.3) rest on extracting K-independent vectors from ℝ-independent ones, which is
the step the adelic argument was doing. That is written up as a named gap the work must close, not
papered over. If reviewers prefer adelic for 5.3 alone, that is a one-paragraph change.

The two normalizations. Mathlib's height uses the sup norm at every place; the Siegel-lemma
literature states its constants for the Arakelov height (ℓ² at archimedean places). Both live in the
roadmap, related by a named comparison lemma (0.2), and every bound says which one it is in. Getting
this wrong silently is the main way this material goes bad.

Conventions

The Pinned conventions table fixes the ones an implementor would otherwise guess: multiplicative
primary with the logarithmic defined as its log; relative vs absolute distinguished by an abs
prefix; ⨆ i, v (x i) written out rather than wrapped in a predicate; Plücker coordinates indexed by
Set.powersetCard ι k to match Module.Basis.exteriorPower; the height of a matrix (entries) kept
notationally distinct from the height of its row space (minors), which the classical literature
writes with one symbol; duality via Submodule.dualAnnihilator; and S for S-units as finite places
only, matching Mathlib and #40791 — with a warning that Bombieri–Gubler takes the opposite convention
and states the rank as |S| − 1.

Sources

Keyed throughout to numbered results, primarily Bombieri–Gubler Heights in Diophantine Geometry
(§1.5–1.6, §2.8–2.9), with the two originals — Bombieri–Vaaler, Invent. Math. 73 (1983) and
Schmidt, Ann. of Math. 85 (1967) — checked directly, plus Hindry–Silverman (the reference
Mathlib's own SiegelsLemma.lean cites) and Cassels for Layer 4.

Mechanics

• Touches only TauCetiRoadmap/ArithmeticHeights/. The README roadmap list, the two issue-template
  dropdowns and TauCetiRoadmap.lean are left to the sync bot, per CONTRIBUTING.
• Suggested.lean pins 52 target signatures, all sorry. lake build passes.
• Applying awaiting-review.

AI assistance

Drafted with Claude Opus 5 (Claude Code), including the survey of the current Mathlib height
tree and the open PRs. I have read the whole thing carefully and take responsibility for it.

Update

Revises TauCetiRoadmap/ArithmeticHeights/, Layer 4. The previous version pinned the real
(adele-free) route to Bombieri–Vaaler but carried a ⚠ box naming one open gap — extracting
K-independent basis vectors from the ℝ-independent output of Minkowski's second theorem — and
allowed an adelic fallback for 5.3 if the gap would not close. This PR closes the gap as a new
milestone (4.4, the extraction lemma), names a second ingredient the route sentences had
silently assumed (4.5, Vaaler's cube-slicing theorem), and pins the covolume constant of 4.3
precisely. The result: the roadmap now asserts Bombieri–Vaaler at the exact constants on the real
route, end to end, with no adelic fallback anywhere.

What changed

• Layer 4 gains milestones 4.4 (extraction) and 4.5 (cube slicing); the ⚠ box is gone, its
  content absorbed into 4.4. The Route paragraph now states the exact-cancellation acceptance
  check and is honest about provenance (see Sources below).
• 4.3 is restated with its precise constant and measure convention, NumberField.mixedEmbedding
  in place of canonicalEmbedding, a proof route (ℚ first, then a pseudo-basis), and a new
  worked example over ℚ(i) that detects the two errors that are invisible over ℚ.
• 5.2 and 5.3 routes corrected. 5.2's "3.4 plus Layer 4 and nothing else" now points at 4.5
  explicitly and cites Aliev–Henk §6 as the reference to hold it against; 5.3's route goes through
  4.4/4.5 (the old route's appeal to 3.7 for the per-vector heights was not how the proof runs) and
  records why the constant has the shape it has.
• Ordering fixed: it claimed Layer 4 is fully independent of Layers 1–3 (false for 4.3) and
  that 5.2 needs neither Layer 3 nor 4 (contradicting 5.2's own route sentence).
• References: Vaaler 1979 (with Kanter 1977), Vaaler 2003, Aliev–Henk 2023, Fukshansky 2006,
  Roy–Thunder 1995 added; the Bombieri–Gubler entry now points at Appendix C.2/C.3 specifically.
• Suggested.lean: three new pinned signatures (the two halves of 4.4, and 4.5), the Layer 4
  header updated, and the Theorem-2 docstring's stale pointer to the deleted ⚠ box fixed.

The gap, closed (4.4)

The extraction is elementary, and losing nothing was the point of the old ⚠ box's worry:

• If u 1, …, u i ∈ K^N have ℝ-independent images under the mixed embedding, their K-span has
  dimension at least i/d: the embedding is ℚ-linear, and a K-space of dimension m is a
  ℚ-space of dimension d·m.
• So a greedy selection produces a K-basis from among the minima vectors, the j-th chosen
  from the first d(j−1)+1 — members of the family, never combinations, so each keeps the norm
  bound it arrived with.
• Since the minima are nondecreasing, λ_{d(j−1)+1}^d ≤ ∏_{r=1}^{d} λ_{d(j−1)+r}: the product of
  the selected heights is bounded by the full product Minkowski's second theorem controls. No loss.

This replaces exactly the step Bombieri–Vaaler §I.3 went adelic for (triangularizing a sublattice
needs 𝓞_K to be a PID). To de-risk the milestone before pinning it, both halves have been
machine-checked in Lean against current Mathlib, sorry-free, at the arbitrary-tower generality the
milestone states; the Suggested.lean signatures are the checked statements verbatim.

The unnamed dependency, named (4.5)

The sharp constants of 5.2 and 5.3 need vol_k (V ∩ [−1,1]^N) ≥ 2^k — Vaaler's cube-slicing
theorem. This is a cost of the theorem, not of the route: Bombieri–Vaaler's own proof quotes it
for the archimedean local volumes, and Bombieri–Gubler carry it as Appendix C.3. The old route
sentences never named it, and it is the hardest single analytic ingredient in the roadmap, so it is
now a milestone, claimable on its own. The milestone also records the reduction that keeps the real
statement the only slicing statement needed: at a complex place the unit polydisc contains the cube
of half-side 1/√2, and slicing that inscribed cube gives (2/√2)^{2k} = 2^k — exactly what the
constant requires, so no polydisc analogue is asked for.

The constant, pinned (4.3)

The old 4.3 said the covolume is |discr K|^{k/2} times "the subspace height" — off by
2^{−r₂ k} against Mathlib's measure normalization, and silent on sup-vs-Arakelov and
relative-vs-absolute. It now reads

covol (V ∩ (𝓞 K)ⁿ)  =  2^{−r₂ k} · |discr K|^{k/2} · H_Ar(V)^d

pinned to volume_fundamentalDomain_latticeBasis. The Route paragraph records the acceptance
identity: the 2^{dk} of 4.2, the 2^{−r₂ k} of 4.3 and the 2^{(r₁+r₂) k} of 4.5's slice
bounds cancel exactly, which is how 5.3's bound comes out with no spare factor — a proof that
produces a stray power of 2 or of the degree has a normalization wrong upstream.

Sources

The revision rests on a literature pass over the non-adelic Siegel literature. What it found, now
cited in the roadmap: the adele-free assembly over ℚ is written out in Aliev–Henk §6 (Theorems
6.2–6.3); the covolume closed form is classical (Fukshansky 2006, attributed there to Thunder);
some power of the discriminant must appear in 5.3's bound (Roy–Thunder 1995), so the constant's
shape is intrinsic; and the best-possible constant is a generalized Hermite constant (Vaaler 2003),
which the references record explicitly as not the target. What it did not find is a published
end-to-end restriction-of-scalars proof at the exact constant — authors who build the ℝ^{dN}
lattice still switch to adelic bodies for the geometry — so the Route paragraph now says plainly
that the assembly, with 4.4 in place of the adelic triangularization, is this roadmap's own, and
that the milestones, not any single reference, are the specification.

Mechanics

• Touches only TauCetiRoadmap/ArithmeticHeights/ (README.md, Suggested.lean). No layer added
  or removed; no target dropped.
• Suggested.lean now pins 55 target signatures (was 52), all sorry. lake build passes.
• Applying awaiting-review.

AI assistance

This revision was drafted with Claude Fable 5 (Claude Code), including the literature pass and
the machine-checked extraction lemma. I have read the whole thing carefully and take
responsibility for it.

Reviewers: the two places worth a careful eye are the extraction argument in 4.4 (one
paragraph of linear algebra; the roadmap's exact-constant claim for the real route stands on it)
and the constant bookkeeping in 4.3/Route (the ℚ(i) worked example is the intended check). A
subject-area reader on geometry of numbers would also be welcome on whether 4.5 should ask for
anything beyond the real cube statement; we deliberately did not, per the inscribed-cube reduction.