Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaRootEvaluation

Abstract

Finite Laurent support justifies the complete cubic-root evaluation of the Jacobi cube.

Finite Laurent support justifies the complete cubic-root evaluation of the Jacobi cube.

Definition 1.1 (indexEquiv).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.indexEquiv

Formalization. D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.indexEquiv (✓ 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 quotient and nonnegative remainder give a genuine equivalence Fin 3 times Z with Z.

Theorem 1.2 (map_T_residue).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.map_T_residue

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.map_T_residue (✓ 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 ring evaluation with T(3)=1 depends only on the integer Laurent residue.

Theorem 1.3 (hasSum_evaluated_columns).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.hasSum_evaluated_columns

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

Evaluation of every Laurent column reconstructs the actual Jacobi cube.

Theorem 1.4 (hasSum_map).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.hasSum_map

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

A coefficient ring map from discrete rationals preserves the full formal-power-series sum.

Theorem 1.5 (evaluated_jacobi_cube).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.evaluated_jacobi_cube

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaRootEvaluation.evaluated_jacobi_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 full evaluated cube uses all three residue sums, with their exact phases and signs.

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