Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

EtaSignK6

Abstract

Two exact trisections and positive ordinary partition convolution give the full normalized k6 coefficient sign pattern.

Two exact trisections and positive ordinary partition convolution give the full normalized k6 coefficient sign pattern.

Definition 1.1 (F6).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.F6

Formalization. D5/S3/Arith/ModularForms/EtaSignK6.F6 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The normalized Euler quotient E(X)^9/E(X^3)^6, with its denominator realized by the actual unit inverse.

Definition 1.2 (C6).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.C6

Formalization. D5/S3/Arith/ModularForms/EtaSignK6.C6 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The rational coefficient at the original natural index in the normalized Euler quotient; no eta-shift relabelling.

Definition 1.3 (G6).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.G6

Formalization. D5/S3/Arith/ModularForms/EtaSignK6.G6 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The zero-progression quotient B(X)^2/E(X^3) used in the second trisection.

Theorem 1.4 (expanded_inverse).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.expanded_inverse

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.expanded_inverse (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

Expansion by three preserves the actual reciprocal of the Euler series.

Theorem 1.5 (F6_eq_expanded_inverse).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.F6_eq_expanded_inverse

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.F6_eq_expanded_inverse (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The expanded reciprocal equals the unit inverse used in the source-defined F6.

Theorem 1.6 (zero_component).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.zero_component

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.zero_component (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The first zero-progression expression is exactly B(X)^2/E(X^3).

Theorem 1.7 (first_dissection).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.first_dissection

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.first_dissection (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The first trisection has factors -9 and 27 and the correctly rescaled reciprocal Euler denominator.

Theorem 1.8 (second_dissection).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.second_dissection

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.second_dissection (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The second trisection has factors 1, -6 and 9 on the three remaining progressions.

Theorem 1.9 (five_coefficient_formulas).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.five_coefficient_formulas

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.five_coefficient_formulas (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

Five exact coefficient formulas cover every natural degree, including zero.

Theorem 1.10 (positive_convolution).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.positive_convolution

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.positive_convolution (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

Nonnegative lattice theta powers with constant term one convolved with ordinary partition powers have strictly positive coefficients.

Theorem 1.11 (progression_signs).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.progression_signs

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.progression_signs (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

Strict signs on the two progressions modulo three and the three remaining progressions modulo nine hold for every natural parameter.

Theorem 1.12 (all_index_signs).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK6.all_index_signs

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK6.all_index_signs (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Acknowledgement. Zeyu Huang, Timothy Huber, James McLaughlin, Pengjun Wang, Yan Xu and Dongxi Ye (2025). Sign-patterns of Certain Infinite Products. DOI: 10.48550/arXiv.2507.16644. URL: https://arxiv.org/abs/2507.16644v1.

Commentary.

The complete BHHK v1 table entry: positivity exactly at 0,2,5,6,8 modulo nine, negativity exactly at 1,3,4,7, and no zero coefficient.

Statements and proof dependencies come from the exact scoped Lean report. Classical theta mathematics is attributed to Borwein and Cooper as quoted in Huang et al. arXiv:2507.16644v1. The repository InversionSeq207 triple-product supplier is reused. No literature priority, worldwide absence, journal-typeset inspection, CI or original-problem acceptance is certified by this document.

References