Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

CubicThetaWeightedNorm

Abstract

Complete finite Eisenstein norm fibres carry cubic phases. Six disjoint core cosets give the weighted cubic dissection.

Complete finite Eisenstein norm fibres carry cubic phases. Six disjoint core cosets give the weighted cubic dissection.

Definition 1.1 (weightedNormCoefficient).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weightedNormCoefficient

Formalization. D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weightedNormCoefficient (✓ 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 finite Eisenstein norm fibre summed with cubic root phase.

Definition 1.2 (weightedNormTheta).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weightedNormTheta

Formalization. D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weightedNormTheta (✓ 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 power series of full finite-fibre phase-weighted norm coefficients.

Theorem 1.3 (phase_mod).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.phase_mod

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.phase_mod (✓ 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 cubic phase depends only on its integer exponent modulo three.

Theorem 1.4 (hasSum_weighted_norm).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.hasSum_weighted_norm

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.hasSum_weighted_norm (✓ 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 entire root-weighted integer lattice sum has the finite-fibre coefficients.

Theorem 1.5 (weighted_norm_three_mul).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weighted_norm_three_mul

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

The residue-zero weighted fibre identifies with the norm fibre at the divided degree.

Theorem 1.6 (weighted_norm_three_mul_add_one).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weighted_norm_three_mul_add_one

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

The six disjoint core cosets have total phase weight minus three.

Theorem 1.7 (weighted_norm_three_mul_add_two).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weighted_norm_three_mul_add_two

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

The residue-two norm fibre is empty, so its weighted coefficient vanishes.

Theorem 1.8 (weighted_norm_dissection).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weighted_norm_dissection

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaWeightedNorm.weighted_norm_dissection (✓ 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 root-weighted lattice theta has the exact cubic dissection.

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