Row Entry Height
Abstract
The Arakelov height of a finite span is bounded by the product of its generators’ heights.
Theorem 1.1 (Row Entry Height).
Lean statement: D5/S3/Arith/AbsoluteValues/Heights/RowEntryHeight.arakelovMulHeight_span_range_le_prod
Proof. Machine-checked in Lean as D5/S3/Arith/AbsoluteValues/Heights/RowEntryHeight.arakelovMulHeight_span_range_le_prod (✓ std3). ∎
Citation. Ralf Stephan (2026). Subspace-Theorems. URL: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8.
Commentary.
The Arakelov height of a finite span is bounded by the product of its generators’ heights.
References
- Truth anchor:
D5/S3/Arith/AbsoluteValues/Heights/RowEntryHeight.arakelovMulHeight_span_range_le_prod - Dependency: D5/S3/Arith/AbsoluteValues/Heights/Duality
- Dependency: D5/S3/Arith/AbsoluteValues/Heights/Hadamard
- Dependency: D5/S3/Arith/AbsoluteValues/Heights/PseudoBasis