Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaJacobiCube

Abstract

Locally finite integer sums realize the actual Jacobi series and its cube. Triangular exponent bounds justify the full Cauchy products, including every integer index.

Locally finite integer sums realize the actual Jacobi series and its cube. Triangular exponent bounds justify the full Cauchy products, including every integer index.

Theorem 1.1 (twice_triangular).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.twice_triangular

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaJacobiCube.twice_triangular (✓ 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 natural triangular exponent has twice its value equal to k(k-1) for every integer k.

Theorem 1.2 (triangular_bound).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.triangular_bound

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

A bound on the triangular exponent bounds the integer index in an explicit finite interval.

Definition 1.3 (jacobiTerm).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.jacobiTerm

Formalization. D5/S3/Arith/ModularForms/CubicThetaJacobiCube.jacobiTerm (✓ 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 signed triangular monomial at the integer Laurent index.

Theorem 1.4 (hasSum_jacobi).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.hasSum_jacobi

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaJacobiCube.hasSum_jacobi (✓ 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 genuine normalized product is the locally finite sum over every integer index.

Theorem 1.5 (hasSum_jacobi_cube).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.hasSum_jacobi_cube

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaJacobiCube.hasSum_jacobi_cube (✓ 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 cube includes all triples; local finiteness justifies the Cauchy products.

Theorem 1.6 (hasSum_map_jacobi).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.hasSum_map_jacobi

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

Coefficient maps preserve the complete locally finite Jacobi sum.

Theorem 1.7 (hasSum_mapped_triple).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaJacobiCube.hasSum_mapped_triple

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

Distinct coefficient evaluations retain every triple in the Cauchy product.

This classical intermediate supplies complete Jacobi columns. CubicThetaCoreProduct and CubicThetaIdentities prove the downstream product-to-lattice identities; EtaSignK6 proves the exact all-index sign theorem. Independent formal acceptance and publication remain separate.

References