Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaTwistedColumns

Abstract

Local finiteness retains every integer triple, and Laurent constant projection gives the complete weighted lattice sum.

Local finiteness retains every integer triple, and Laurent constant projection gives the complete weighted lattice sum.

Definition 1.1 (variableUnit).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.variableUnit

Formalization. D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.variableUnit (✓ 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 invertible Laurent monomial for the integer Jacobi index.

Definition 1.2 (constantUnit).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.constantUnit

Formalization. D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.constantUnit (✓ 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 embedding of a scalar unit into the Laurent coefficient ring.

Theorem 1.3 (variable_zpow).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.variable_zpow

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.variable_zpow (✓ 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 integer power of the Laurent variable is its corresponding single monomial.

Definition 1.4 (twist).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twist

Formalization. D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twist (✓ 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 Laurent ring homomorphism multiplying the variable by a scalar unit.

Theorem 1.5 (twist_single).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twist_single

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twist_single (✓ 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 twisted Laurent monomial carries exactly the scalar phase at its integer index.

Definition 1.6 (twistedCube).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twistedCube

Formalization. D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twistedCube (✓ 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 Jacobi series twisted by u, its inverse, and one.

Definition 1.7 (columnZero).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.columnZero

Formalization. D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.columnZero (✓ 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 linear projection to the complete Laurent constant column.

Theorem 1.8 (twisted_triple_term).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twisted_triple_term

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twisted_triple_term (✓ 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 zero-sum triple has norm exponent x^2+xy+y^2 and phase u^(x-y).

Theorem 1.9 (hasSum_twisted_column_zero).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.hasSum_twisted_column_zero

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

All integer pairs occur in the constant Laurent column, with their exact phase.

Theorem 1.10 (twisted_column_zero).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twisted_column_zero

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaTwistedColumns.twisted_column_zero (✓ 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 projected product is the full finite-fibre weighted theta.

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