Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Weighted Deletion for Binary Carry Blocks

Abstract

Weighted Deletion for Binary Carry Blocks

Theorem 1.1 (Weighted determinant deletion).

Lean statement: D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelDeletion.weighted_deletion

Proof. Machine-checked in Lean as D5/S3/Combinatorics/DigitHankel/CyclotomicDigitHankelDeletion.weighted_deletion (✓ 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.

Let f over a field of characteristic zero satisfy the two binary carry recurrences with weights w and x, with k at least two and n in the stated middle range. Replacing f above the threshold 2 to the k by the correction x divided by two minus w gives a shorter sequence g. The Hankel determinant H at n and its bordered difference determinant E then equal the displayed powers of 2, x minus 2w, and the smaller determinants H prime and E prime at n minus 2 to the k.

References