Pseudo Basis Metrics

Abstract

The projective Arakelov height descends from the tuple height under nonzero scalar multiplication.

Definition 1.1 (Pseudo Basis Metrics).

Lean statement: D5/S3/Arith/AbsoluteValues/Heights/PseudoBasisMetrics.projectiveArakelovMulHeight

Formalization. D5/S3/Arith/AbsoluteValues/Heights/PseudoBasisMetrics.projectiveArakelovMulHeight (✓ std3).

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

Commentary.

The projective Arakelov height descends from the tuple height under nonzero scalar multiplication.

References

• Truth anchor: D5/S3/Arith/AbsoluteValues/Heights/PseudoBasisMetrics.projectiveArakelovMulHeight
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/PseudoBasis