Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Three affine cosets in a shifted Eisenstein lattice

Abstract

Three affine cosets in a shifted Eisenstein lattice

The full lattice exponent Q(x,y)-x-y is nonnegative and has finite integer fibres. Three explicit affine cosets, selected by (x-y) modulo three, identify these fibres with three copies of the previously defined core fibres.

Definition 1.1 (shiftedExponent).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedExponent

Formalization. D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedExponent (✓ 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 shifted norm Q(x,y)-x-y.

Definition 1.2 (ShiftedFiber).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.ShiftedFiber

Formalization. D5/S3/Arith/ModularForms/CubicThetaShifted.ShiftedFiber (✓ 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 pair at the given natural exponent.

Theorem 1.3 (shifted_norm).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shifted_norm

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

Q(3x-1,3y-1)=9(Q(x,y)-x-y)+3.

Theorem 1.4 (shifted_exponent_nonneg).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shifted_exponent_nonneg

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

The shifted exponent is nonnegative at every integer pair.

Definition 1.5 (shiftedFiber_finite).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedFiber_finite

Formalization. D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedFiber_finite (✓ 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 shifted exponent fibre is finite.

Definition 1.6 (shiftedCoreEquiv).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedCoreEquiv

Formalization. D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedCoreEquiv (✓ 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 three affine cosets are disjoint and exhaust every shifted norm fibre.

Definition 1.7 (shiftedTheta).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedTheta

Formalization. D5/S3/Arith/ModularForms/CubicThetaShifted.shiftedTheta (✓ 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 rational series counting the full shifted fibres.

Theorem 1.8 (hasSum_shifted_theta).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.hasSum_shifted_theta

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/CubicThetaShifted.hasSum_shifted_theta (✓ 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 shifted fibre series is the full monomial sum over all integer pairs.

Theorem 1.9 (shifted_theta_eq_three_core).

Lean statement: D5/S3/Arith/ModularForms/CubicThetaShifted.shifted_theta_eq_three_core

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

This exact all-index identity supplies the multiplicity three in the Jacobi cube.

This is classical intermediate mathematics. CubicThetaCoreProduct supplies the downstream product-to-core lattice identity and EtaSignK6 supplies the exact all-index sign theorem. Independent formal acceptance and publication remain separate; no literature priority or novelty credit is asserted.

References