Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaIdentities

Abstract

The two classical cubic theta identities follow from genuine Euler products, complete lattices, and expanding coefficient induction.

The two classical cubic theta identities follow from genuine Euler products, complete lattices, and expanding coefficient induction.

Definition 1.1 (E).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.E

Formalization. D5/S3/Arith/ModularForms/CubicThetaIdentities.E (✓ std3).

Source. Repository-derived.

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 actual Euler series supplied by Mathlib’s pentagonal product theorem.

Definition 1.2 (P).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.P

Formalization. D5/S3/Arith/ModularForms/CubicThetaIdentities.P (✓ std3).

Source. Repository-derived.

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 unit reciprocal of the actual Euler series.

Definition 1.3 (expand3).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.expand3

Formalization. D5/S3/Arith/ModularForms/CubicThetaIdentities.expand3 (✓ std3).

Source. Repository-derived.

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 power-series algebra homomorphism substituting X cubed.

Definition 1.4 (B).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.B

Formalization. D5/S3/Arith/ModularForms/CubicThetaIdentities.B (✓ std3).

Source. Repository-derived.

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 actual quotient E(X)^3/E(X^3).

Theorem 1.5 (euler_mul_inverse).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.euler_mul_inverse

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

Source. Repository-derived.

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 Euler series times its normalized unit reciprocal equals one.

Theorem 1.6 (core_eq_product).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.core_eq_product

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

Source. Repository-derived.

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 full core lattice series equals the actual quotient E(X^3)^3/E(X).

Theorem 1.7 (B_dissection).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.B_dissection

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

Source. Repository-derived.

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.

This first cubic identity identifies an actual Euler quotient with the lattice dissection.

Theorem 1.8 (quotient_multiplication).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.quotient_multiplication

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

Source. Repository-derived.

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 quotient multiplication law is proved using only the two actual unit inverses.

Theorem 1.9 (cubic_defect_recurrence).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.cubic_defect_recurrence

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

Source. Repository-derived.

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 cubic defect satisfies a positive-degree expanding homogeneous recurrence.

Theorem 1.10 (cubic_identity).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaIdentities.cubic_identity

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

Source. Repository-derived.

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.

Both sides are the actual classical series; coefficient induction closes every degree.

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