Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

QuadraticPrefixEnergy

Abstract

Finite sign prefixes have their length parity. Reflected interval sums give a triangular reduction of the literal double sum. The two quotient vectors are proved integral, their reflection and midpoint values give square norms, and an odd natural h satisfies the exact sign-square identity modulo32.

Finite sign prefixes have their length parity. Reflected interval sums give a triangular reduction of the literal double sum. The two quotient vectors are proved integral, their reflection and midpoint values give square norms, and an odd natural h satisfies the exact sign-square identity modulo32.

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.

Definition 1.1 (partialSum).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.partialSum

Formalization. D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.partialSum (✓ 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.

Inclusive positive-index partialSum; its value at zero is the empty sum.

Theorem 1.2 (twice_weighted_prefix).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_weighted_prefix

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_weighted_prefix (✓ 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 diagonal of the square accounts for the difference between the two triangles.

Theorem 1.3 (twice_weighted_predecessor).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_weighted_predecessor

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_weighted_predecessor (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.twice_weighted_predecessor supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.4 (reflected_row_sum).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.reflected_row_sum

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.reflected_row_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.

Splitting a translated interval at its midpoint and reflecting its upper part. There is no division in this integral identity.

Theorem 1.5 (difference_row_sum).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.difference_row_sum

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.difference_row_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.

Splitting a difference row at its unique zero argument. The negative part is reflected before summation, so no out-of-range natural subtraction is used for χ.

Theorem 1.6 (twice_triangle).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_triangle

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_triangle (✓ 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.

Triangular reduction of the actual double product sum for any reflected sign sequence. The square-one and cancellation hypotheses are supplied by the quadratic character.

Theorem 1.7 (prefix_mod_two).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.prefix_mod_two

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.prefix_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.

Prefixes of sign sequences have the parity of their length.

Definition 1.8 (evenB).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.evenB

Formalization. D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.evenB (✓ 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-case vector, defined by the integer quotient used in the ordinary proof.

Theorem 1.9 (twice_evenB).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_evenB

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_evenB (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.twice_evenB supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.10 (evenB_reflect).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.evenB_reflect

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.evenB_reflect (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.evenB_reflect supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.11 (evenB_midpoint).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.evenB_midpoint

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.evenB_midpoint (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.evenB_midpoint supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Definition 1.12 (oddB).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB

Formalization. D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB (✓ 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 odd-case vector; integrality is proved rather than imposed as a premise.

Theorem 1.13 (twice_oddB).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_oddB

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.twice_oddB (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.twice_oddB supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.14 (oddB_reflect).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB_reflect

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB_reflect (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.oddB_reflect supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.15 (oddB_midpoint).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB_midpoint

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB_midpoint (✓ 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 exact Lean declaration D5.S3.Arith.CharacterSums.QuadraticPrefixEnergy.oddB_midpoint supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.16 (sum_odd_reflection).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.sum_odd_reflection

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.sum_odd_reflection (✓ 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.

A reflection on an odd interval pairs every term except its midpoint.

Theorem 1.17 (oddB_square_sum).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB_square_sum

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.oddB_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.

The odd-case square norm is twice its lower half, with a proved zero midpoint.

Theorem 1.18 (odd_sign_square_mod32).

Lean statement: D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.odd_sign_square_mod32

Proof. Machine-checked in Lean as D5/S3/Arith/CharacterSums/QuadraticPrefixEnergy.odd_sign_square_mod32 (✓ 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 odd-integer identity is kept modulo 32 before cancellation of the factor two. The exponent is the natural quotient from the original class-number statement.

References