Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

EtaSignK10

Abstract

The complete unshifted BHHK denominator-ten sign pattern at every natural index.

The original quotient is F10=E(q)^9/E(q^3)^10, with the denominator defined by its actual unit inverse and C10(n) its unshifted natural coefficient. Its first cubic trisection has constants -9 and 27 and zero component G10=E(q)^2/E(q^3)^3. The exact squared dissection identifies G10 with the sections UP,-VP,-WP. Positive ordinary partition coefficients smooth the W hole in every degree. Thus C10(9m+6) is strictly negative for every m, including m=0. The endpoint proves both residue-nine biconditionals and nonvanishing with no eventual or finite-range qualifier; C10_zero proves the empty-index value one. The mathematical derivation implements the supplied ordinary algebraic source dated 3 November 2026, SHA256 f9c81115730bc353681e172d5b2ad17d199d66bd4602b56a5da7dfe8e185852b. Classical cubic theta identities and positive convolution are reused from the existing k6 chain. These source statements do not certify independent formal review, literature priority, unique status, CI, merge, or original-problem acceptance.

Definition 1.1 (F10).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK10.F10

Formalization. D5/S3/Arith/ModularForms/EtaSignK10.F10 (✓ 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.

Commentary.

The ninth power of the actual Euler series times the tenth power of the unit inverse of E(q^3).

Definition 1.2 (C10).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK10.C10

Formalization. D5/S3/Arith/ModularForms/EtaSignK10.C10 (✓ 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.

Commentary.

The actual rational coefficient at the original natural index, including zero.

Definition 1.3 (G10).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK10.G10

Formalization. D5/S3/Arith/ModularForms/EtaSignK10.G10 (✓ 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.

Commentary.

The exact zero-progression quotient E(q)^2/E(q^3)^3.

Theorem 1.4 (F10_eq_expanded_inverse).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK10.F10_eq_expanded_inverse

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.F10_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.

Commentary.

The denominator is exactly the expansion of the ordinary Euler reciprocal.

Theorem 1.5 (zero_component).

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

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.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.

Commentary.

The cubic-lift zero component B^3 P^7 equals the actual G10.

Theorem 1.6 (first_dissection).

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

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.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.

Commentary.

The first exact trisection preserves the factors -9 and 27.

Theorem 1.7 (second_dissection).

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

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.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.

Commentary.

The zero component is the exact U,-V,-W partition smoothing.

Theorem 1.8 (smoothed_positive).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK10.smoothed_positive

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.smoothed_positive (✓ 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.

Commentary.

All coefficients of UP, VP, WP are strictly positive, with no hole.

Theorem 1.9 (five_coefficient_formulas).

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

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.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.

Commentary.

Five exact formulas cover both nonzero progressions modulo three and all remaining progressions modulo nine.

Theorem 1.10 (progression_signs).

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

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.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.

Commentary.

All five progression signs hold strictly for every natural parameter.

Theorem 1.11 (all_index_signs).

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

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.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.

Commentary.

C10 is positive iff its residue is 0,2,5,8; negative iff 1,3,4,6,7; every coefficient is nonzero.

Theorem 1.12 (C10_zero).

Lean statement: D5/S3/Arith/ModularForms/EtaSignK10.C10_zero

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EtaSignK10.C10_zero (✓ 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.

Commentary.

The constant coefficient of the actual quotient equals one.

References