Phase Power Auxiliary Determinant
Abstract
Phase Power Auxiliary Determinant
Theorem 1.1 (Phase power endpoint criterion).
Lean statement: D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelEndpoints.phase_power_auxiliary
Proof. Machine-checked in Lean as D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelEndpoints.phase_power_auxiliary (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Bartosz Sobolewski, Maciej Ulas (2026). Hankel determinants of weighted binary sums of digits. DOI: 10.48550/arXiv.2607.09376. URL: https://arxiv.org/abs/2607.09376v1.
Commentary.
For d at least two and a d-th primitive root zeta, define the phase sequence F and its bordered determinant E. At every k at least one and every a, E at k minus one and size 2 to the k is nonzero exactly when no integer from zero through k minus one added to a is divisible by d.
References
- Truth anchor:
D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelEndpoints.phase_power_auxiliary - Dependency: D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelDeletion
- Dependency: D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelVanishing