Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaResidueSums

Abstract

The three full scalar residue sums at a cubic root are zero, Euler, and Euler.

The three full scalar residue sums at a cubic root are zero, Euler, and Euler.

Definition 1.1 (residueTerm).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.residueTerm

Formalization. D5/S3/Arith/ModularForms/CubicThetaResidueSums.residueTerm (✓ 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 complete signed monomial for an integer Jacobi index in a specified cubic residue.

Theorem 1.2 (residue_exponent_one).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.residue_exponent_one

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

The first residue exponent is precisely the generalized pentagonal number.

Theorem 1.3 (residue_exponent_two).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.residue_exponent_two

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

The second residue exponent is the pentagonal number of the negative integer index.

Theorem 1.4 (residue_exponent_reflection).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.residue_exponent_reflection

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaResidueSums.residue_exponent_reflection (✓ 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-residue exponent is preserved by the integer involution m to 1-m.

Theorem 1.5 (hasSum_residue_zero).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.hasSum_residue_zero

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaResidueSums.hasSum_residue_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 zero-residue sum vanishes by a complete integer involution, including both zero exponents.

Theorem 1.6 (hasSum_residue_one).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.hasSum_residue_one

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

The first residue is exactly Euler’s actual pentagonal series.

Theorem 1.7 (hasSum_residue_two).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaResidueSums.hasSum_residue_two

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

The second residue is the same Euler series by integer negation.

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