Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaCubeDissection

Abstract

Every Laurent index of the genuine Jacobi cube is evaluated by a full affine lattice reindexing.

Every Laurent index of the genuine Jacobi cube is evaluated by a full affine lattice reindexing.

Definition 1.1 (residueExponent).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCubeDissection.residueExponent

Formalization. D5/S3/Arith/ModularForms/CubicThetaCubeDissection.residueExponent (✓ 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 nonnegative integer exponent 3tri(m)+rm for every integer m and residue r in Fin 3.

Theorem 1.2 (residue_exponent_nonneg).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCubeDissection.residue_exponent_nonneg

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCubeDissection.residue_exponent_nonneg (✓ 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 indices, including negative m, give a nonnegative residue exponent.

Theorem 1.3 (residue_exponent_cast).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCubeDissection.residue_exponent_cast

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCubeDissection.residue_exponent_cast (✓ 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 natural exponent preserves the exact integer polynomial.

Theorem 1.4 (cube_column_three_mul).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCubeDissection.cube_column_three_mul

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaCubeDissection.cube_column_three_mul (✓ 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 columns in residue zero are translated complete norm lattices.

Theorem 1.5 (cube_column_three_mul_add_one).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCubeDissection.cube_column_three_mul_add_one

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

All columns in residue one are translated shifted lattices, with the exact sign.

Theorem 1.6 (cube_column_three_mul_add_two).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaCubeDissection.cube_column_three_mul_add_two

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

Complementing the three integer indices gives every residue-two column.

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