Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaProductTwist

Abstract

Three genuine root-twisted Jacobi products are factored at finite cutoff, then passed to the coefficientwise limit.

Three genuine root-twisted Jacobi products are factored at finite cutoff, then passed to the coefficientwise limit.

Definition 1.1 (finiteFactor).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.finiteFactor

Formalization. D5/S3/Arith/ModularForms/CubicThetaProductTwist.finiteFactor (✓ 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 single finite product of shifted factors 1-C(z)X^(j+shift), for j below the cutoff.

Definition 1.2 (finiteEuler).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.finiteEuler

Formalization. D5/S3/Arith/ModularForms/CubicThetaProductTwist.finiteEuler (✓ 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 finite product of actual Euler factors from one through the cutoff.

Definition 1.3 (finiteJacobi).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.finiteJacobi

Formalization. D5/S3/Arith/ModularForms/CubicThetaProductTwist.finiteJacobi (✓ 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 finite Jacobi product with its degree-zero factor retained.

Definition 1.4 (jacobiEvaluation).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.jacobiEvaluation

Formalization. D5/S3/Arith/ModularForms/CubicThetaProductTwist.jacobiEvaluation (✓ 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 Jacobi series evaluated at a Laurent unit.

Theorem 1.5 (finite_jacobi_eq).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.finite_jacobi_eq

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaProductTwist.finite_jacobi_eq (✓ 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 finite product agrees with evaluation of the existing genuine Jacobi construction.

Theorem 1.6 (three_finite_factors).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.three_finite_factors

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

Finite factorization includes the zero-degree factor and both infinite-product directions.

Theorem 1.7 (finite_three_jacobi).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.finite_three_jacobi

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaProductTwist.finite_three_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 product of the three finite root twists factors into the cube-variable Jacobi product and Euler factors.

Theorem 1.8 (tendsto_finite_jacobi_evaluation).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.tendsto_finite_jacobi_evaluation

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

Finite Jacobi evaluations converge coefficientwise to evaluation of the actual Jacobi series.

Theorem 1.9 (three_jacobi_product).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaProductTwist.three_jacobi_product

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaProductTwist.three_jacobi_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 root-twisted product identity is obtained from finite factorizations without dividing.

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