Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaCoreProduct

Abstract

The actual quotient E(X^3)^3/E(X) equals the complete core lattice theta at every coefficient.

The actual quotient E(X^3)^3/E(X) equals the complete core lattice theta at every coefficient.

Theorem 1.1 (map_pentagonal).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.map_pentagonal

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

Every commutative coefficient ring map preserves the actual pentagonal Euler series.

Theorem 1.2 (coreTheta_mul_euler).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.coreTheta_mul_euler

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.coreTheta_mul_euler (✓ 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 complete lattice theta times the actual Euler product is E(X^3)^3.

Theorem 1.3 (euler_constant_one).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.euler_constant_one

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.euler_constant_one (✓ 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 product has constant coefficient one.

Theorem 1.4 (core_product_eq_theta).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.core_product_eq_theta

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.core_product_eq_theta (✓ 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 is the actual quotient, rather than a series defined to have nonnegative coefficients.

Theorem 1.5 (coeff_core_product).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.coeff_core_product

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

Every normalized quotient coefficient counts the entire finite integer lattice fibre.

Theorem 1.6 (root_equation).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.root_equation

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.root_equation (✓ 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 quadratic algebra contains a root of w squared plus w plus one.

Theorem 1.7 (root_cube).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.root_cube

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.root_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 chosen root has cube one.

Theorem 1.8 (eval_T_one).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.eval_T_one

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.eval_T_one (✓ 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 Laurent evaluation maps index one to the algebraic root.

Theorem 1.9 (eval_T_two).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.eval_T_two

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.eval_T_two (✓ 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 Laurent evaluation maps index two to the square of the root.

Theorem 1.10 (eval_T_three).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCoreProduct.eval_T_three

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCoreProduct.eval_T_three (✓ 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 Laurent evaluation maps index three to one.

These are attributed classical intermediate identities. CubicThetaIdentities proves the downstream Borwein relations and EtaSignK6 proves the exact all-index sign theorem. Independent formal acceptance and publication remain separate. No priority or unique claim is made.

References