Short independent algebraic integers at the uniform discriminant-root scale, from greedy lattice vectors, the multiplication pairing, and the covolume estimate.

The product-of-lengths bound for a prescribed first lattice vector. Each later vector is shortest outside the preceding span, and the covolume bound for positive monotone flag thresholds applies.

Numerical conversion of a lattice norm-product bound into the uniform discriminant-root scale for its largest minimum.

theorem CCDN.prescribed_greedy_lattice_basis_product_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {n : ℕ} {w : E} (b : Module.Basis (Fin (n + 1)) ℝ E) (hb : IsPrescribedGreedyLatticeFamily L w ⇑b) {δ : ℝ} (hδ : 0 < δ) (hlower : ∀ x ∈ L, x ≠ 0 → δ ≤ ‖x‖) : ∏ i : Fin (n + 1), ‖b i‖ ≤ ‖w‖ / δ * (↑n + 1) ^ (n + 1) * ZLattice.covolume L MeasureTheory.volume

If δ > 0 bounds the norms of nonzero lattice vectors from below, then a prescribed greedy lattice basis with first vector w satisfies ∏ i, ‖b i‖ ≤ (‖w‖ / δ) * (n + 1) ^ (n + 1) * covol(L).

theorem CCDN.exists_numberField_short_basis (K : Type u_1) [Field K] [NumberField K] (hd : 2 ≤ Module.finrank ℚ K) : ∃ (b : Module.Basis (Fin (Module.finrank ℚ K)) ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K)), (∀ (i : Fin (Module.finrank ℚ K)), b i ∈ NumberField.mixedEmbedding.euclidean.integerLattice K) ∧ ∀ (i : Fin (Module.finrank ℚ K)), ‖b i‖ ≤ ↑(Module.finrank ℚ K) ^ 3 * |↑(NumberField.discr K)| ^ (1 / ↑(Module.finrank ℚ K))

A real basis of integral lattice vectors with an explicit constant depending only on the field degree.