Bombieri Vaaler Max Norm

Abstract

An integral basis of a matrix kernel has a discriminant and row-space height bound with an explicit complex-place factor.

Theorem 1.1 (Bombieri Vaaler Max Norm).

Lean statement: D5/S3/Arith/AbsoluteValues/Heights/BombieriVaalerMaxNorm.exists_basis_ker_prod_absMulHeight_le

Proof. Machine-checked in Lean as D5/S3/Arith/AbsoluteValues/Heights/BombieriVaalerMaxNorm.exists_basis_ker_prod_absMulHeight_le (✓ std3). ∎

Citation. Ralf Stephan (2026). Subspace-Theorems. URL: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8.

Commentary.

An integral basis of a matrix kernel has a discriminant and row-space height bound with an explicit complex-place factor.

References

• Truth anchor: D5/S3/Arith/AbsoluteValues/Heights/BombieriVaalerMaxNorm.exists_basis_ker_prod_absMulHeight_le
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/Duality
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/Extraction
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/MinkowskiSecond
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/MixedCube