Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

EulerNineSquareDissection

Abstract

Cubic residue extraction and positive decompositions control every squared section.

Write A=Q4, B9=Q2, C=Q1, and use the actual coloured partition product D from EulerNineComparison. The residue-two section of R^3 vanishes by the existing cubic theta dissection. Expanding the proved R dissection and cancelling the constant-one unit A gives B9^2=AC+qCD. Hence W=2AC-B9^2=(1-q)AC+q(AC-CD). Both summands are nonnegative by the paid restricted-product comparisons and exact AD=B9C multiplicities. This proves the difficult lower bounds without division of an inequality. The sole auxiliary degree-one hole is removed by ordinary partition smoothing in EtaSignK10.

Theorem 1.1 (restricted_cubic_relation).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.restricted_cubic_relation

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.restricted_cubic_relation (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

B9^2=AC+qCD is derived from actual theta suppliers and unit cancellation.

Definition 1.2 (U).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.U

Formalization. D5/S3/Arith/ModularForms/EulerNineSquareDissection.U (✓ std3).

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

The positive first squared section A^2+2qB9C.

Definition 1.3 (V).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.V

Formalization. D5/S3/Arith/ModularForms/EulerNineSquareDissection.V (✓ std3).

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

The signed second squared section 2AB9-qC^2.

Definition 1.4 (W).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.W

Formalization. D5/S3/Arith/ModularForms/EulerNineSquareDissection.W (✓ std3).

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

The difficult third squared section 2AC-B9^2.

Theorem 1.5 (coeff_U_ge_one).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_U_ge_one

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_U_ge_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

Every natural coefficient of U is at least one.

Theorem 1.6 (coeff_V_ge_one).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_V_ge_one

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_V_ge_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

Every natural coefficient of V is at least one by a positive exact decomposition.

Theorem 1.7 (W_positive_decomposition).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.W_positive_decomposition

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.W_positive_decomposition (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

W equals the lower reciprocal product plus q times the nonnegative difference AC-CD.

Theorem 1.8 (coeff_W_nonnegative).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_W_nonnegative

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_W_nonnegative (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

Every coefficient of W is nonnegative.

Theorem 1.9 (W_initial).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.W_initial

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.W_initial (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

W has constant coefficient one and degree-one coefficient zero.

Theorem 1.10 (coeff_W_ge_one).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_W_ge_one

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.coeff_W_ge_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

Every W coefficient at degree zero or at least two is at least one.

Theorem 1.11 (R_square_dissection).

Lean statement: D5/S3/Arith/ModularForms/EulerNineSquareDissection.R_square_dissection

Proof. Machine-checked in Lean as D5/S3/Arith/ModularForms/EulerNineSquareDissection.R_square_dissection (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kathrin Bringmann, Guoniu Han, Bernhard Heim and Ben Kane (2024). Periodic sign changes for weakly holomorphic eta-quotients. DOI: 10.48550/arXiv.2409.07164. URL: https://arxiv.org/abs/2409.07164v1.

Commentary.

The actual squared quotient is U(q^3)-qV(q^3)-q^2W(q^3).

References