Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

QuadraticPrefixParity

Abstract

A disjoint sigma union applies the sign-product rule with exact multiplicities. The central interval lengths sum to m(m+1). The resulting integral congruence modulo4 supplies quotient parity; reflection supplies the even square norm. These are consumed in both prime families.

A disjoint sigma union applies the sign-product rule with exact multiplicities. The central interval lengths sum to m(m+1). The resulting integral congruence modulo4 supplies quotient parity; reflection supplies the even square norm. These are consumed in both prime families.

Four-slot escape registrations are unfinished, tracked at https://github.com/the-omega-institute/trureturing/issues/26321. No declared_validated status is claimed. This registration debt is separate from the native mathematical proof.

Theorem 1.1 (sign_rows_mod_four).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.sign_rows_mod_four

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.sign_rows_mod_four (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

Applying the sign rule to a genuine disjoint union counts repeated signs with multiplicity. Neither the total length nor its product is an extra hypothesis.

Theorem 1.2 (central_interval_length).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.central_interval_length

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.central_interval_length (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The lengths of the nested central intervals add to m(m+1).

Theorem 1.3 (central_half_sum_mod_four).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.central_half_sum_mod_four

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.central_half_sum_mod_four (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The sum of the central half-interval quotients modulo two, kept integrally modulo four. This supplies the parity correction in both energy arguments.

Theorem 1.4 (evenB_square_sum).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.evenB_square_sum

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.evenB_square_sum (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

Symmetry of the even quotient vector, including both zero endpoints.

Theorem 1.5 (evenB_add_central).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.evenB_add_central

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.evenB_add_central (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The even quotient differs from the central quotient by a negative prefix.

Theorem 1.6 (twice_prefix_sum_mod_four).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.twice_prefix_sum_mod_four

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.twice_prefix_sum_mod_four (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The sum of prefixes has the parity of the corresponding triangular number.

Theorem 1.7 (square_sum_mod_two).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixParity.square_sum_mod_two

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixParity.square_sum_mod_two (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

Squaring an integer preserves its parity, also under finite summation.

References