Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaWeightedProduct

Abstract

The genuine twisted product and its complete Laurent constant column identify the actual weighted Euler quotient.

The genuine twisted product and its complete Laurent constant column identify the actual weighted Euler quotient.

Theorem 1.1 (columnZero_mul_map).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.columnZero_mul_map

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

Laurent constant-column extraction commutes with multiplication by a scalar series.

Theorem 1.2 (columnZero_jacobi_cube_variable).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.columnZero_jacobi_cube_variable

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.columnZero_jacobi_cube_variable (✓ 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-dilated Laurent variable has only its integer index zero in column zero.

Theorem 1.3 (columnZero_expand).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.columnZero_expand

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

Laurent constant projection commutes with substitution of X cubed.

Theorem 1.4 (weighted_theta_mul_euler).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.weighted_theta_mul_euler

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

Taking the complete Laurent constant column proves the actual weighted product identity.

Theorem 1.5 (norm_dissection_mul_euler).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.norm_dissection_mul_euler

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaWeightedProduct.norm_dissection_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 rational cubic dissection is identified with E(X)^3/E(X^3), not assumed.

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