Auxiliary Polynomial Fixed Degree

Abstract

A fixed-degree construction yields an auxiliary polynomial under the power inequality.

Theorem 1.1 (Auxiliary Polynomial Fixed Degree).

Lean statement: D5/S3/Arith/DiophantineApproximation/AuxiliaryPolynomialFixedDegree.exists_ne_zero_le_index_logHeight_le_of_pow_le

Proof. Machine-checked in Lean as D5/S3/Arith/DiophantineApproximation/AuxiliaryPolynomialFixedDegree.exists_ne_zero_le_index_logHeight_le_of_pow_le (✓ std3). ∎

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

Commentary.

A fixed-degree construction yields an auxiliary polynomial under the power inequality.

References

• Truth anchor: D5/S3/Arith/DiophantineApproximation/AuxiliaryPolynomialFixedDegree.exists_ne_zero_le_index_logHeight_le_of_pow_le
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/BombieriVaalerRelative
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/GaussLemma
• Dependency: D5/S3/Arith/DiophantineApproximation/BoxMonomial
• Dependency: D5/S3/Arith/DiophantineApproximation/CountingVolume
• Dependency: D5/S3/Arith/DiophantineApproximation/MvHasseDeriv
• Dependency: D5/S3/Arith/DiophantineApproximation/PolynomialIndex